Research Report A68: Implementing LTL Model Checking with Net Unfoldings

Author: Javier Esparza and Keijo Heljanko

Date: March 2001

Pages: 29

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

Full report in Postscript
Full report in Portable Document Format