Information Technology Reference
In-Depth Information
Informally,
T
is the logical constant true;
¬F
is the negation of
F
; a formula
K
X
expresses that an agent of
S
, identified by
X
(we write
X
∈ S
), can infer
the message
m
; the
M
:
αF
modality expresses the
possibility
to perform a
symbolic transition
M
:
α
and then satisfy
F
provided that
M
,M
is a consistent
list of constraints;
∨
i∈I
represents the logical disjunction. As usual, we consider
∨
i∈∅
as
F
, where
F
is a short-cut for
¬
T
.
=
M
where
M
is a list of constraints which regard the
free variables of the system and of the formula. This allow us to consider system
configuration where some variables may be free but somehow constrained.
Finally, the formal semantics of a formula
F ∈ SHML
w.r.t. a compound
system
S
is inductively defined in Tab. 4, where we assume that
Vars
(
S
)
The truth relation is
|
∩
Vars
(
F
)=
∅
.
Table 4.
Semantics of the logical language
S |
=
M
T
iff [[
M
]]
=
∅
K
X
S |
=
M
iff
X ∈ S, X
=
A
φ
and [[
M, m ∈
D
(
φ
)]] =
∅
S |
=
M
¬F
iff not
S |
=
M
F
∃S
:
S
M
:
c
!
m
S |
=
M
M
:
c
!
mF
iff
S
and
S
|
=
M,M
,M
,m∈m
F
−→
s
∃S
:
S
M
:
c
!
y
S |
=
M
M
:
c
?
xF
S
and
S
|
=
M,M
,M
,x∈y
F
iff
−→
s
∃S
:
S
M
:
τ
S |
=
M
M
:
τ F
−→
s
S
and
S
|
=
M,M
,M
F
iff
S |
=
M
∨
i∈I
F
i
iff
∃i ∈ I
:
S |
=
M
F
i
The model checking problem for finite processes w.r.t. the SHML formulas is
decidable when some conditions are fulfilled. In particular we say that a model
checking problem
S |
=
M
F
is well defined when
-
M
is closed and monotonic;
-
The free variables of
S
occurs in a term in the left hand side of a constraint
in
M
;
-
For each sub formula
M
:
c
!
mF
of
F
we have that all the variables in
vars
(
m
) occurs either in the left hand side of a variable in
M
or there is a
super-term
M
,c
?
xF
s.t. the variable is x.
-
We require that each constraint
t ∈
D
R
(
T
) that occurs in a list of constraints
M
in the subformula
M
:
αF
is such that for each constraint
t
∈
D
R
(
T
)
in
F
we have
T ⊆ T
. Moreover, we require that if a constrain
t ∈
D
R
(
T
)
occurs in
M
then for each constraint
t
∈
D
R
(
T
)in
F
we have
T
⊆ T
.
These conditions ensure that the
nfc
terminates.
Proposition 1.
A model checking problem well defined is decidable.
