McMillan has presented a deadlock detection method for Petri nets based on finite complete prefixes (i.e. net unfoldings). The approach transforms the PSPACE-complete deadlock detec-tion problem for a 1-safe Petri net into a potentially exponentially larger NP-complete prob-lem of deadlock detection for a finite complete prefix. McMillan devised a branch-and-bound algorithm for deadlock detection in prefixes. Recently, Melzer and Römer have presented another approach, which is based on solving mixed integer programming problems. In this work it is shown that instead of using mixed integer programming, a constraint-based logic programming framework can be employed, and a linear-size, translation from deadlock detec-tion in prefixes into the problem of finding a stable model of a logic program is presented. As a side result also such a translation for solving the reachability problem is devised. Correct-ness proofs of both the translations are presented. Experimental results are given from an im-plementation combining the prefix generator of the PEP-tool, the translation, and an imple-mentation of a constraint-based logic programming framework, the smodels system. The ex-periments show the proposed approach to be quite competitive, when compared to the ap-proaches of McMillan and Melzer/Römer.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.