Well-structured transition systems everywhere!

被引：438
作者：
Finkel, A
Suhnoebelen, P
机构：
[1] ENS Cachan, Lab Specificat & Verificat, F-94235 Cachan, France
[2] CNRS UMR 8643, F-94235 Cachan, France
来源：
THEORETICAL COMPUTER SCIENCE | 2001年 / 256卷 / 1-2期
关键词：
infinite systems; verification; well-quasi-ordering;
D O I：
10.1016/S0304-3975(00)00102-X
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Well-structured transition systems (WSTSs) are a general class of infinite-state systems for which decidability results rely on the existence of a well-quasi-ordering between states that is compatible with the transitions. In this article, we provide an extensive treatment of the WSTS idea and show several new results. Our improved definitions allow many examples of classical systems to be seen as instances of WSTSs. (C) 2001 Elsevier Science B.V. All rights reserved.
引用
收藏
页码：63 / 92
页数：30
相关论文
共 62 条
[1]  
Abdulla P., 1993, Proceedings of Eighth Annual IEEE Symposium on Logic in Computer Science (Cat. No.93CH3328-2), P160, DOI 10.1109/LICS.1993.287591
[2]   General decidability theorems for infinite-state systems [J].
Abdulla, PA ;
Cerans, K ;
Jonsson, B ;
Tsay, YK .
11TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1996, :313-321
[3]  
Abdulla PA, 1998, LECT NOTES COMPUT SC, V1384, P298, DOI 10.1007/BFb0054179
[4]   Ensuring completeness of symbolic verification methods for infinite-state systems [J].
Abdulla, PA ;
Jonsson, B .
THEORETICAL COMPUTER SCIENCE, 2001, 256 (1-2) :145-167
[5]  
ABDULLA PA, IN PRESS INFORM COMP
[6]  
ABDULLA PA, 2000, BQOS TIMED PETRI NET
[7]  
ABDULLA PA, 1994, LECT NOTES COMPUTER, V820, P316
[8]  
ABDULLA PA, 2000, P 15 IEEE S LOG COMP
[9]   A THEORY OF TIMED AUTOMATA [J].
ALUR, R ;
DILL, DL .
THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235
[10]  
Araki T., 1976, Theoretical Computer Science, V3, P85, DOI 10.1016/0304-3975(76)90067-0
1234567