Implementing LTL Model Checking with Net Unfoldings

Reference:

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

Abstract:

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.

Keywords:

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

Suggested BibTeX entry:

@techreport{HUT-TCS-A68,
    address = {Espoo, Finland},
    author = {Javier Esparza and Keijo 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},
}