Parameter Synthesis Problems for one parametric clock Timed Automata
Provides a theoretical solution for a class of parametric timed automata, enabling automated synthesis of parameter valuations for real-time systems verification.
The paper solves the parameter synthesis problem for parametric timed automata with one parametric clock and arbitrarily many parameters, showing it is solvable for linear and polynomial inequality constraints over nonnegative reals.
In this paper, we study the parameter synthesis problem for a class of parametric timed automata. The problem asks to construct the set of valuations of the parameters in the parametric timed automa- ton, referred to as the feasible region, under which the resulting timed automaton satisfies certain properties. We show that the parameter syn- thesis problem of parametric timed automata with only one parametric clock (unlimited concretely constrained clock) and arbitrarily many pa- rameters is solvable when all the expressions are linear expressions. And it is moreover the synthesis problem is solvable when the form of con- straints are parameter polynomial inequality not just simple constraint and parameter domain is nonnegative real number.