Implementing LTL Model Checking with Net Unfoldings


Javier Esparza and Keijo Heljanko. Implementing LTL model checking with net unfoldings. In Matthew B. Dwyer, editor, Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN'2001), volume 2057 of Lecture Notes in Computer Science, pages 37–56, Toronto, Canada, May 2001. Springer-Verlag.


We report on an implementation of the unfolding approach to model-checking LTL-X recently presented by the authors. Contrary to that work, we consider an state-based version of LTL-X, which is more used in practice. We improve on the checking algorithm; the new version allows to reuse code much more efficiently. We present results on a set of case studies.


net unfoldings, model checking, tableau systems, LTL, Petri nets

Suggested BibTeX entry:

    address = {Toronto, Canada},
    author = {Javier Esparza and Keijo Heljanko},
    booktitle = {Proceedings of the 8th International {SPIN} Workshop on Model Checking of Software ({SPIN}'2001)},
    editor = {Matthew B. Dwyer},
    month = {May},
    pages = {37--56},
    publisher = {Springer-Verlag},
    series = {Lecture Notes in Computer Science},
    title = {Implementing {LTL} Model Checking with Net Unfoldings},
    volume = {2057},
    year = {2001},

See ...