Czasopismo
1999
|
Vol. 37, Nr 3
|
247-268
Tytuł artykułu
Autorzy
Wybrane pełne teksty z tego czasopisma
Warianty tytułu
Języki publikacji
Abstrakty
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
Czasopismo
Rocznik
Tom
Strony
247-268
Opis fizyczny
bibliogr. 20 poz.
Twórcy
autor
- Laboratory for Theoretical Computer Science Helsinki University of Technology P.O. Box 5400, 02015 HUT, Finland, Keijo.Heljanko@hut.fi
Bibliografia
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.baztech-article-BUS1-0007-0016