Robust parametric reachability for timed automata

被引：30
|
作者：
Doyen, Laurent
机构：
[1] School of Computer and Communication Sciences, Swiss Federal Institute of Technology (EPFL)
来源：
INFORMATION PROCESSING LETTERS | 2007年 / 102卷 / 05期
关键词：
parametric timed automata; real-time systems; formal methods; model checking; theory of computation; robustness; verification;
D O I：
10.1016/j.ipl.2006.11.018
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
We review the known decidability and undecidability results for reachability in parametric timed automata. Then, we present a new proof of undecidability in dense time for open timed automata that avoids equalities in clock constraints. Our result shows that the undecidability of parametric timed automata does not follow from their ability to specify punctual constraints in a dense time domain. (c) 2006 Elsevier B.V. All rights reserved.
引用
收藏
页码：208 / 213
页数：6
相关论文
共 50 条
  • [1] REACHABILITY AND LIVENESS IN PARAMETRIC TIMED AUTOMATA
    Andre, Etienne
    Lime, Didier
    Roux, Olivier H.
    LOGICAL METHODS IN COMPUTER SCIENCE, 2020, 18 (01)
  • [2] Control synthesis for parametric timed automata under reachability
    Gol, Ebru A. Y. D. I. N.
    TURKISH JOURNAL OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCES, 2021, 29 (03) : 1751 - 1764
  • [3] Robust reachability in timed automata and games: A game-based approach
    Bouyer, Patricia
    Markey, Nicolas
    Sankur, Ocan
    THEORETICAL COMPUTER SCIENCE, 2015, 563 : 43 - 74
  • [4] Revisiting Reachability in Timed Automata
    Quaas, Karin
    Shirmohammadi, Mahsa
    Worrell, James
    2017 32ND ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2017,
  • [5] Reachability in Two-Parametric Timed Automata with one Parameter is EXPSPACE-Complete
    Goeller, Stefan
    Hilaire, Mathieu
    THEORY OF COMPUTING SYSTEMS, 2024, 68 (04) : 900 - 985
  • [6] Reachability in Two-Parametric Timed Automata with One Parameter Is EXPSPACE-Complete
    Goeller, Stefan
    Hilaire, Mathieu
    38TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE (STACS 2021), 2021, 187
  • [7] PARAMETRIC UPDATES IN PARAMETRIC TIMED AUTOMATA
    Andre, Etienne
    Lime, Didier
    Ramparison, Mathias
    LOGICAL METHODS IN COMPUTER SCIENCE, 2021, 17 (02) : 13:1 - 13:67
  • [8] Distributed reachability analysis in timed automata
    Behrmann G.
    International Journal on Software Tools for Technology Transfer, 2005, 7 (1) : 19 - 30
  • [9] Symbolic and Compositional Reachability for Timed Automata
    Larsen, Kim Guldstrand
    REACHABILITY PROBLEMS, 2010, 6227 : 24 - 28
  • [10] Reachability relations of timed pushdown automata
    Clemente, Lorenzo
    Lasota, Slawomir
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2021, 117 : 202 - 241
12345