@inproceedings{
    Heljanko:Tacas99,
    editor = "Cleaveland, Rance",
    author = "Heljanko, Keijo",
    publisher = "Springer-Verlag",
    title = "Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe {Petri} Nets",
    url = "http://users.ics.tkk.fi/kepa/publications/",
    series = "Lecture Notes in Computer Science",
    booktitle = "Proceedings of 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99)",
    address = "Amsterdam, Netherlands",
    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{\"o}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{\"o}mer.},
    volume = "1579",
    juforank = "1",
    flags = "SA-IN-98-01",
    year = "1999",
    keywords = "verification, Petri nets, logic programs, deadlocks, reachability",
    pages = "240--254"
}