@inproceedings{
    Heljanko:CSP98,
    editor = "Burkhard, H.-D. and Czaja, L. and Starke, P.",
    author = "Heljanko, Keijo",
    publisher = "Humboldt-University, Berlin",
    title = "Deadlock Checking for Complete Finite Prefixes Using Logic Programs with Stable Model Semantics ({E}xtended Abstract)",
    url = "http://users.ics.tkk.fi/kepa/publications/",
    series = "Informatik-Bericht Nr. 110",
    booktitle = "Proceedings of the Workshop Concurrency, Specification & Programming 1998",
    year = "1998",
    abstract = {McMillan has presented a deadlock detection method based on complete finite prefixes (i.e., net unfoldings) of a Petri net. The problem of checking deadlock-freedom is NP-complete in the size of the prefix. McMillan originally suggested a branch-and-bound algorithm for deadlock detection in prefixes. Recently, Melzer and R{\"o}mer have presented another algorithm which is based on solving mixed integer programming problems. We show that instead of using mixed integer programming, a constraint-based logic programming framework can be employed, and present a simple linear-size translation from deadlock detection in prefixes into the problem of finding a stable model of a logic program. We present experimental results from a straightforward prototype implementation combining the prefix generator of the PEP-tool, the translation, and an implementation of constraint-based logic programing framework, the Smodels system. We find our approach competitive with the previous approaches.},
    month = "September",
    juforank = "NA",
    flags = "SA-IN-98-01",
    address = "Berlin, Germany",
    keywords = "Petri nets, verification, deadlocks, net unfoldings, prefixes, logic programming",
    pages = "106--115"
}