An improvement of McMillan’s unfolding algorithm

Javier Esparza, Stefan Römer, Walter Vogler

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

131 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
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 2nd International Workshop, TACAS 1996, Proceedings
EditorsTiziana Margaria, Bernhard Steffen
PublisherSpringer Verlag
Pages87-106
Number of pages20
ISBN (Print)3540610421, 9783540610427
DOIs
StatePublished - 1996
Event2nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1996 - Passau, Germany
Duration: 27 Mar 199629 Mar 1996

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1055
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference2nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1996
Country/TerritoryGermany
CityPassau
Period27/03/9629/03/96

Fingerprint

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

Cite this