Language Preservation Problems in Parametric Timed AutomataArticle
Authors: Étienne André ; Didier Lime ; Nicolas Markey
NULL##NULL##NULL
Étienne André;Didier Lime;Nicolas Markey
Parametric timed automata (PTA) are a powerful formalism to model and reason
about concurrent systems with some unknown timing delays. In this paper, we
address the (untimed) language- and trace-preservation problems: given a
reference parameter valuation, does there exist another parameter valuation
with the same untimed language, or with the same set of traces? We show that
these problems are undecidable both for general PTA and for the restricted
class of L/U-PTA, even for integer-valued parameters, or over bounded time. On
the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter
deterministic L-PTA and U-PTA. We also consider robust versions of these
problems, where we additionally require that the language be preserved for all
valuations between the reference valuation and the new valuation.