Well-structured transition systems everywhere!

被引:432
作者
Finkel, A
Suhnoebelen, P
机构
[1] ENS Cachan, Lab Specificat & Verificat, F-94235 Cachan, France
[2] CNRS UMR 8643, F-94235 Cachan, France
关键词
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
相关论文
共 50 条
  • [31] Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach
    Zhang, Kuize
    Yin, Xiang
    Zamani, Majid
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2019, 64 (12) : 5116 - 5123
  • [32] A Deductive Approach towards Reasoning about Algebraic Transition Systems
    Fu, Jun
    Wu, Jinzhao
    Tan, Hongyan
    MATHEMATICAL PROBLEMS IN ENGINEERING, 2015, 2015
  • [33] An efficient algorithm for minimizing real-time transition systems
    Yannakakis, M
    Lee, D
    FORMAL METHODS IN SYSTEM DESIGN, 1997, 11 (02) : 113 - 136
  • [34] Logical Characterizations of Behavioral Relations on Transition Systems of Probability Distributions
    Crafa, Silvia
    Ranzato, Francesco
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2015, 16 (01)
  • [35] Invariant-preserving transformations for the verification of place/transition systems
    Cheung, TY
    Zeng, W
    IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 1998, 28 (01): : 114 - 121
  • [36] An Efficient Algorithm for Minimizing Real-Time Transition Systems
    Mihalis Yannakakis
    David Lee
    Formal Methods in System Design, 1997, 11 : 113 - 136
  • [37] Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking
    Classen, Andreas
    Cordy, Maxime
    Schobbens, Pierre-Yves
    Heymans, Patrick
    Legay, Axel
    Raskin, Jean-Francois
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2013, 39 (08) : 1069 - 1089
  • [38] Optimal Temporal Logic Control for Deterministic Transition Systems With Probabilistic Penalties
    Svorenova, Maria
    Cerna, Ivana
    Belta, Calin
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2015, 60 (06) : 1528 - 1541
  • [39] Automatic Discovery of Fair Paths in Infinite-State Transition Systems
    Cimatti, Alessandro
    Griggio, Alberto
    Magnago, Enrico
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2021, 2021, 12971 : 32 - 47
  • [40] An approximation algorithm for box abstraction of transition systems on real state spaces
    Hiraishi, Kunihiko
    Kobayashi, Koich
    FORMAL METHODS IN SYSTEM DESIGN, 2013, 42 (02) : 175 - 192