I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - Implementing LTL Model Checking with Net Unfoldings


J. Esparza and K. Heljanko. Implementing LTL model checking with net unfoldings. Research Report A68, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, March 2001.


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 = {Espoo, Finland},
    author = {J. Esparza and K. Heljanko},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {March},
    number = {A68},
    pages = {29},
    title = {Implementing {LTL} Model Checking with Net Unfoldings},
    type = {Research Report},
    year = {2001}

GZipped PostScript (271 kB)
PDF (281 kB)
Conference version