MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable
Parametric timed automata extend timed automata (Alur and Dill, 1991) in that they allow the specification of parametric bounds on the clock values. Since their introduction in 1993 by Alur, Henzinger, and Vardi, it is known that the emptiness problem for parametric timed automata with one clock is...
Main Author: | Karin Quaas |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2014-03-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1404.0087v1 |
Similar Items
-
Improved Undecidability Results for Reachability Games on Recursive Timed Automata
by: Shankara Narayanan Krishna, et al.
Published: (2014-08-01) -
On the Expressiveness of TPTL and MTL over ω-Data Words
by: Claudia Carapelle, et al.
Published: (2014-05-01) -
Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic (Extended Abstract)
by: R van der Meyden, et al.
Published: (2016-06-01) -
Undecidability of the Spectral Gap in One Dimension
by: Johannes Bausch, et al.
Published: (2020-08-01) -
Kleene-Schützenberger and Büchi Theorems for Weighted Timed Automata
by: Quaas, Karin
Published: (2010)