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 条
[21]   Lazy Reachability Checking for Timed Automata Using Interpolants [J].
Toth, Tamas ;
Majzik, Istvan .
FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS 2017), 2017, 10419 :264-280
[22]   Online Parametric Timed Pattern Matching with Automata-Based Skipping [J].
Waga, Masaki ;
Andre, Etienne .
NASA FORMAL METHODS (NFM 2019), 2019, 11460 :371-389
[23]   Reachability results for timed automata with unbounded data structures [J].
Lanotte, Ruggero ;
Maggiolo-Schettini, Andrea ;
Troina, Angelo .
ACTA INFORMATICA, 2010, 47 (5-6) :279-311
[24]   Robust safety of timed automata [J].
Martin De Wulf ;
Laurent Doyen ;
Nicolas Markey ;
Jean-François Raskin .
Formal Methods in System Design, 2008, 33 :45-84
[25]   Robust safety of timed automata [J].
De Wulf, Martin ;
Doyen, Laurent ;
Markey, Nicolas ;
Raskin, Jean-Francois .
FORMAL METHODS IN SYSTEM DESIGN, 2008, 33 (1-3) :45-84
[26]   An Inverse Method for Parametric Timed Automata [J].
Andre, Etienne ;
Chatain, Thomas ;
Fribourg, Laurent ;
Encrenaz, Emmanuelle .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 223 (0C) :29-46
[27]   Zone extrapolations in parametric timed automata [J].
Arcile, Johan ;
Andre, Etienne .
INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2025, 21 (02) :707-726
[28]   Zone Extrapolations in Parametric Timed Automata [J].
Arcile, Johan ;
Andre, Etienne .
NASA FORMAL METHODS (NFM 2022), 2022, 13260 :451-469
[29]   What's Decidable About Parametric Timed Automata? [J].
Andre, Etienne .
FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, (FTSCS 2015), 2016, 596 :52-68
[30]   Durations and parametric model-checking in timed automata [J].
Bruyere, Veronique ;
Dall'olio, Emmanuel ;
Raskin, Jean-Francois .
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2008, 9 (02)
12345