Marie Van Den Bogaard, récompensée pour ses travaux sur la vérification des systèmes réactifs

Certains systèmes sont trop critiques pour risquer l’incident, il faut alors apporter une preuve mathématique qu’ils vont fonctionner correctement. Marie Van Den Bogaard, maître de conférences à l’Université Gustave Eiffel et membre du LIGM, applique ainsi des méthodes formelles pour la vérification des systèmes réactifs. Ces derniers permettent à plusieurs agents d’interagir de façon complexe et continue, tout en ayant chacun leur propre tâche.

« Les voitures autonomes sont de bons exemples de systèmes réactifs, précise Marie Van Den Bogaard. Elles doivent aller d’un point à l’autre tout en respectant un grand nombre de contraintes liées à la conduite. Les systèmes réactifs sont souvent critiques, leur exécution réclame des garanties fortes pour éviter les accidents. »

Pour cela, les méthodes formelles prennent un système réactif et en extraient un modèle mathématique, à partir duquel on observe ses propriétés pour obtenir des preuves mathématiques de la fiabilité du système. Différentes méthodes existent, mais Marie Van Den Bogaard s’est spécialisée dans l’approche « jeu », influencée, comme son nom l’indique, par la théorie des jeux.

Dans ces parties à durée infinie, les joueurs déplacent un unique pion le long des sommets d’un graphe. Les sommets de ce graphe représentent les différentes configurations possibles du système global, modifiées à chaque action d’un joueur. Chaque participant a son propre objectif de nature qu’il doit valider afin de remporter la partie ; on parle d’objectif qualitatif (modèle oui/non).

« Si on parle de voitures, cet objectif va généralement être d’arriver à destination, reprend comme exemple Marie Van Den Bogaard. Ces objectifs qualitatifs peuvent aussi être nuancés : effectuer le trajet en un temps raisonnable, le faire sans passer par trop d’étapes ou de détours… » L’enseignante-chercheuse développe avant tout une compréhension théorique de ces systèmes, ouvrant à terme la porte à de nouveaux travaux et applications de la part de la communauté scientifique.

Marie Van Den Bogaard manie pour cela le concept du mean-payoff, où l’on prend en compte la moyenne lissée des gains instantanés obtenus par les mouvements de pion de chaque joueur. Les possibilités sont fortement circonscrites si l’on considère en plus que les joueurs sont rationnels, et ne changent pas brusquement de stratégie. On se retrouve alors dans le cas d’un autre concept classique, l’équilibre de Nash, où chaque joueur prévoit correctement le choix des autres et parvient grâce à cela à maximiser ses gains. Cela permet d’éliminer encore plus de cas irréalistes.

Dans l’article Subgame-perfect equilibria in mean-payoff games, Marie Van Den Bogaard développe, avec ses coauteurs Léonard Brice et Jean-François Raskin de l’Université libre de Bruxelles, le concept d’exigence de négociation. Ces travaux leur ont valu d’obtenir le prix du meilleur article à la conférence Concur.

On associe pour cela un nombre à chaque sommet du graphe détenu par un joueur, qui n’en changera que s’il en trouve un meilleur. Une fois que l’on connaît les exigences de chaque joueur pour chaque sommet, une phase de négociation leur permet de mettre à jour leurs exigences respectives en fonction de celles des autres. Cette phase élimine des comportements non rationnels, et elle est répétée jusqu’à une stabilisation où l’on ne peut plus mettre à jour les exigences. On parle alors d’équilibre parfait en sous-jeu. Il peut y en avoir plusieurs de possibles pour un même jeu et, s’ils sont tous identifiés, on a éliminé tous les cas irrationnels. On peut alors vérifier beaucoup plus facilement et rapidement si un système dynamique va fonctionner sans risque.