Model Checking the Branching Time Temporal Logic CTL

Reference:

Keijo Heljanko. Model checking the branching time temporal logic CTL. Master's thesis, Helsinki University of Technology, Department of Computer Science and Engineering, Espoo, Finland, May 1997. Also available as: Series A: Research Report 45, Helsinki University of Technology, Department of Computer Science and Engineering, Digital Systems Laboratory.

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, PROD

Suggested BibTeX entry:

@mastersthesis{Heljanko:mthesis,
    address = {Espoo, Finland},
    author = {Keijo Heljanko},
    month = {May},
    note = {Also available as: Series A: Research Report 45, Helsinki University of Technology, Department of Computer Science and Engineering, Digital Systems Laboratory.},
    pages = {72},
    school = {Helsinki University of Technology, Department of Computer Science and Engineering},
    title = {Model Checking the Branching Time Temporal Logic {C}{T}{L}},
    year = {1997},
}