Reference:

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

Abstract:

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:

@article{ERV01,
    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}
}