SMT-based Parameter Synthesis for L/U Automata

International Workshop on Petri Nets and Software Engineering

Micha l Knapik ; Wojciech Penczek

Others  :  http://ceur-ws.org/Vol-851/paper6.pdf

来源: CEUR

【 摘 要 】

We present and evaluate a straightforward method of representing finite runs of a parametric timed automaton (PTA) by means of formulae accepted by satisfiability modulo theories (SMT)-solvers. Our method is applied to the problem of parametric reachability, i.e., the synthesis of a set of the parameter substitutions under which a state satisfying a given property is reachable. While the problem of parametric reachability is not decidable in general, we provide algorithms for underapproximation of the solution to this problem for a certain class of PTA, namely for the lower/upper bound automata.