Information Technology Reference
In-Depth Information
2
Preliminaries
A
Kripke structure
is a tuple
K
=(
Σ
;
Σ
0
;
δ
;`
) with
Σ
a finite set of states,
Σ
0
Σ
the
IP (
A
)
the labeling of the states with
atomic propositions
A
=
f
p
;:::g
. For technical reasons
we assume that every state has at least one successor state. A
path
δ
Σ
Σ
`
Σ
!
set of initial states,
the transition relation between states, and
:
π
=(
s
0
;
s
1
;:::
) is an
infinite sequence of states
s
i
2
Σ
.Define
π
(
i
)=
s
i
as the
i
-th state in
π
. We also use the
i
=(
notation
π
π
(
i
)
;
π
(
i
+1)
;:::
) for the suffix of
π
starting at
π
(
i
). The image operation
on a set of states
S
.
As temporal operators we consider, the
next time
operator
X
,the
finally
operator
F
, the globally operator
G
,the
until
operator
U
, and its dual, the
release
operator
R
.
An LTL formula
f
is called an
eventuality
iff
f
=
F
h
or
f
=(
g
U
h
). In this case
h
is called the
body
of
f
. We assume the formulae to be in negation normal form, as in
[2, 9, 10]. Thus negations only occur in front of atomic propositions. This restriction
does not lead to an exponential blow up because we have included the
R
operator that
fulfills the property
Σ
is defined as Img(
S
) :=
f
t
2
Σ
j9
s
2
S
:
(
s
;
t
)
2
δ
g
g
.
An LTL formulae
f
holds on a path
:
(
f
U
g
)
:
f
R
:
π
, written
π
j
=
f
, according to the following
definitions:
π
j
=
p
iff
p
`
(
π
(0))
π
j
=
:
piff
p
62 `
(
π
(0))
π
j
=
g
^
h f
π
j
=
g
and
π
j
=
h
π
j
=
g
_
hiff
π
j
=
g
or
π
j
=
h
i
i
π
j
=
G
giff
8
i
:
π
j
=
g
π
j
=
hiff
9
i
:
π
j
=
h
1
π
j
=
X
giff
π
j
=
g
i
j
π
j
=
g
U
hi f
9
i
:
π
j
=
h
and
8
j
<
i
:
π
j
=
g
i
j
π
j
=
g
R
hi f
8
i
:
π
j
=
h
or
9
j
<
i
:
π
j
=
g
Since we are only concerned with finding witnesses for LTL formulae, we define an
LT L f o r m u l a
f
to hold at state
s
Σ
ω
2
Σ
(written
s
j
=
f
) iff there exists a path
π
in
starting at
π
(0)=
s
with
π
j
=
f
. In addition we define
f
to hold in a set of states
S
Σ
(written
S
j
=
f
)iffthereexists
s
2
S
with
s
j
=
f
.
3
Single State Tableaux
In this section we present a variation on a tableau construction for explicit state model
checking of LTL properties based on [2, 19]. The nodes in these
hybrid
tableaux also
contain states of the model under investigation and not just temporal formulae. The
main contribution of our paper is a symbolic extension to this tableau construction and
is introduced Section 4.
The LTL model checking algorithm of [19] is the dual to the tableau construction
of [2]. In [2] universal path quantifiers are considered, whereas [19] and our approach
solve the dual model checking problem for existential path quantifiers. A tableau in the
sense of [19] can be transformed into a tableau of [2] by replacing every literal by its
negation, every temporal operator by its dual, e.g. every occurrence of
F
by
G
,every
E
by
A
, and every boolean operator by its dual as well, e.g.
^
by
_
. In essence this
Search WWH ::
Custom Search