Travail réalisé avec Bertrand Jeannet, Gabriel Kalyon, Hervé Marchand et Thierry Massart.

La synthèse de contrôleurs vise à rendre conforme à une spécification un système à événement discrets en restreignant son comportement. Pour ce faire, on calcule automatiquement un "superviseur" qui a une observation partielle du système. Ce superviseur autorise (ou non) certains événements à se produire.

Les travaux dans ce domaine se restreignent généralement à des systèmes dans lequel le problème d'atteignabilité est décidable (eg des systèmes finis). Cependant, en utilisant des méthodes de calcul approché de point-fixe utilisées en interprétation abstraite, on peut obtenir un superviseur valide même dans le cas où ce problème est indécidable.

Dans cet exposé, je présenterai les principes de la synthèse de contrôleurs pour des systèmes finis et pour des systèmes symboliques, et je montrerai comment calculer des superviseurs valides dans le cas des systèmes décentralisés/sous observation partielle et dans le cas des systèmes distribués.