The doctoral dissertations of the former Helsinki University of Technology (TKK) and Aalto University Schools of Technology (CHEM, ELEC, ENG, SCI) published in electronic format are available in the electronic publications archive of Aalto University - Aaltodoc.
Aalto

Combining Symbolic and Partial Order Methods for Model Checking 1-Safe Petri Nets

Keijo Heljanko

Dissertation for the degree of Doctor of Science in Technology to be presented with due permission of the Department of Computer Science and Engineering, for public examination and debate in Auditorium T2 at Helsinki University of Technology (HUT CS building, Espoo, Finland) on the 22nd of March, 2002, at 12 noon.

Overview in PDF format (ISBN 951-22-5893-5)   [579 KB]
Dissertation is also available in print (ISBN 951-22-5886-2)

Abstract

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.

This thesis consists of an overview and of the following 6 publications:

  1. 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. © 1999 IOS Press. By permission.
  2. 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. © 2000 Springer-Verlag. By permission.
  3. 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. © 2000 Springer-Verlag. By permission.
  4. 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. © 2001 Springer-Verlag. By permission.
  5. 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. © 2001 Springer-Verlag. By permission.
  6. 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. © 2001 Springer-Verlag. By permission.

Keywords: verification, model checking, Petri nets, complete finite prefixes, partial order methods, symbolic methods, bounded model checking

This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.

© 2002 Helsinki University of Technology

Last update 2011-05-26