Information Technology Reference
In-Depth Information
transformation is just a negation of every formula in the tableau. The terminology of a
successful tableau has also to be revised, which can be found further down.
We call the type of tableau of [19] a
single state tableau
(S-Tableau), since every
node in the tableau only contains a single state. Our tableau construction, introduced in
section 4, allows a set of states at each tableau node. These tableaux are called
multiple
state tableaux
(M-Tableau). In the rest of this section we will present a slight modifica-
tion of the S-Tableau construction of [19] and note some facts that can be derived from
[2, 19].
s
`
E
(Φ
;
p
)
s
`
E
(Φ)
s
`
E
(Φ
;:
p
)
s
`
E
(Φ)
p
2
A
p
2
A
R
A
+
:
p
2 `
(
s
)
;
R
A
−
:
p
62 `
(
s
)
;
s
`
E
(Φ
;
f
U
g
)
s
`
E
(Φ
;
g
)
s
`
E
(Φ
;
f
^
g
)
s
`
E
(Φ
;
f
;
g
)
R
U
:
R
^
:
s
`
E
(Φ
;
f
;
X
f
U
g
)
s
`
E
(Φ
;
f
R
g
)
s
`
E
(Φ
;
f
;
g
)
s
`
E
(Φ
;
f
_
g
)
s
`
E
(Φ
;
f
)
R
R
:
R
_
:
s
`
E
(Φ
;
g
;
X
f
R
g
)
s
`
E
(Φ
;
g
)
s
`
E
(
Φ
;
F
f
)
G
f
)
s
`
E
(Φ
;
f
;
XG
f
)
s
`
E
(
Φ
;
R
F
:
R
G
:
s
`
E
(Φ
;
f
)
s
`
E
(Φ
;
XF
f
)
s
`
E
(
X
Φ
1
;:::;
X
Φ
n
)
s
1
`
E
(Φ
1
;:::;
Φ
n
)
R
X
:
f
s
1
;:::;
s
m
g
=Img(
f
s
g
)
:::
s
m
`
E
(Φ
1
;:::;
Φ
n
)
s
`
E
(Φ)
s
`
E
(Φ)
R
split
:
Fig. 1.
S-Rules: Single state tableau rules.
A
single state sequent
(S-Sequent) consists of a single state
s
and a list of LTL
formulae
Φ
=(
Φ
1
;:::;
Φ
n
), written
s
`
E
(
Φ
). The order of the formulae in the list is
not important. An S-Sequent
s
Φ
1
^^
Φ
n
in
K
. An S-Tableau is a finite directed graph of nodes labeled with S-Sequents that are
connected via the rules shown in figure 1. The application of a rule results in edges
between the premise and each conclusion. If not otherwise stated, we assume that a
tableau is fully expanded, i.e. no rule can generate new sequents or edges. For technical
reasons a sequent may occur several times in a tableau. In particular, we assume that
two nodes labeled with the same sequent are connected with an edge generated by
application of the split rule
R
split
. This assumption allows us to extract an S-Tableau
from an M-Tableau without shortening paths in the tableau. Refer to Lemma 6 for more
details. We further assume that the split rule is only applied finitely often which keeps
the tableau finite, since the number of different sequents is finite and nodes labeled with
identical sequents can only be introduced by the split rule.
An S-Path
x
is defined as the sequence of labels (sequents) of the nodes on a path
through an S-Tableau. Since a path through a tableau can be both, finite or infinite,
`
E
(
Φ
) holds in a Kripke structure
K
iff
s
j
=
Search WWH ::
Custom Search