Synthèse de stratégies pour des systèmes réactifs avec objectifs quantitatifs

Description

Le service de Véronique Bruyère a des activités de recherche dans le domaine des méthodes formelles et plus particulièrement en vérification et synthèse de systèmes informatiques fiables par le biais de la théorie algorithmique des jeux. Ces dernières années, d’importants progrès ont été réalisés à propos des systèmes réactifs qui sont des systèmes informatiques en interaction permanente avec l’environnement dans lequels ils évoluent (comme les contrôleurs embarqués dans les voitures ou les avions). Ces systèmes réactifs sont modélisés par des graphes dont les sommets modélisent les configurations du système et les arêtes modélisent les actions contrôlables (incontrôlables) du système (de l’environnement). L’interaction continue entre le système et l’environnement est modélisée par un jeu à deux joueurs sur ces graphes, dans lequel le système tente de maintenir un comportement cohérent quoique fasse l’environnement. Avoir un contrôleur fiable du système revient à exhiber une stratégie gagnante pour le système dans ce jeu sur graphe. L’existence, la construction, l’implémentation et la forme de telles stratégies ont été étudiées pour différents types d’objectifs, d’abord qualitatifs (par exemple éviter un deadlock) et plus récemment quantitatifs (par exemple minimiser l’énergie dépensée). Il reste beaucoup de questions ouvertes concernant la combinaison d’objectifs qualitatifs et quantitatifs.