Implementing a CTL Model Checker

Reference:

Keijo Heljanko. Implementing a CTL model checker. In L. Czaja, P. Starke, H.-D. Burkhard, and M. Lenz, editors, Proceedings of the Workshop Concurrency, Specification & Programming 1996, Informatik-Bericht Nr. 69, pages 75–84, Berlin, Germany, September 1996. Humboldt-University, Berlin.

Abstract:

This paper discusses the implementation of a branching time temporal logic CTL model checker for the PROD Pr/T-Net Reachability analysis tool. A new algorithm for model checking CTL is presented. This algorithm doesn't need the converse of the transition relation as the EMC algorithm does [4]. The algorithm also provides a counterexample and witness facility using one-pass reachability graph traversal. The ALMC local model checking algorithm as presented in [10] uses a two-pass algorithm. The new algorithm presented here is a global model checking algorithm and requires less memory in the worst case than the local model checking ALMC algorithm.

Keywords:

model checking, temporal logic, CTL, verification, PROD

Suggested BibTeX entry:

@inproceedings{Heljanko:CSP96,
    address = {Berlin, Germany},
    author = {Keijo Heljanko},
    booktitle = {Proceedings of the Workshop Concurrency, Specification \& Programming 1996},
    editor = {L. Czaja and P. Starke and H.-D. Burkhard and M. Lenz},
    month = {September},
    pages = {75--84},
    publisher = {Humboldt-University, Berlin},
    series = {Informatik-Bericht Nr. 69},
    title = {Implementing a {C}{T}{L} Model Checker},
    year = {1996},
}