Reference:
Keijo Heljanko. Deadlock and reachability checking with finite complete prefixes. Research Report A56, Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science, Espoo, Finland, December 1999.
Abstract:
McMillan has presented a verification method for finitestate 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 NPcomplete. (ii) Model checking a fixed size CTL formula with finite complete prefixes is proved PSPACEcomplete. (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 mcsmodels tool is presented, with experimental results supporting the feasibility of the approach.
The implementation combines the prefix generator of the PEPtool, the translations, and an implementation of a constraintbased logic programming framework, the 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
Suggested BibTeX entry:
@techreport{HUTTCSA56,
address = {Espoo, Finland},
author = {Keijo Heljanko},
institution = {Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science},
month = {December},
number = {A56},
pages = {70},
title = {Deadlock and Reachability Checking with Finite Complete Prefixes},
type = {Research Report},
year = {1999},
}
