Bounded Reachability Checking with Process Semantics


Keijo Heljanko. Bounded reachability checking with process semantics. In Kim Guldstrand Larsen and Mogens Nielsen, editors, Proceedings of the 12th International Conference on Concurrency Theory (Concur'2001), volume 2154 of Lecture Notes in Computer Science, pages 218–232, Aalborg, Denmark, August 2001. Springer-Verlag.


Bounded model checking has been recently introduced as an efficient verification method for reactive systems. In this work we apply bounded model checking to asynchronous systems. More specifically, we translate the bounded reachability problem for 1-safe Petri nets into constrained Boolean circuit satisfiability. We consider three semantics: process, step, and interleaving semantics. We show that process semantics has often the best performance for bounded reachability checking.


bounded model checking, process semantics, reachability, Petri nets

Suggested BibTeX entry:

    address = {Aalborg, Denmark},
    author = {Keijo Heljanko},
    booktitle = {Proceedings of the 12th International Conference on Concurrency Theory (Concur'2001)},
    editor = {Kim Guldstrand Larsen and Mogens Nielsen},
    month = {August},
    pages = {218--232},
    publisher = {Springer-Verlag},
    series = {Lecture Notes in Computer Science},
    title = {Bounded Reachability Checking with Process Semantics},
    volume = {2154},
    year = {2001},

See ...