Stepwise CTL Model Checking of State/Event Systems
by Jørn Lind-Nielsen and
Henrik Reif Andersen.
In CAV'99: Computer Aided Verification, Lecture Notes in Computer
Science, Springer.
Abstract
In this paper we present an efficient technique for symbolic model
checking of any CTL formula with respect to a state/event system.
Such a system is a concurrent version of a Mealy machine and is used
to describe embedded reactive systems. The technique uses
compositionality to find increasingly better upper and lower bounds of
the solution to a CTL formula until an exact answer is found.
Experiments show this approach to succeed on examples larger than the
standard backwards traversal can handle, and even in many cases where
both methods succeed it is shown to be faster.
[BiBTeX entry]
[Postscript]