Language Preservation Problems in Parametric Timed Automata

Abstract

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.

Extended version of the paper of the name published in the proceedings of FORMATS 2015

References in corpus (1)

• The language preservation problem is undecidable for parametric event-recording automata

Cited by in corpus (5)

• A Benchmarks Library for Extended Parametric Timed Automata
• Guaranteeing Timed Opacity using Parametric Timed Model Checking
• Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed Automata
• Efficient Convex Zone Merging in Parametric Timed Automata
• Reachability and liveness in parametric timed automata