Reference:
Keijo Heljanko. Using logic programs with stable model semantics to solve deadlock and reachability problems for 1safe Petri nets. In Rance Cleaveland, editor, Proceedings of 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), volume 1579 of Lecture Notes in Computer Science, pages 240–254, Amsterdam, Netherlands, 1999. SpringerVerlag.
Abstract:
McMillan has presented a deadlock detection method for Petri nets based on finite complete prefixes (i.e., net unfoldings). The basic idea is to transform the PSPACEcomplete deadlock detection problem for a 1safe Petri net into a potentially exponentially larger NPcomplete problem of deadlock detection for a finite complete prefix. McMillan suggested a branchandbound 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 constraintbased logic programming framework can be employed, and a linearsize translation from deadlock detection 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. Experimental results are given from an implementation combining the prefix generator of the PEPtool, the translation, and an implementation of a constraintbased logic programming framework, the Smodels system. The experiments show the proposed approach to be quite competitive, when compared to the approaches of McMillan and Melzer/Römer.
Keywords:
verification, Petri nets, logic programs, deadlocks, reachability
Suggested BibTeX entry:
@inproceedings{Heljanko:Tacas99,
address = {Amsterdam, Netherlands},
author = {Keijo Heljanko},
booktitle = {Proceedings of 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99)},
editor = {Rance Cleaveland},
pages = {240254},
publisher = {SpringerVerlag},
series = {Lecture Notes in Computer Science},
title = {Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1Safe {Petri} Nets},
volume = {1579},
year = {1999},
}
