Deadlock and Reachability Checking with Finite Complete Prefixes
Keijo Heljanko · 1999
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 novel way of deadlock and reachability checking using the net unfolding approach is devised. More specifically, the main contributions are: (i) A proof of NP-completeness of a subroutine of the finite complete prefix generation algorithm. (ii) A proof of PSPACE-completeness of model checking with finite complete prefixes. (iii) Translations of the problems of deadlock and reachability checking into the problem of finding a stable model of a logic program. (iv) An implementation of the translations in the mcsmodels tool, 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 Smodels system. The experiments show that the proposed approach is quite competitive when compared to previous finite complete prefix based deadlock checking algorithms.