Nous nous intéresserons au modèle des automates temporisés, qui a été proposé dans les années 1990 pour représenter les systèmes soumis à des contraintes temporelles quantitatives. Nous verrons quelles bonnes propriétés sont satisfaites par ce modèle et en explorerons quelques extensions. Nous présenterons enfin le modèle des automates à "entonnoirs" (funnel automata), basé sur les automates temporisés et leurs extensions, qui permettent d'appréhender et résoudre des problèmes de contrôle de systèmes dynamiques.

Cet exposé illustrera comment le domaine des méthodes formelles, et en particulier la thématique du model-checking, peut trouver des applications dans des domaines voisins tels que la robotique. Ce pont entre les deux domaines a été réalisé conjointement avec Nicolas Markey (maintenant à l'IRISA, Rennes), Nicolas Perrin (ISIR, Paris) et Philippe Schlehuber-Caissier (maintenant au LRDE, Paris).

http://www.lsv.fr/~bouyer/