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
    ENGELFRIET, J
    [J]. ACTA INFORMATICA, 1991, 28 (06) : 575 - 591
  • [5] MODEL CHECKING USING NET UNFOLDINGS
    ESPARZA, J
    [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
12