REDUCTION AND COVERING OF INFINITE REACHABILITY TREES

被引：52
作者：
FINKEL, A
机构：
[1] RES CTR COMP SCI MONTREAL, MONTREAL, QUEBEC, CANADA
[2] UNIV MONTREAL, MONTREAL H3C 3J7, QUEBEC, CANADA
来源：
INFORMATION AND COMPUTATION | 1990年 / 89卷 / 02期
关键词：
D O I：
10.1016/0890-5401(90)90009-7
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a structure for transition systems with which the main decidability results on Petri nets can be generalized to structured transition systems. We define the reduced reachability tree of a structured transition system; it allows one to decide the finite reachability tree problem (also called the finite termination problem) and the finite reachability set problem. A general definition of the coverability set is given and the procedure of Karp and Miller is extended for well-structured transition systems. We show then that the coverability problem is a decidable problem in the framework of well-structured transition systems. Finally, we introduce structured set of terminal states and we show that the finite reachability tree problem and the finite reachability set problem are decidable. Coverability is an open problem for structured transition systems with a structured set of terminal states. © 1990.
引用
收藏
页码：144 / 179
页数：36
相关论文
共 33 条
[21]  
KELLER R, 1972, 117 PRINC U TECH REP
[22]   FORMAL VERIFICATION OF PARALLEL PROGRAMS [J].
KELLER, RM .
COMMUNICATIONS OF THE ACM, 1976, 19 (07) :371-384
[23]  
Konig D., 1936, THEORIE ENDLICHEN UN
[24]  
KOSARAJU SR, 1982, 1JTH P ANN ACM S THE
[25]  
KRUSKAL JB, 1972, J COMBIN THEORY A, V13
[26]  
MAYR EW, 1984, SIAM J COMPUTING, V13
[27]  
MEMMI G, 1985, THEORET COMPUT SCI, V35
[28]  
Pachl J., 1987, Protocol Specification, Testing, and Verification, VII. Proceedings of the IFIP WG 6.1 Seventh International Conference, P207
[29]  
PARIGOT M, 1986, COMMUNICATION
[30]  
Peterson J. L., 1981, PETRI NET THEORY MOD
1234