An improvement of McMillan's unfolding algorithm

Javier Esparza, Stefan Römer, Walter Vogler

Research output: Contribution to journalArticlepeer-review

220 Scopus citations

Abstract

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
Volume20
Issue number3
DOIs
StatePublished - May 2002

Keywords

  • Partial-order semantics
  • Petri nets
  • Unfolding

Fingerprint

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

Cite this