An undecidable problem for timed automata

被引:4
|
作者
Puri, A [1 ]
机构
[1] AT&T Bell Labs, Murray Hill, NJ 07974 USA
关键词
timed systems; hybrid systems; decidability;
D O I
10.1023/A:1008319830371
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
The reachability problem for timed automata is decidable when the coefficients in the guards are rational numbers. We show that the reachability problem is undecidable when the coefficients are chosen from the set {1, root 2}. A consequence of this is that the parameter synthesis problem for timed automata with even a single parameter is undecidable. We discuss why such undecidability results arise in timed and hybrid systems, what they mean, and if it is possible to "get around" them.
引用
收藏
页码:135 / 146
页数:12
相关论文
共 50 条
  • [1] Undecidable problem for timed automata
    Bell Laboratories, Murray Hill, NJ 07974, United States
    Discrete Event Dyn Syst Theory Appl, 2 (135-146):
  • [2] An Undecidable Problem for Timed Automata
    Anuj Puri
    Discrete Event Dynamic Systems, 1999, 9 : 135 - 146
  • [3] Undecidable problems about timed automata
    Finkel, Olivier
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2006, 4202 : 187 - 199
  • [4] Decidable and undecidable problems in schedulability analysis using timed automata
    Krcál, P
    Yi, W
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2004, 2988 : 236 - 250
  • [5] MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable
    Quaas, Karin
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (145): : 5 - 17
  • [6] The Containment Problem for Unambiguous Register Automata and Unambiguous Timed Automata
    Antoine Mottet
    Karin Quaas
    Theory of Computing Systems, 2021, 65 : 706 - 735
  • [7] The Containment Problem for Unambiguous Register Automata and Unambiguous Timed Automata
    Mottet, Antoine
    Quaas, Karin
    THEORY OF COMPUTING SYSTEMS, 2021, 65 (04) : 706 - 735
  • [8] On the optimal reachability problem of weighted timed automata
    Bouyer, Patricia
    Brihaye, Thomas
    Bruyere, Veronique
    Raskin, Jean-Francois
    FORMAL METHODS IN SYSTEM DESIGN, 2007, 31 (02) : 135 - 175
  • [9] On the optimal reachability problem of weighted timed automata
    Patricia Bouyer
    Thomas Brihaye
    Véronique Bruyère
    Jean-François Raskin
    Formal Methods in System Design, 2007, 31 : 135 - 175
  • [10] The language preservation problem is undecidable for parametric event-recording automata
    Andre, Etienne
    Lin, Shang-Wei
    INFORMATION PROCESSING LETTERS, 2018, 136 : 17 - 20