2018/09/15 by Dai, Liyun, Chen, Taolue, Liu, Zhiming +3
#FOS: Computer and information sciences #FOS: Electrical engineering #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · doi:10.48550/arxiv.1809.07177
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.