Information Technology Reference
In-Depth Information
R∈
Actr
×
sHML
is a satisfaction relation i
ff
Definition 1 (Satisfiability).
A relation
:
(
A
,
ff
)
∈R
never
(
A
,ϕ∧ψ
)
∈R
implies
(
A
,ϕ
)
∈R
and
(
A
,ψ
)
∈R
whenever A
α
(
A
,
[
α
]
ϕ
)
∈R
implies
(
B
,ϕ
)
∈R
==⇒
B
(
A
,
max
(
X
,ϕ
))
∈R
implies
(
A
,ϕ{
max
(
X
,ϕ
)
/
X
}
)
∈R
∈|=
s
.
5
Satisfiability,
|=
s
,isthe
largest
satisfaction relation; we write A
|=
s
ϕ
for
(
A
,ϕ
)
Example 2 (Satisfiability).
Consider the safety formula
ϕ
safe
max
(
X
,
[
α
][
α
][
β
]
ff
∧
[
α
]
X
)
(2)
stating that a satisfying actor system cannot perform a sequence of two external actions
α
followed by the action
β
(through the subformula [
α
][
α
][
β
]
ff
), and that this needs to
hold after every
α
action (through [
α
]
X
); e
ff
ectively the formula states that sequences
of
α
-actions
greater than two
cannot be followed by a
β
-action.
Asystem
A
1
exhibiting (just) the behaviour
A
1
αβ
==⇒
satisfies
ϕ
safe
, as would a system
A
2
with just the (infinite) behaviour
A
2
α
A
2
.System
A
3
with a trace
A
3
ααβ
=⇒
===⇒
does not
ϕ
safe
. However, if at runtime,
A
3
exhibits the alternate behaviour
A
3
β
satisfy
=⇒
(through
an internal choice) we
would not be able to
detect the fact that
A
3
|=
s
ϕ
safe
.
Since actors may violate a property along one execution but satisfy it along another,
the inverse of
, is too coarse to be used for a definition of monitor
correctness along the lines of (1) discussed earlier. We thus define a
violation relation
,
Def. 2, characterising actors violating a property along a specific execution trace.
|=
s
, i.e.,
A
|=
s
ϕ
Definition 2 (Violation).
The violation relation, denoted as
|=
v
,isthe
least
relation of
BAct
∗
×
sHML)
satisfying the following rules:
6
the form
(Actr
×
A
,
s
|=
v
ff
always
,
|=
v
ϕ∧ψ
,
|=
v
ϕ
,
|=
v
ψ
A
s
if A
s
or A
s
if A
α
A
,α
s
|=
v
[
α
]
ϕ
==⇒
B and B
,
s
|=
v
ϕ
max
(
X
,ϕ
)
A
,
s
|=
v
max
(
X
,ϕ
)
if A
,
s
|=
v
ϕ{
/
}
X
Example 3 (Violation).
Recall the safety formula
ϕ
safe
defined in (2). Actor
A
3
, from
Ex. 2, together with the witness violating trace
ααβ
violate
ϕ
safe
, i.e.,(
A
3
,ααβ
)
|=
v
ϕ
safe
.
However,
A
3
together with trace
|=
v
ϕ
safe
. Def. 2 relates
a violating trace with an actor
only when
that trace leads the actor to a violation: if
A
3
cannot perform the trace
β
do not violate
ϕ
safe
, i.e.,(
A
3
,β
)
αααβ
,byDef.2,wehave(
A
3
,αααβ
)
|=
v
ϕ
safe
, even though
the trace is prohibited by
ϕ
safe
. A violating trace may also lead a system to a violation
before its end, e.g., (
A
3
,ααβα
)
|=
v
ϕ
safe
according to Def. 2.
5
It follows from standard fixed-point theory that the implications of satisfaction relation are
bi-implications for Satisfiability.
6
We write
A
,
s
|=
v
ϕ
in lieu of (
A
,
s
,ϕ
)
∈|=
v
. It also follows from standard fixed-point theory
that the constraints of the violation relation are bi-implications.
