An improvement of McMillan's unfolding algorithm

被引：173

作者：

Esparza, J

Römer, S

Vogler, W

机构：

[1] Tech Univ Munich, Inst Informat, D-80333 Munich, Germany

[2] Univ Augsburg, Inst Informat, D-86159 Augsburg, Germany

来源：

FORMAL METHODS IN SYSTEM DESIGN | 2002年 / 20卷 / 03期

关键词：

unfolding; partial-order semantics; Petri nets;

D O I：

10.1023/A:1014746130920

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：285 / 310

页数：26

共 19 条

[1]

Best Eike, 1988, EATCS MONOGRAPHS THE, V13

[2]

CORBETT JC, 1994, P 1994 INT S SOFTW T, P204

[3]

DIEKERT V, 1990, LNCS, V454

[4] BRANCHING-PROCESSES OF PETRI NETS [J].

ENGELFRIET, J .

ACTA INFORMATICA, 1991, 28 (06) :575-591

[5] MODEL CHECKING USING NET UNFOLDINGS [J].

ESPARZA, J .

SCIENCE OF COMPUTER PROGRAMMING, 1994, 23 (2-3) :151-195

[6]

ESPARZA J, 1996, LNCS, V1055, P87

[7]

HAAR S, 1998, WORKSH CONC SPEC PRO, V10, P88

[8]

KISHINEVSKY M, 1993, CONCURRENT HARDWARE

[9]

KONDRATYEV A, 1994, P S ADV RES AS CIRC

[10]

MARTIN AJ, 1985, CHAP HILL C VLSI, P245

← 1 2 →