Date: May 1997
Pages: 72
Reachability analysis is a method for analyzing the dynamic behavior of a concurrent system. One way of specifying the properties that the behaviors of the system must fulfill is to use the branching time temporal logic CTL (Computation tree logic). The process of checking whether the behavior of the system fulfills the specified property is called model checking. In this work we analyze several algorithms for CTL model checking. The main contribution of this report is a new model checking algorithm with time complexity matching the best existing algorithms, and memory requirements which are either equal or smaller than the existing algorithms, depending on the structure of the system under consideration. The algorithm has a counterexamples and witnesses facility, which is very valuable when trying to find the cause of incorrect behavior of the system. The presented algorithm is also straightforward to implement efficiently, and we have implemented the algorithm in the PROD tool set.
Keywords: Model checking, temporal logic, CTL, verification, reachability analysis, state-space exploration, PROD.