14-18 juin 2021 Virtuelle (France)
De l'analyse automatique de systèmes temporisés au contrôle de systèmes dynamiques
Patricia Bouyer-Decitre  1@  
1 : Laboratoire Méthodes Formelles  (LMF)
Institut National de Recherche en Informatique et en Automatique, CentraleSupélec, Université Paris-Saclay, Centre National de la Recherche Scientifique : UMR9021, Ecole Normale Supérieure Paris-Saclay
4, avenue des Sciences, 91190, Gif-sur-Yvette -  France

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/


Personnes connectées : 28 Vie privée
Chargement...