|
|
 |
|
Jeudi 20 Octobre
| Heure: |
15:30 - 16:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Integer-Complete Synthesis for Bounded Parametric Timed Automata |
| Description: |
Étienne André 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.
Joint work with Didier Lime and Olivier H. Roux. |
|
|
