Contrôleurs pour la Synthèse Multicritère de Systèmes Réactifs : une Perspective Stratégique

Nous vivons l’ère de l’intelligence ambiante : nous sommes entourés de systèmes (informatiques) réactifs (SIRs) qui interagissent continuellement avec leur environnement via des instructions utilisateur, des senseurs, etc. Leur exactitude est souvent cruciale, soit pour des raisons de sécurité (p.ex. ABS), soit pour des contraintes de production de masse (p.ex. smartphones). Néanmoins, leur conception est complexe et sujette aux erreurs. La vérification formelle et la synthèse sont deux réussites de l’informatique, qui ont pour but la construction automatique de contrôleurs fiables pour les SIRs. Beaucoup de techniques se fondent sur la théorie des jeux, modélisant les interactions entre le SIR et son environnement sous forme de jeu compétitif.

Le domaine a évolué des spécifications booléennes vers les quantitatives, amenant des modèles capables de décrire la performance de SIRs. Les recherches récentes se concentrent sur les interactions entre différents aspects quantitatifs (ou qualitatifs) et les compromis en résultant. De tels compromis peuvent apparaître entre différentes ressources (p.ex. diminuer le temps de réponse requiert plus de puissance de calcul et de consommation énergétique) mais aussi entre différents modèles comportementaux (p.ex. performance dans le pire des cas vs en moyenne). Ces interactions sont au coeur des scénarios réels et demandent que les développeurs décident de l’équilibre entre différents aspects. Mon groupe de recherche est l’un des précurseurs sur la  synthèse multicritère.

L’objectif de ce projet est de questionner le concept central de stratégie, actuellement basé sur des modèles inspirés des automates finis, et servant de canevas formel pour des contrôleurs implémentables. Mon but est d’augmenter la compréhension théorique et l’utilité pratique de ce concept abstrait via l’étude systématique de modèles de stratégie alternatifs. Ce projet présage des avancées fondamentales vers la synthèse multicritère réellement applicable.