Combining symbolic and partial order methods for model checking 1-safe Petri nets

No Thumbnail Available
Journal Title
Journal ISSN
Volume Title
Doctoral thesis (article-based)
Checking the digitized thesis and permission for publishing
Instructions for the author
Degree programme
55, [97]
Research reports / Helsinki University of Technology, Laboratory for Theoretical Computer Science. A, 71
In this work, methods are presented for model checking finite state asynchronous systems, more specifically 1-safe Petri nets, with the aim of alleviating the state explosion problem. Symbolic model checking techniques are used, combined with two partial order semantics known as net unfoldings and processes. We start with net unfoldings and study deadlock and reachability checking problems, using complete finite prefixes of net unfoldings introduced by McMillan. It is shown how these problems can be translated compactly into the problem of finding a stable model of a logic program. This combined with an efficient procedure for finding stable models of a logic program, the Smodels system, provides the basis of a prefix based model checking procedure for deadlock and reachability properties, which is competitive with previously published procedures using prefixes. This work shows that, if the only thing one can assume from a prefix is that it is complete, nested reachability properties are relatively hard. Namely, for several widely used temporal logics which can express a violation of a certain fixed safety property, model checking is PSPACE-complete in the size of the complete finite prefix. A model checking approach is devised for the linear temporal logic LTL-X using complete finite prefixes. The approach makes the complete finite prefix generation formula specific, and the prefix completeness notion application specific. Using these ideas, an LTL-X model checker has been implemented as a variant of a prefix generation algorithm. The use of bounded model checking for asynchronous systems is studied. A method to express the process semantics of a 1-safe Petri net in symbolic form as a set of satisfying truth assignments of a constrained Boolean circuit is presented. In the experiments the BCSat system is used as a circuit satisfiability checker. Another contribution employs logic programs with stable model semantics to develop a new linear size bounded LTL-X model checking translation that can be used with step semantics of 1-safe Petri nets.
verification, model checking, Petri nets, complete finite prefixes, partial order methods, symbolic methods, bounded model checking
Other note
  • K. Heljanko: Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets, Fundamenta Informaticae 37(3):247-268, 1999. [article1.pdf] © 1999 IOS Press. By permission.
  • K. Heljanko: Model checking with finite complete prefixes is PSPACE-complete, in Proceedings of the 11th International Conference on Concurrency Theory (CONCUR'2000), State College, Pennsylvania, USA, August 2000, volume 1877 of Lecture Notes in Computer Science, pages 108-122. [article2.pdf] © 2000 Springer-Verlag. By permission.
  • J. Esparza, K. Heljanko: A new unfolding approach to LTL model checking, in Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP'2000), Geneva, Switzerland, July 2000, volume 1853 of Lecture Notes in Computer Science, pages 475-486. [article3.pdf] © 2000 Springer-Verlag. By permission.
  • J. Esparza, K. Heljanko: Implementing LTL model checking with net unfoldings, in Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN'2001), Toronto, Canada, May 2001, volume 2057 of Lecture Notes in Computer Science, pages 37-56. [article4.pdf] © 2001 Springer-Verlag. By permission.
  • K. Heljanko: Bounded reachability checking with process semantics, in Proceedings of the 12th International Conference on Concurrency Theory (CONCUR'2001), Aalborg, Denmark, August 2001, volume 2154 of Lecture Notes in Computer Science, pages 218-232. [article5.pdf] © 2001 Springer-Verlag. By permission.
  • K. Heljanko, I. Niemelä: Bounded LTL model checking with stable models, in Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'2001), Vienna, Austria, September 2001, volume 2173 of Lecture Notes in Artificial Intelligence, pages 200-212. [article6.pdf] © 2001 Springer-Verlag. By permission.
Permanent link to this item