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.
翻译:在本文中, 我们研究一组参数的参数合成问题。 问题在于构建参数计时自动- 吨参数的一组估值, 称为可行区域, 由此得出的定时自动- 吨能满足某些属性。 我们显示, 当所有表达式都是线性表达式时, 参数测时自动- 倾斜参数的参数合成问题是可溶解的 。 此外, 当共力体的形式是参数多元不平等时, 不仅简单的制约, 参数域是非负数 。