Information Technology Reference
In-Depth Information
where the first sequent is not actually generated since it already exists in the tableau.
We have to combine the
R
split
rule with the image and atomic rules to technically
avoid introducing an intermediate sequent,
)in the example, that might
violate the invariant. The correctness and completeness results can be proven for this
modification as well. Without combining these rules each application of
R
X
,
R
A
+
or
R
A
−
could potentially need an additional application of
R
split
. This could potentially
double the number of sequents and the number of sequents with the same RHS can
only be bounded by 4
f
1
;
2
;
3
;
4
g`
E
(
Φ
j
Σ
j
, which is still linear in the number of states.
8
Complexity and Related Work
In this section we discuss the complexity of our new algorithm based on M-Tableaux
and compare it with other local and global techniques for LTL model checking.
The size of a tableau with root
Σ
0
`
E
(
f
), not using the optimization of the last sec-
tion, is in
O
(2
j
Σ
j
2
j
f
j
). The time taken is polynomial in the size of the tableau. Thus the
time complexity is (roughly) the same as the space complexity. With the optimization
of the last section the size of the tableau is reduced to
O
(
2
j
f
j
). As a consequence
the time complexity of our algorithm is at most polynomial in the number of states,
with a small degree polynomial, and exponential in the size of the formula. The explicit
state model checking algorithms of [2, 16, 21] are linear in the number of states and the
number of transitions. Note that the number of transitions may be quadratic in the num-
ber of states. If an explicit state representation is used, we conjecture that our tableau
construction can be implemented with the same linear time complexity. However, with
our approach we are able to use compact data structures, such as BDDs, to represent
sets of states symbolically and thus can hope to achieve exponentially smaller tableaux
and exponentially smaller running times for certain examples.
The method of [10] translates an LTL formula into a tableau similar to the tableaux
in our approach. In [10] the nodes contain only formulae and no states. The size of
the tableau can be exponential in the size of the LTL formula. The second step is a
translation of the generated tableau into a
µ
-calculus formula that is again exponential
in the size of the tableau. Additionally, the alternation depth of the
µ
-calculus formula
can not be restricted. With [13, 22] this results in a model checking algorithm with time
and space complexity that is double exponential in the size of the formula and single
exponential in the size of the model
K
.
In [15] an ELTL formula is translated to a Buchi automata with the method of [29].
This leads to an exponential blow up in the worst case. But see [14] for an argument
why this explosion might not happen in practice, which also applies to our approach.
The resulting Buchi automata is translated to
post-µ
, a forward version of the standard
modal
µ
-calculus, for which similar complexity results for model checking as in [13, 22]
can be derived. This translation produces a
µ
-calculus formula of alternation depth 2
which results in an algorithm with an at least quadratic running time in
j
Σ
j
.
The LTL model checking algorithm of [15] is also forward oriented. A forward
state space traversal potentially avoids searching through non reachable states, as it is
usually the case with simple backward approaches. However, it is not clear how DFS
can be incorporated into symbolic
µ
-calculus model checking.
j
Σ
j
Search WWH ::
Custom Search