What's decidable about parametric timed automata?
From MaRDI portal
Publication:4686606
DOI10.1007/978-3-319-29510-7_3zbMATH Open1396.68064arXiv1907.01721OpenAlexW2296504218MaRDI QIDQ4686606FDOQ4686606
Authors: Étienne André 
Publication date: 2 October 2018
Published in: Communications in Computer and Information Science (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1907.01721
Recommendations
Cites Work
- Uppaal in a nutshell
- A theory of timed automata
- Title not available (Why is that?)
- What's decidable about hybrid automata?
- Symbolic model checking for real-time systems
- Low dimensional hybrid systems -- decidable, undecidable, don't know
- AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA
- Parametric real-time reasoning
- Decision problems for lower/upper bound parametric timed automata
- Linear parametric model checking of timed automata
- Parametric temporal logic for “model measuring”
- Title not available (Why is that?)
- Real-Time Model-Checking: Parameters everywhere
- 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
- Bounded Model Checking for Parametric Timed Automata
- Advances in Parametric Real-Time Reasoning
- Robustness in timed automata
- Robust parametric reachability for timed automata
- Language emptiness of continuous-time parametric timed automata
- The expressive power of clocks
- Integer-complete synthesis for bounded parametric timed automata
- Language preservation problems in parametric timed automata
- Parametric Interrupt Timed Automata
- MTL-model checking of one-clock parametric timed automata is undecidable
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
- Decision Problems for Lower/Upper Bound Parametric Timed Automata
- Language emptiness of continuous-time parametric timed automata
- Language preservation problems in parametric timed automata
- The language preservation problem is undecidable for parametric event-recording automata
- What's decidable about recursive hybrid 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
- Title not available (Why is that?)
Uses Software
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)
