Information Technology Reference
In-Depth Information
The other direction is proven by constructing a successful S-Path from a successful
SCC. This is easily done by generating a cyclic path segment through the SCC con-
taining every sequent in the SCC. From the start of the cycle we can find another path
segment back to the root of the tableau. Combining these two segments, repeating the
cyclic segment infinitely often, results in an infinite successful S-path.
t
If the tableau is unsuccessful then the root sequent can not hold. If the tableau is
successful then it contains a finite successful path or a successful SCC. In the first case
we can extract a finite witness for the root sequent by extracting a list of states from
the finite successful path. In the second case we extract the witness from the S-Path
generated in the second part of the proof for Lemma 3.
If we apply our approach to a universal model checking problem by using the nega-
tion of the universal property to be checked in the root of the tableau, then the procedure
described in the previous paragraph serves as an algorithm for generating counterexam-
ples.
To find the successful SCCs of an S-Tableau in linear time, a variation of the stan-
dard algorithm of Tarjan for the decomposition of a directed graph into its strongly
connected components can be used. In particular, whenever a new SCC in Tarjan's
algorithm is found, we check on-the-fly if it is successful. Thus the model checking
problem can be solved in linear time in the size of the tableau as well. The size of the
tableau is bounded by the number of different S-Sequents. Note that the split rule is
never applied in this context. The number of different S-Sequents in a tableau with root
s
2
j
f
j
), since the RHS of a sequent may contain an arbitrary subset
of subformulae of
f
. This gives an explicit state model checking algorithm with worst
case complexity linear in the size of the Kripke structure and exponential in the size of
the formula. For more details compare with [2].
A
cyclic path
is an infinite path of the form
A
`
E
(
f
) is in
O
(
j
Σ
j
B
ω
, that starts with a finite prefix
A
and continues with a path segment
B
repeated infinitely often. Not all infinite paths
through a tableau are
cyclic paths
. However, the proof of Lemma 3 shows that it is
enough to consider cyclic paths only, when looking for successful paths to determine
whether a tableau is successful.
4
Multiple State Tableaux
In this section we extend the tableau construction of the last section to handle multiple
states in one sequent. In combination with a symbolic representation, such as BDDs,
this extension potentially leads to an exponential reduction in tableau size. The idea
of handling set of states on the left hand side (LHS) of sequents already occurred in
[4] as an extension of local model checking for the modal
µ
-calculus [28]. The tableau
construction in this section extends the LTL model checking algorithm of [2] in a similar
way.
A
multiple state sequent
(M-Sequent) consists of a set of states
S
and a list of LTL
formulae
' to separate
left and right hand side of S-Sequents and M-Sequents, but capital letters, e.g.
S
,forset
of states on the LHS of M-Sequents and lower case letters, e.g.
s
, for S-Sequents. An
Φ
=(
Φ
1
;:::;
Φ
n
), written
S
`
E
(
Φ
). We use the same symbol '
`
Search WWH ::
Custom Search