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 条
[31]   Pareto Optimal Reachability Analysis for Simple Priced Timed Automata [J].
Zhang, Zhengkui ;
Nielsen, Brian ;
Larsen, Kim Guldstrand ;
Nies, Gilles ;
Stenger, Marvin ;
Hermanns, Holger .
FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2017, 2017, 10610 :481-495
[32]   Revisiting Bounded Reachability Analysis of Timed Automata Based on MILP [J].
Ober, Iulian .
FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2018, 2018, 11119 :269-283
[33]   Decision problems for lower/upper bound parametric timed automata [J].
Bozzelli, Laura ;
La Torre, Salvatore .
FORMAL METHODS IN SYSTEM DESIGN, 2009, 35 (02) :121-151
[34]   Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata [J].
Jovanovic, Aleksandra ;
Kwiatkowska, Marta ;
Norman, Gethin ;
Peyras, Quentin .
THEORETICAL COMPUTER SCIENCE, 2017, 669 :1-21
[35]   Parametric non-interference in timed automata [J].
Andre, Etienne ;
Kryukov, Aleksander .
2020 25TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2020), 2020, :37-42
[36]   Controlling Actions and Time in Parametric Timed Automata [J].
Andre, Etienne ;
Knapik, Michal ;
Penczek, Wojciech ;
Petrucci, Laure .
2016 16TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN (ACSD 2016), 2016, :45-54
[37]   LTL Parameter Synthesis of Parametric Timed Automata [J].
Bezdek, Peter ;
Benes, Nikola ;
Barnat, Jiri ;
Cerna, Ivana .
SOFTWARE ENGINEERING AND FORMAL METHODS: 14TH INTERNATIONAL CONFERENCE, SEFM 2016, 2016, 9763 :172-187
[38]   On the expressive power of invariants in parametric timed automata [J].
Andre, Etienne ;
Lime, Didier ;
Ramparison, Mathias .
2019 24TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2019), 2019, :87-96
[39]   A Benchmarks Library for Extended Parametric Timed Automata [J].
Andre, Etienne ;
Marinho, Dylan ;
van de Pol, Jaco .
TESTS AND PROOFS (TAP 2021), 2021, 12740 :39-50
[40]   TREAT: Timed REachability Analysis Tool [J].
Kang, I .
INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS I-V, PROCEEDINGS, 1999, :586-591
12345