Sciweavers

RP
2015
Springer

Integer-Complete Synthesis for Bounded Parametric Timed Automata

8 years 7 months ago
Integer-Complete Synthesis for Bounded Parametric Timed Automata
Abstract. Ensuring the correctness of critical real-time systems, involving concurrent behaviors and timing requirements, is crucial. Parameter synthesis aims at computing dense sets of valuations for the timing requirements, 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 undecidable 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 underapproximation in the form of linear constraints containing all the integer points ensuring reachability or unavoidability, and all the (non-necessarily integer) 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.
Étienne André, Didier Lime, Olivier
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where RP
Authors Étienne André, Didier Lime, Olivier H. Roux
Comments (0)