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

Distinctions Informatique

Utilisés par exemple dans les véhicules autonomes, les systèmes réactifs doivent remplir leurs missions sans accrocs. Marie Van Den Bogaard, du Laboratoire d'Informatique Gaspard-Monge (LIGM - CNRS/Université Gustave Eiffel), utilise des outils issus de la théorie des jeux pour vérifier leur fiabilité. Avec ses co-auteurs, elle a obtenu le prix de la meilleure publication de la conférence Concur.

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.

Pour modéliser un système réactif, on considère chacun de ses agents et composants comme un joueur, tandis que leurs interactions sont appelées des parties.
,

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.

Notre approche sur l’exigence de négociation est prometteuse pour d’autres classes de jeu, nous cherchons à présent à l’appliquer sur des objectifs plus généraux.
,

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.

Contact

Marie Van Den Bogaard
Maître de conférences, membre du LIGM