Multiple State and Single State Tableaux for Combining Local and Global Model Checking - Correct System Design: Recent Insights and Advances - page 171

The method of [7] translates an LTL model checking problem into a FairCTL model
checking problem. With the result of [13] this leads to a model checking algorithm that
is linear in the size of the model and exponential in the size of the formula. Again, these
complexity results are only valid for explicit state model checking. The algorithms of
[7, 15] are based on BFS and it is not clear how to implement them depth first.
The work by Iwashita [17, 18] does not handle full LTL and no complexity analysis
is given. But if we restrict our algorithm to the path expressions of [17, 18], then our
algorithm subsumes the algorithms of [17, 18], even for the layered approach of [18].
In [4] an M-Tableau construction for the modal µ -calculus was presented. The main
motivation in [4] for using set of states in sequents was to be able to handle infinite state
systems. Therefore no complexity results were given. In addition, the modal µ -calculus,
as already discussed above, can not represent LTL properties directly without a prior
translation [10, 29].
Our tableau construction is on-the-fly (see liveness example in Section 6) and only
needs O ( ) image computations. Previous symbolic model checking algorithms for

LTL [7, 15], based on fixpoint calculations, require O (

j Σ j

2 ) image computations.

j Σ j

9Con lu ion

Although our technique clearly extends the work of [17, 18] and bridges the gap be-
tween local and global model checking, we still need to show that it works in practice.
We are currently working on proving the conjecture that our tableau construction can be
implemented with linear complexity. We also want to investigate heuristics for applying
the split rule. The approximation techniques of [25, 26] are a good starting point.

References

[1] I. Beer, S. Ben-David, C. Eisner, D. Geist, L. Gluhovsky, T. Heyman, A. Landver, P. Paanah,
Y. Rodeh, G. Ronin, and Y. Wolfsthal. Rulebase: Model checking at IBM. In CVA'97 ,

number 1254 in LNCS, pages 480-483. Springer-Verlag, 1997.
[2] G. Bhat, R. Cleaveland, and O. Grumberg. Efficient on-the-fly model checking for CTL*.
In LICS'95 . IEEE Computer Society, 1995.
[3] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In
TACAS'99 , LNCS. Springer, 1999.
[4] J. Bradfield and C. Stirling. Local model checking for infinite state spaces. Theorectical
Computer Science , 96:157-174, 1992.
[5] R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transac-
tions on Computers , 35(8), 1986.
[6] J. R. Burch, E. M. Clarke, and K. L. McMillan. Symbolic model checking: 10 20

states and

beyond. Information and Computation , 98, 1992.
[7] E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. Fo r m a l
Methods in System Design , 10:47-71, 1997.
[8] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using
branching time temporal logic. In Logic of Programs: Workshop , LNCS. Springer, 1981.
[9] R. Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta

Informatica , 27, 1990.