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, InformatikBericht Nr. 69, pages 75–84, Berlin, Germany, September 1996. HumboldtUniversity, Berlin.
Abstract:
This paper discusses the implementation of a branching time temporal logic CTL model checker for the PROD Pr/TNet 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 onepass reachability graph traversal. The ALMC local model checking algorithm as presented in [10] uses a twopass 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 = {7584},
publisher = {HumboldtUniversity, Berlin},
series = {InformatikBericht Nr. 69},
title = {Implementing a {C}{T}{L} Model Checker},
year = {1996},
}
