Information Technology Reference
In-Depth Information
Actors
j
1
,
j
2
and
h
are local, thus not visible to the environment. The monitored actor
i
may receive value
v
from actor
j
1
, read it from its mailbox, and then output it to some
environment actor
obs
, while recording this
external
output at
h
's mailbox (the tracer).
h
)
i
[
v
]
∗
A
τ
τ
−−→·
obs
!
v
−−−−→
]
◦
−−→·
(
ν
j
1
,
j
2
,
j
1
[
v
]
j
2
[
i
!
u
]
h
[
e
q
:
{
sd
,
obs
,
v
}
But if actor
j
2
sends its value to
i
before
j
1
, we observe a di
ff
erent external behaviour
h
)
i
[
u
]
∗
A
τ
τ
−−→·
obs
!
u
−−−−→
]
◦
−−→·
(
ν
j
1
,
j
2
,
j
1
[
i
!
v
]
j
2
[
u
]
h
[
e
q
:
{
sd
,
obs
,
u
}
i.e.,
A
outputs
u
instead of
v
to
obs
(accordingly monitor
h
would hold the entry
{
sd
instead); these behaviours amounts to an
internal choice
.
External choice
results when
A
receives di
,
obs
,
u
}
ff
erent external inputs: we can derive
i
?
v
1
−−−→
i
?
v
2
−−−→
A
B
1
,butalso
A
B
2
. Subsequently,
B
1
can only produce the external output
∗
obs
!
v
1
−−−−−→
∗
obs
!
v
2
−−−−−→
B
1
τ
whereas from
B
2
can only produce
B
2
τ
−→
−→
. Note that, in the first
case,
h
's mailbox is appended by entries
{
,
i
,
v
1
}
:
{
,
,
v
1
}
whereas, in the second
rv
sd
obs
case, it is appended by
{
rv
,
i
,
v
2
}
:
{
sd
,
obs
,
v
2
}
.
3
The Logic
To specify reactive properties of the systems we consider an adaptation of SafeHML[1]
(sHML) , a sub-logic of the Hennessy-Milner Logic (HML) with recursion.
4
It assumes
a denumerable set of formula variables,
X
,
Y
∈
LVar, and is defined by the grammar:
ϕ,ψ ∈
sHML ::
=
ff
| ϕ∧ψ |
[
α
]
ϕ |
X
|
max
(
X
,ϕ
)
The formulas for falsity,
ff
, conjunction,
ϕ∧ψ
, and action necessity, [
α
]
ϕ
, are inherited
from HML[18], whereas variables
X
and the recursion construct
max
(
X
,ϕ
)areusedto
define
maximal
fixpoints; as expected,
max
(
X
,ϕ
) is a binder for the free variables
X
in
, inducing standard notions of open and closed formulas. We only depart from the
logic of [1] by limiting formulas to
basic actions
ϕ
BAct, including just input,
i
?
v
,
and
unbound
outputs,
i
!
v
, so as to keep our technical development manageable.
Remark 3.
The handling of bounded output actions, (
h
)
i
!
v
, is well understood [24] and
does not pose problems to monitoring, apart from making action pattern matching cum-
bersome; it also complicates instrumentation (see Sec. 4 and 5). Silent
α,β ∈
labels can also
be monitored using minor adaptations; they however increase substantially the size of
the traces recorded, unnecessarily cluttering the tracing semantics of Section 2.
τ
ϕ{
ψ
/
The semantics of our logic is defined for closed formulas, using the operation
}
,
X
which substitutes free occurrences of
X
in
without introducing any variable
capture. It is specified as the satisfaction relation of Def. 1 (adapted from [1]). In what
follows, we write
weak
transitions
A
ϕ
with
ψ
∗
B
and
A
τ
∗
B
and
A
α
B
,for
A
τ
α
−→
===⇒
==⇒
→
→
·
∗
B
resp. We l e t
s
τ
→
(BAct)
∗
range over
lists of basic actions
and write sequences
·
,
t
∈
of weak actions
A
α
1
α
n
=⇒
s
==⇒
s
==⇒
=⇒···
B
,where
s
=α
1
,...,α
n
,as
A
B
(or as
A
when
B
is unimportant).
4
HML with recursion has been shown to be equally expressive to the
μ
-calculus[20].
