Research Report A56: Deadlock and Reachability Checking with Finite Complete Prefixes

Author: Keijo Heljanko

Date: Dec 1999

Pages: 70

McMillan has presented a verification method for finite-state Petri nets based on finite complete prefixes of net unfoldings. Computational complexity of using finite complete prefixes as a symbolic representation of the state space is discussed. In addition a novel way of deadlock and reachability checking using the finite complete prefix approach is devised.

More specifically, the main contributions are: (i) The possible extensions calculation subroutine of the prefix generation algorithm is proved NP-complete. (ii) Model checking a fixed size CTL formula with finite complete prefixes is proved PSPACE-complete. (iii) The translations of the problems of deadlock and reachability checking using finite complete prefixes into the problem of finding a stable model of a logic program are devised. (iv) The implementation of the above mentioned translations in the {\tt mcsmodels} tool is presented, with experimental results supporting the feasibility of the approach.

The implementation combines the prefix generator of the PEP-tool, the translations, and an implementation of a constraint-based logic programming framework, the {\tt smodels} system. The experiments show that the proposed approach is quite competitive when compared to previous prefix based deadlock checking algorithms.

Keywords: Computer aided verification, Petri nets, finite complete prefixes, net unfoldings, model checking, deadlocks, reachability, logic programs, stable model semantics, computational complexity

Full report in Postscript