MODEL CHECKING USING NET UNFOLDINGS

被引：85

作者：

ESPARZA, J

机构：

[1] UNIV HILDESHEIM, HILDESHEIM, GERMANY

[2] UNIV EDINBURGH, EDINBURGH, MIDLOTHIAN, SCOTLAND

来源：

SCIENCE OF COMPUTER PROGRAMMING | 1994年 / 23卷 / 2-3期

关键词：

D O I：

10.1016/0167-6423(94)00019-0

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

McMillan (1992) described a technique for deadlock detection based on net unfoldings. We extend its applicability to the properties of a temporal logic with a possibility operator. The new algorithm is shown to be polynomial in the size of the net for 1-safe conflict-free Petri nets, while the algorithms of the literature require exponential time.

引用

页码：151 / 195

页数：45

共 41 条

[1]

Andersen H. R., 1992, Computer Aided Verification. 3rd International Workshop CAV '91. Proceedings, P24

[2] THE TEMPORAL LOGIC OF BRANCHING TIME [J].

BENARI, M ;

PNUELI, A ;

MANNA, Z .

ACTA INFORMATICA, 1983, 20 (03) :207-226

[3]

BERNARDINELLO L, 1982, LECTURE NOTES COMPUT, V609, P304

[4]

BEST E, 1992, LECT NOTES COMPUT SC, V626, P35, DOI 10.1007/BFb0023756

[5]

BEST E, 1987, THEORET COMPUT SCI, V55, P299

[6]

Best Eike, 1988, EATCS MONOGRAPHS THE, V13

[7]

BRADFIELD JC, 1991, THESIS U EDINBURGH

[8]

BROWNE M, 1985, IEEE INT C COMPUTER

[9] REASONING ABOUT NETWORKS WITH MANY IDENTICAL FINITE STATE PROCESSES [J].

BROWNE, MC ;

CLARKE, EM ;

GRUMBERG, O .

INFORMATION AND COMPUTATION, 1989, 81 (01) :13-31

[10]

Burch J. R., 1990, P 5 ANN IEEE S LOG C, P428, DOI DOI 10.1109/LICS.1990.113767

← 1 2 3 4 5 →