What's Decidable About Parametric Timed Automata?

被引：10

作者：

Andre, Etienne ^{[1
,2
]}

机构：

[1] Univ Paris 13, CNRS, UMR 7030, Sorbonne Paris Cite,LIPN, F-93430 Villetaneuse, France

[2] Ecole Cent Nantes, IRCCyN, CNRS, UMR 6597, Nantes, France

来源：

FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, (FTSCS 2015) | 2016年 / 596卷

关键词：

MODEL CHECKING; VERIFICATION;

D O I：

10.1007/978-3-319-29510-7_3

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Parametric timed automata (PTA) are a powerful formalism to reason, simulate and formally verify critical real-time systems. After two decades of research on PTA, it is now well-understood that any non-trivial problem studied is undecidable for general PTA. We provide here a survey of decision and computation problems for PTA. On the one hand, bounding time, bounding the number of parameters or the domain of the parameters does not (in general) lead to any decidability. On the other hand, restricting the number of clocks, the use of clocks (compared or not with the parameters), and the use of parameters (e.g., used only as upper or lower bounds) leads to decidability of some problems.

引用

页码：52 / 68

页数：17

共 34 条

[1] A THEORY OF TIMED AUTOMATA [J].

ALUR, R ;

DILL, DL .

THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235

[2]

Alur R., 1993, Proceedings of the Twenty-Fifth Annual ACM Symposium on the Theory of Computing, P592, DOI 10.1145/167088.167242

[3]

Andre Etienne, 2015, Reachability Problems. 9th International Workshop, RP 2015. Proceedings: LNCS 9328, P7, DOI 10.1007/978-3-319-24537-9_2

[4]

Andre Etienne, 2012, FM 2012: Formal Methods. Proceedings of the 18th International Symposium, P33, DOI 10.1007/978-3-642-32759-9_6

[5]

Andre E., 2016, DECISION PROBL UNPUB

[6] Language Preservation Problems in Parametric Timed Automata [J].

Andre, Etienne ;

Markey, Nicolas .

FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS 2015), 2015, 9268 :27-43

[7] AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA [J].

Andre, Etienne ;

Chatain, Thomas ;

Fribourg, Laurent ;

Encrenaz, Emmanuelle .

INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2009, 20 (05) :819-836

[8]

[Anonymous], 1967, Computation

[9] Low dimensional hybrid systems - decidable, undecidable, don't know [J].

Asarin, Eugene ;

Mysore, Venkatesh P. ;

Pnueli, Amir ;

Schneider, Gerardo .

INFORMATION AND COMPUTATION, 2012, 211 :138-159

[10] Language Emptiness of Continuous-Time Parametric Timed Automata [J].

Benes, Nikola ;

Bezdek, Peter ;

Larsen, Kim G. ;

Srba, Jiri .

AUTOMATA, LANGUAGES, AND PROGRAMMING, PT II, 2015, 9135 :69-81

← 1 2 3 4 →