Fundamental structures in well-structured infinite transition systems

被引：18
作者：
Finkel, A
Schnoebelen, P
机构：
[1] ENS Cachan, Lab Specificat & Verificat, F-94235 Cachan, France
[2] CNRS, URA 2236, F-94235 Cachan, France
来源：
LATIN '98: THEORETICAL INFORMATICS | 1998年 / 1380卷
关键词：
D O I：
10.1007/BFb0054314
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We suggest a simple and clean definition for Well-Structured Transition Systems [20, 1], a general class of infinite state systems for which decidability results exist. As a consequence we can (1) generalize the definition in many ways, (2) find examples of (general) WSTS's in many fields, and (3) present new decidability results.
引用
收藏
页码：102 / 118
页数：17
相关论文
共 30 条
[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, 1994, LECT NOTES COMPUTER, V280, P316
[4]  
ABDULLA PA, 1997, METHODS TOOLS VERIFI
[5]  
[Anonymous], 1993, LECT NOTES COMP SCI
[6]  
BAETEN JCM, 1987, LECT NOTES COMPUT SC, V259, P94
[7]  
BONCHATBONRAT A, 1894, P 3 INT C THEOR CRIM
[8]   CHARACTERIZING FINITE KRIPKE STRUCTURES IN PROPOSITIONAL TEMPORAL LOGIC [J].
BROWNE, MC ;
CLARKE, EM ;
GRUMBERG, O .
THEORETICAL COMPUTER SCIENCE, 1988, 59 (1-2) :115-131
[9]   SYMBOLIC MODEL CHECKING - 1020 STATES AND BEYOND [J].
BURCH, JR ;
CLARKE, EM ;
MCMILLAN, KL ;
DILL, DL ;
HWANG, LJ .
INFORMATION AND COMPUTATION, 1992, 98 (02) :142-170
[10]   Unreliable channels are easier to verify than perfect channels [J].
Cece, G ;
Finkel, A ;
Iyer, SP .
INFORMATION AND COMPUTATION, 1996, 124 (01) :20-31
123