Deadlock and Reachability Checking with Finite Complete Prefixes

Reference:

Keijo Heljanko. Deadlock and Reachability Checking with Finite Complete Prefixes. Licentiate's thesis, Helsinki University of Technology, Department of Computer Science and Engineering, Espoo, Finland, December 1999. Also available as: Series A: Research Report 56, Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science.

Abstract:

Net unfoldings are a partial order semantics for Petri nets. 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.

Keywords:

verification, Petri nets, unfoldings, logic programs, computational complexity, deadlocks, reachability

Suggested BibTeX entry:

@phdthesis{Heljanko:licthesis,
    address = {Espoo, Finland},
    author = {Keijo Heljanko},
    month = {December},
    note = {Also available as: Series A: Research Report 56, Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science.},
    pages = {70},
    school = {Helsinki University of Technology, Department of Computer Science and Engineering},
    title = {Deadlock and Reachability Checking with Finite Complete Prefixes},
    type = {Licentiate's thesis},
    year = {1999},
}