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 条
  • [41] Alternating timed automata
    Lasota, S
    Walukiewicz, I
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2005, 3441 : 250 - 265
  • [42] On Simplification of Timed Automata
    Gromov, Maxim
    PROCEEDINGS OF 2016 IEEE EAST-WEST DESIGN & TEST SYMPOSIUM (EWDTS), 2016,
  • [43] Calculus for timed automata
    D'Argenio, P.R.
    Brinksma, E.
    1996, (1135)
  • [44] Recursive Timed Automata
    Trivedi, Ashutosh
    Wojtczak, Dominik
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, 2010, 6252 : 306 - 324
  • [45] Timed P Automata
    Barbuti, Roberto
    Maggiolo-Schettini, Andrea
    Milazzo, Paolo
    Tesei, Luca
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 227 : 21 - 36
  • [46] Interrupt Timed Automata
    Berard, Beatrice
    Haddad, Serge
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS, 2009, 5504 : 197 - +
  • [47] IMITATOR II: A Tool for Solving the Good Parameters Problem in Timed Automata
    Andre, Etienne
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2010, (39): : 91 - 99
  • [48] A partial order semantics approach to the clock explosion problem of timed automata
    Lugiez, D
    Niebert, P
    Zennou, S
    THEORETICAL COMPUTER SCIENCE, 2005, 345 (01) : 27 - 59
  • [49] Shrinking Timed Automata
    Sankur, Ocan
    Bouyer, Patricia
    Markey, Nicolas
    IARCS ANNUAL CONFERENCE ON FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE (FSTTCS 2011), 2011, 13 : 90 - 102
  • [50] Diagnosis of timed automata: Theory and application to the DAMADICS actuator benchmark problem
    Supavatanakul, P
    Lunze, J
    Puig, V
    Quevedo, J
    CONTROL ENGINEERING PRACTICE, 2006, 14 (06) : 609 - 619