Biomedical Engineering Reference
In-Depth Information
The Computational Tree Logic allows the formulation of properties on this tree. It
is thus well adapted to formulate dynamical properties on undeterministic discrete
dynamical systems. In particular, one can express possibilities in the future. For
instance, the formula
EF
(
l
i
=0)expresses that “it is possible to reach a state in
which the level of the
i
th component is 0”, and the formula
EG
(
l
i
=0)expresses
that “it is possible that the
i
th component stay for ever at the level 0”.
Computational Tree Logic is defined in two steps. The first step consists in
defining the
syntax
of the logic, i.e. rules for constructing formulas. The second
step consists in defining the
semantic
of the logic, i.e. meaning of formulas.
The
syntax
of
CTL
is inductively defined by:
•
For all genes
i
and integers
k
,(
l
i
=
k
), (
l
i
<k
), (
l
i
>k
), (
l
i
≤
k
)and(
l
i
≥
k
)
are (
atomic
)
CTL
formulas.
• f
φ
and
ψ
are two
CTL
formulas then (
ψ
),
EX
(
φ
),
EF
(
φ
),
EG
(
φ
),
E
(
φ
U
ψ
),
AX
(
φ
),(
AF
(
φ
)), (
AG
(
φ
)), and (
A
(
φ
U
ψ
))are
CTL
formulas.
¬
φ
), (
φ
∧
ψ
), (
φ
∨
ψ
), (
φ
⇒
|
= between the states
x
of a
given asynchronous state graphs
S
and the
CTL
formulas
φ
. The semantic of atomic
formulas is the following:
x
The
semantic
is given by the satisfaction relation
|
=(
l
i
<k
)
if and only if
x
i
<k
and so on. The semantic of the classical logical connectives
¬
|
=(
l
i
=
k
) if and only if
x
i
=
k
;
x
(negation),
∧
(conjunction),
∨
(disjunction), and
⇒
(implication) is usual: for
instance,
x
|
=
ψ
. The other connectives,
called
temporal connectives
, are made with two letters and lead to formulas that are
satisfiedbyastate
x
according to the set of infinite paths of
S
starting from
x
.
3
Intuitively,
E
and
A
correspond to existential and universal quantifiers respectively:
E
means “for at least one path” and
A
“for all paths”. The other letters express
properties along the paths:
X
(
φ
) means that
φ
is true at the ne
X
tstep,
F
(
φ
) means
that
φ
is ture in the
F
uture;
G
(
φ
) means that
φ
is
G
lobally true, and (
ψ
U
φ
) means
that
ψ
is always true
U
ntil
φ
becomes true. See Fig.
2.12
for an illustration. Formally,
the semantic of temporal connectives is given by:
|
=
φ
∧
ψ
if and only if
x
|
=
φ
and
x
•
x
|
=
EX
(
φ
)
⇐⇒
there exists a successor of
x
satisfying
φ
.
•
x
|
=
AX
(
φ
)
⇐⇒
all the successors of
x
satisfy
φ
.
•
x
|
=
EF
(
φ
)
⇐⇒
there exists an infinite path starting from
x
which contains a
state satisfying
φ
.
•
x
|
=
AF
(
φ
)
⇐⇒
all the infinite paths starting from
x
contain a state
satisfying
φ
.
•
x
there exists an infinite path starting from
x
which only
contains states satisfying
φ
.
|
=
EG
(
φ
)
⇐⇒
3
An infinite path of
S
is an infinite sequence of states
x
0
x
1
x
2
,...
such that, for all
k ∈
N
:if
x
k
has a successor in
S
,then
x
k
→ x
k
+1
is an arc of
S
,and
x
k
=
x
k
+1
otherwise.
Search WWH ::
Custom Search