Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri Nets

• Autorzy: Heljanko K.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

verification; Petri net; logic programs; deadlock checking; reachability

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 1999
• Tom: Vol. 37, Nr 3
• Strony: 247--268
• Opis fizyczny: bibliogr. 20 poz.

Twórcy

autor

Heljanko K.

• Laboratory for Theoretical Computer Science Helsinki University of Technology P.O. Box 5400, 02015 HUT, Finland,