@phdthesis{
    Heljanko:licthesis,
    author = "Heljanko, Keijo",
    juforank = "NA",
    school = "Helsinki University of Technology, Department of Computer Science and Engineering",
    title = "Deadlock and Reachability Checking with Finite Complete Prefixes",
    url = "http://www.tcs.hut.fi/Publications/reports/A56abstract.html",
    abstract = "Net unfoldings are a partial order semantics for Petri nets. McMillan has presented a verification method for finite-state Petri nets based on finite complete prefixes of net unfoldings. Computational complexity of using finite complete prefixes as a symbolic representation of the state space is discussed. In addition novel way of deadlock and reachability checking using the net unfolding approach is devised. More specifically, the main contributions are: (i) A proof of NP-completeness of a subroutine of the finite complete prefix generation algorithm. (ii) A proof of PSPACE-completeness of model checking with finite complete prefixes. (iii) Translations of the problems of deadlock and reachability checking into the problem of finding a stable model of a logic program. (iv) An implementation of the translations in the mcsmodels tool, with experimental results supporting the feasibility of the approach. The implementation combines the prefix generator of the PEP-tool, the translations, and an implementation of a constraint-based logic programming framework, the Smodels system. The experiments show that the proposed approach is quite competitive when compared to previous finite complete prefix based deadlock checking algorithms.",
    address = "Espoo, Finland",
    month = "December",
    note = "Also available as: Series A: Research Report 56, Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science.",
    flags = "copy SA-IN-98-01",
    year = "1999",
    keywords = "verification, Petri nets, unfoldings, logic programs, computational complexity, deadlocks, reachability",
    type = "Licentiate's thesis",
    pages = "70"
}