Integer-Complete Synthesis for Bounded Parametric Timed Automata?

Abstract. Ensuring the correctness of critical real-time systems, involv-ing concurrent behaviors and timing requirements, is crucial. Parameter synthesis aims at computing dense sets of valuations for the timing re-quirements, guaranteeing a good behavior. However, in most cases, the emptiness problem for reachability (i.e., whether there exists at least one parameter valuation for which some state is reachable) is undecid-able and, as a consequence, synthesis procedures do not terminate in general, even for bounded parameters. In this paper, we introduce a parametric extrapolation, that allows us to derive an underapproxima-tion in the form of linear constraints containing all the integer points ensuring reachability or unavoidability, and all the (non-necessarily inte-ger) convex combinations of these integer points, for general PTA with a bounded parameter domain. Our algorithms terminate and can output constraints arbitrarily close to the complete result.