Parameter Synthesis Problems for Parametric Timed Automata
For researchers in formal verification, this work advances the tractability of parameter synthesis by identifying and solving decidable subclasses of an otherwise undecidable problem.
This paper studies parameter synthesis for parametric timed automata (PTAs), aiming to compute feasible parameter valuations for given properties. It identifies decidable subclasses of PTAs and proposes efficient algorithms for them.
We consider the parameter synthesis problem of parametric timed automata (PTAs). The problem is, given a PTA and a property, to compute the set of valuations of the parameters under which the resulting timed automaton satisfies the property. Such a set of parameter valuations is called a feasible region for the PTA and the property. The problem is known undecidable in general. This paper, however, presents our study on some decidable sub-classes of PTAs and proposes efficient parameter synthesis algorithms for them.