Deadlock Checking for Complete Finite Prefixes Using Logic Programs with Stable Model Semantics (Extended Abstract)

Reference:

Keijo Heljanko. Deadlock checking for complete finite prefixes using logic programs with stable model semantics (Extended abstract). In H.-D. Burkhard, L. Czaja, and P. Starke, editors, Proceedings of the Workshop Concurrency, Specification & Programming 1998, Informatik-Bericht Nr. 110, pages 106–115, Berlin, Germany, September 1998. Humboldt-University, Berlin.

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ö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.

Keywords:

Petri nets, verification, deadlocks, net unfoldings, prefixes, logic programming

Suggested BibTeX entry:

@inproceedings{Heljanko:CSP98,
    address = {Berlin, Germany},
    author = {Keijo Heljanko},
    booktitle = {Proceedings of the Workshop Concurrency, Specification & Programming 1998},
    editor = {H.-D. Burkhard and L. Czaja and P. Starke},
    month = {September},
    pages = {106--115},
    publisher = {Humboldt-University, Berlin},
    series = {Informatik-Bericht Nr. 110},
    title = {Deadlock Checking for Complete Finite Prefixes Using Logic Programs with Stable Model Semantics ({E}xtended Abstract)},
    year = {1998},
}