@inproceedings{
    Heljanko:CSP96,
    editor = "Czaja, L. and Starke, P. and Burkhard, H.-D. and Lenz, M.",
    author = "Heljanko, Keijo",
    publisher = "Humboldt-University, Berlin",
    title = "Implementing a {C}{T}{L} Model Checker",
    url = "http://users.ics.tkk.fi/kepa/publications/",
    series = "Informatik-Bericht Nr. 69",
    booktitle = "Proceedings of the Workshop Concurrency, Specification & Programming 1996",
    year = "1996",
    corerank = "NA",
    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.",
    month = "September",
    juforank = "NA",
    address = "Berlin, Germany",
    keywords = "model checking, temporal logic, CTL, verification, PROD",
    pages = "75--84"
}