Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - An Improvement of McMillan's Unfolding Algorithm


J. Esparza, S. Römer, and W. Vogler. An improvement of McMillan's unfolding algorithm. Formal Methods in System Design, 20:285–310, 2002.


McMillan has proposed a new technique to avoid the state explosion problem in the verification of systems modelled with finite-state Petri nets. The technique requires to construct a finite initial part of the unfolding of the net. McMillan's algorithm for this task may yield initial parts that are larger than necessary (exponentially larger in the worst case). We present a refinement of the algorithm which overcomes this problem.

Suggested BibTeX entry:

    author = {J. Esparza and S. R{\"o}mer and W. Vogler},
    journal = {Formal Methods in System Design},
    pages = {285--310},
    title = {An Improvement of {McMillan's} Unfolding Algorithm},
    volume = {20},
    year = {2002}

GZipped PostScript (149 kB)
PDF (351 kB)
Conference version