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 条
[41]   Reachability in Succinct and Parametric One-Counter Automata [J].
Haase, Christoph ;
Kreutzer, Stephan ;
Ouaknine, Joel ;
Worrell, James .
CONCUR 2009 - CONCURRENCY THEORY, PROCEEDINGS, 2009, 5710 :369-383
[42]   Reachability analysis for timed automata using max-plus algebra [J].
Lu, Qi ;
Madsen, Michael ;
Milata, Martin ;
Ravn, Soren ;
Fahrenberg, Uli ;
Larsen, Kim G. .
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2012, 81 (03) :298-313
[43]   A Symbolic Algorithm for the Analysis of Robust Timed Automata [J].
Kordy, Piotr ;
Langerak, Rom ;
Mauw, Sjouke ;
Polderman, Jan Willem .
FM 2014: FORMAL METHODS, 2014, 8442 :351-366
[44]   On parametric timed automata and one-counter machines [J].
Bundala, Daniel ;
Ouaknine, Joel .
INFORMATION AND COMPUTATION, 2017, 253 :272-303
[45]   Timed verification of the generic architecture of a memory circuit using parametric timed automata [J].
Chevallier, Remy ;
Encrenaz-Tiphene, Emmanuelle ;
Fribourg, Laurent ;
Xu, Weiwen .
FORMAL METHODS IN SYSTEM DESIGN, 2009, 34 (01) :59-81
[46]   Parametric Deadlock-Freeness Checking Timed Automata [J].
Andre, Etienne .
THEORETICAL ASPECTS OF COMPUTING - ICTAC 2016, 2016, 9965 :469-478
[47]   Layered and Collecting NDFS with Subsumption for Parametric Timed Automata [J].
Hoang Gia Nguyen ;
Petrucci, Laure ;
van de Pol, Jaco .
2018 23RD INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS), 2018, :1-9
[48]   Modelling and analysis of asynchronous circuits and timing diagrams using parametric timed automata [J].
Chen, CL ;
Lin, T ;
Yen, HC .
PROCEEDINGS OF THE 23RD IASTED INTERNATIONAL CONFERENCE ON MODELLING, IDENTIFICATION, AND CONTROL, 2004, :500-505
[49]   Decision problems for lower/upper bound parametric timed automata [J].
Laura Bozzelli ;
Salvatore La Torre .
Formal Methods in System Design, 2009, 35 :121-151
[50]   Shrinking timed automata [J].
Sankur, Ocan ;
Bouyer, Patricia ;
Markey, Nicolas .
INFORMATION AND COMPUTATION, 2014, 234 :107-132
12345