Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets

Reference:

Keijo Heljanko. Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe 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. Springer-Verlag.

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 PSPACE-complete deadlock detection problem for a 1-safe Petri net into a potentially exponentially larger NP-complete problem of deadlock detection for a finite complete prefix. McMillan suggested 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 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 PEP-tool, the translation, and an implementation of a constraint-based 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 = {240--254},
    publisher = {Springer-Verlag},
    series = {Lecture Notes in Computer Science},
    title = {Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe {Petri} Nets},
    volume = {1579},
    year = {1999},
}