I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - Model checking using net unfoldings


J. Esparza. Model checking using net unfoldings. Science of Computer Programming, 23:151–195, 1994.


McMillan (1992) described a technique for deadlock detection based on net unfoldings. We extend its applicability to the properties of a temporal logic with a possibility operator. The new algorithm is shown to be polynomial in the size of the net for 1-safe conflict free Petri nets, while the algorithms of the literature require exponential time.

Suggested BibTeX entry:

    author = {J. Esparza},
    journal = {Science of Computer Programming},
    pages = {151--195},
    title = {Model checking using net unfoldings},
    volume = {23},
    year = {1994}

This work is not available online here.