Vérification de modèles quantitatifs

Dans cet exposé, nous nous intéressons à la vérification de systèmes complexes, c'est-à-dire de systèmes soumis à de multiples contraintes quantitatives. Nous baserons notre exposé sur le modèle des automates temporisés, qui a vu le jour dans les années 1990 et qui permet de représenter des systèmes soumis à des contraintes sur les délais. Nous en exposerons les propriétés fondamentales, au cœur de leur succès, puis nous exposerons quelques extensions qui ont été étudiées, afin d'enrichir les propriétés quantitatives que l'on peut prendre en compte. Nous mentionnerons également quelques outils permettant d'analyser ces modèles, ainsi que quelques exemples d'applications.