@article{
    Heljanko:Fundamenta99,
    author = "Heljanko, Keijo",
    publisher = "IOS Press",
    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/",
    journal = "Fundamenta Informaticae",
    number = "3",
    abstract = {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 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 devised 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. Correctness proofs of both the translations are presented. 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 = "37",
    juforank = "2",
    flags = "SA-IN-98-01",
    year = "1999",
    keywords = "verification, Petri nets, logic programs, deadlocks, reachability",
    pages = "247--268"
}