An improvement of McMillan's unfolding algorithm

Javier Esparza, Stefan Römer, Walter Vogler

Research output: Contribution to journalArticlepeer-review

220 Scopus citations


McMillan has recently 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.

Original languageEnglish
Pages (from-to)285-310
Number of pages26
JournalFormal Methods in System Design
Issue number3
StatePublished - May 2002


  • Partial-order semantics
  • Petri nets
  • Unfolding


Dive into the research topics of 'An improvement of McMillan's unfolding algorithm'. Together they form a unique fingerprint.

Cite this