Parameter Synthesis Problems for one parametric clock Timed Automata

TL;DR

This paper investigates the parameter synthesis problem for a specific class of parametric timed automata with one parametric clock, providing solutions under linear and polynomial inequality constraints.

Contribution

It demonstrates the solvability of the parameter synthesis problem for automata with one parametric clock and complex polynomial constraints, extending previous results.

Findings

Parameter synthesis is solvable for automata with one parametric clock and linear expressions.

Synthesis remains solvable with polynomial inequality constraints.

The parameter domain considered is the nonnegative real numbers.

Abstract

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.