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