Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Advances in Parametric Real-Time Reasoning
verfasst von : Daniel Bundala, Joël Ouaknine
Erschienen in: Mathematical Foundations of Computer Science 2014
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We study the decidability and complexity of the reachability problem in parametric timed automata. The problem was introduced 20 years ago by Alur, Henzinger, and Vardi in [1], where they showed decidability in the case of a single parametric clock, and undecidability for timed automata with three or more parametric clocks.
By translating such problems as reachability questions in certain extensions of parametric one-counter machines, we show that, in the case of two parametric clocks (and arbitrarily many nonparametric clocks), reachability is decidable for parametric timed automata with a single parameter, and is moreover
PSPACE
NEXP
-hard. In addition, in the case of a single parametric clock (with arbitrarily many nonparametric clocks and arbitrarily many parameters), we show that the reachability problem is
NEXP
-complete, improving the nonelementary decision procedure of Alur
et al.