Model Checking the Branching Time Temporal Logic CTL

Reference:

Keijo Heljanko. Model checking the branching time temporal logic CTL. Research Report A45, Helsinki University of Technology, Digital Systems Laboratory, Espoo, Finland, May 1997.

Abstract:

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.

Suggested BibTeX entry:

@techreport{HUT-TCS-A45,
    address = {Espoo, Finland},
    author = {Keijo Heljanko},
    institution = {Helsinki University of Technology, Digital Systems Laboratory},
    month = {May},
    number = {A45},
    pages = {72},
    title = {Model Checking the Branching Time Temporal Logic {C}{T}{L}},
    type = {Research Report},
    year = {1997},
}

NOTE: Reprint of Master's thesis; see URL below.
PostScript (1 MB)
GZipped PostScript (219 kB)
See www.tcs.hut.fi ...