Deadlock and Reachability Checking with Finite Complete Prefixes

摘要

McMillan has presented a verification method for finite-state Petri nets based on211u001efinite complete prefixes of net unfoldings. Computational complexity of using 211u001efinite complete prefixes as a symbolic representation of the state space is 211u001ediscussed. In addition a novel way of deadlock and reachability checking using 211u001ethe finite complete prefix approach is devised. More specifically, the main 211u001econtributions are: (1) The possible extensions calculation subroutine of the 211u001eprefix generation algorithm is proved NP-complete. (2) Model checking a fixed 211u001esize CTL formula with finite complete prefixes is proved PSPACE-complete. (3) The 211u001etranslations of the problems of deadlock and reachability checking using finite 211u001ecomplete prefixes into the problem of finding a stable model of a logic program 211u001eare devised. (4) The implementation of the above mentioned translations in the 211u001emosmodels tool is presented, with experimental results supporting the feasibility 211u001eof the approach.