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.
@article{arxiv.1809.07177,
title = {Parameter Synthesis Problems for one parametric clock Timed Automata},
author = {Liyun Dai and Taolue Chen and Zhiming Liu and Bican Xia and Naijun Zhan and Kim G. Larsen},
journal= {arXiv preprint arXiv:1809.07177},
year = {2018}
}
Comments
20 pages, 1 figure. arXiv admin note: substantial text overlap with arXiv:1808.06792