Parameter Synthesis Problems for Parametric Timed Automata

TL;DR

This paper investigates the parameter synthesis problem for parametric timed automata, focusing on decidable subclasses and proposing efficient algorithms to compute feasible parameter regions.

Contribution

It identifies decidable subclasses of PTAs and develops efficient algorithms for parameter synthesis within these subclasses.

Findings

Decidable subclasses of PTAs are characterized.

Efficient algorithms for parameter synthesis are proposed.

Feasible regions for parameters can be computed in these subclasses.

Abstract

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.