What's decidable about parametric timed automata?
From MaRDI portal
Publication:4686606
Abstract: Parametric timed automata (PTAs) are a powerful formalism to reason, simulate and formally verify critical real-time systems. After 25 years of research on PTAs, it is now well-understood that any non-trivial problem studied is undecidable for general PTAs. We provide here a survey of decision and computation problems for PTAs. 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. We also put emphasis on open problems. We also discuss formalisms close to parametric timed automata (such as parametric hybrid automata or parametric interrupt timed automata), and we study tools dedicated to PTAs and their extensions.
Recommendations
Cites work
- scientific article; zbMATH DE number 1444359 (Why is no real title available?)
- scientific article; zbMATH DE number 3310089 (Why is no real title available?)
- A theory of timed automata
- AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA
- Advances in Parametric Real-Time Reasoning
- Bounded Model Checking for Parametric Timed Automata
- Decision problems for lower/upper bound parametric timed automata
- Integer-complete synthesis for bounded parametric timed automata
- Language emptiness of continuous-time parametric timed automata
- Language preservation problems in parametric timed automata
- Linear parametric model checking of timed automata
- Low dimensional hybrid systems -- decidable, undecidable, don't know
- MTL-model checking of one-clock parametric timed automata is undecidable
- Parametric Interrupt Timed Automata
- Parametric real-time reasoning
- Parametric temporal logic for “model measuring”
- Real-Time Model-Checking: Parameters everywhere
- Robust parametric reachability for timed automata
- Robustness in timed automata
- Symbolic model checking for real-time systems
- The expressive power of clocks
- Time-bounded reachability for monotonic hybrid automata: complexity and fixed points
- Timed verification of the generic architecture of a memory circuit using parametric timed automata
- Uppaal in a nutshell
- What's decidable about hybrid automata?
Cited in
(13)- MTL-model checking of one-clock parametric timed automata is undecidable
- Decision problems for lower/upper bound parametric timed automata
- Parametric updates in parametric timed automata
- TCTL model checking lower/upper-bound parametric timed automata without invariants
- The language preservation problem is undecidable for parametric event-recording automata
- Language emptiness of continuous-time parametric timed automata
- Decision Problems for Lower/Upper Bound Parametric Timed Automata
- What's decidable about recursive hybrid automata?
- Language preservation problems in parametric timed automata
- Language preservation problems in parametric timed automata
- Iterative bounded synthesis for efficient cycle detection in parametric timed automata
- On the expressiveness of parametric timed automata
- scientific article; zbMATH DE number 1798172 (Why is no real title available?)
This page was built for publication: What's decidable about parametric timed automata?
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4686606)
