Jeudi 20 Octobre

Retour à la vue des calendrier
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.