Jeudi 21 Mai

Retour à la vue des calendrier
Jeudi 21 Mai
Heure: 14:30 - 15:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Reachability Preservation Based Parameter Synthesis for Timed Automata
Description: Étienne André The synthesis of timing parameters consists in deriving conditions
on the timing constants of a concurrent system such that it meets its
Parametric timed automata are a powerful formalism for parameter
synthesis, although most problems are undecidable.
We first address here the following reachability preservation
problem: given a reference parameter valuation and a (bad) control
state, do there exist other parameter valuations that reach this control
state iff the reference parameter valuation does?
We show that this problem is undecidable, and introduce a procedure
that outputs a possibly underapproximated answer.
We then show that our procedure can efficiently replace the
behavioral cartography to partition a bounded parameter subspace into
good and bad subparts; furthermore, our procedure can even outperform
the classical bad-state driven parameter synthesis semi-algorithm,
especially when distributed on a cluster.