Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
Decision Problems for Lower/Upper Bound Parametric Timed Automata
verfasst von : Laura Bozzelli, Salvatore La Torre
Erschienen in: Automata, Languages and Programming
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 investigate a class of parametric timed automata, called lower bound/upper bound (L/U) automata, where each parameter occurs in the timing constraints either as a lower bound or as un upper bound. For such automata, we show that checking if for a parameter valuation (resp., all parameter valuations) there is an infinite accepting run is
Pspace
-complete. We extend these results by allowing the specification of constraints on parameters as a linear system. We show that the considered decision problems are still
Pspace
-complete, if the lower bound parameters are not compared to the upper bound parameters in the linear system, and are undecidable in general. Finally, we consider a parametric extension of
, and prove that the related satisfiability and model checking (w.r.t. L/U automata) problems are
Pspace
-complete.