Skip to Main content Skip to Navigation
Conference papers

Integer-Complete Synthesis for Bounded Parametric Timed Automata

Étienne André 1 Didier Lime 2 Olivier Henri Roux 2
2 STR - STR
LS2N - Laboratoire des Sciences du Numérique de Nantes
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 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 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.
Complete list of metadatas

Cited literature [31 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-02939637
Contributor : Didier Lime <>
Submitted on : Tuesday, September 15, 2020 - 5:03:42 PM
Last modification on : Tuesday, January 5, 2021 - 4:26:09 PM
Long-term archiving on: : Friday, December 4, 2020 - 5:24:04 PM

File

andre-RP-15.pdf
Files produced by the author(s)

Identifiers

Citation

Étienne André, Didier Lime, Olivier Henri Roux. Integer-Complete Synthesis for Bounded Parametric Timed Automata. 9th International Conference on Reachability Problems (RP 2015), Sep 2015, Warsaw, Poland. pp.7-19, ⟨10.1007/978-3-319-24537-9_2⟩. ⟨hal-02939637⟩

Share

Metrics

Record views

33

Files downloads

159