Description

La théorie des jeux en IA est un cadre mathématique puissant pour raisonner sur les systèmes réactifs. Ces derniers se caractérisent par une interaction continue entre deux ou plusieurs entités, appelées agents, et le comportement du système repose entièrement sur cette interaction. La théorie des jeux a été largement étudiée dans un certain nombre de domaines, tels que l'économie, la biologie et l'informatique.

Une application importante de la théorie des jeux en informatique, et plus récemment en IA, concerne la vérification formelle des systèmes. En effet, la théorie des jeux est devenue un outil puissant pour vérifier le bon fonctionnement des systèmes réactifs et des systèmes embarqués. Ce succès remonte à la fin des années soixante-dix avec l'introduction du model checking [1]. L'idée de cette technique est à la fois efficace et simple. Effectivement, pour vérifier si un système satisfait un comportement souhaité, nous vérifions plutôt si un modèle mathématique du système répond à une spécification formelle. Pour cette dernière, des logiques temporelles, telles que LTL et CTL, sont généralement utilisées.

Cependant, les premières applications du model checking concernaient uniquement les systèmes fermés, qui se caractérisent par le fait que leur comportement est entièrement déterminé par leurs états internes. Malheureusement, toutes les techniques de model checking développées pour manipuler des systèmes fermés se révèlent inutiles dans la pratique, car la plupart des systèmes sont ouverts, c'est-à-dire qu'ils se caractérisent par une interaction continue avec d'autres systèmes. Pour surmonter ce problème, le model checking a été étendu aux systèmes multi-agents. Les contributions révolutionnaires qui ont été faites dans cette direction concernent l'introduction de logiques pour le raisonnement stratégique, telles que l'Alternating-time Logic (ATL) [2], la Strategy Logic (SL) [3], et leurs extensions. ATL est une généralisation de CTL, dans laquelle les quantificateurs de chemin existentiel E et universel A sont remplacés par des modalités stratégiques de la forme et [A], où A est un ensemble d'agents. D'autre part, SL est une extension de LTL et traite les stratégies comme des objets du premier ordre, qui peuvent être déterminés par les quantificateurs existentiels Ex et universels Ax, qui peuvent être respectivement lus comme 'il existe une stratégie x' et 'pour toutes les stratégies x'.

Cependant, ATL et SL souffrent de deux problèmes principaux sur deux aspects différents. D’une part, ATL présente une complexité polynomial du model checking, mais elle ne peut pas exprimer plusieurs concepts de solutions, tels que l'équilibre de Nash. La principale limitation d'ATL est qu'elle utilise les stratégies de façon implicite dans la sémantique de ses modalités. Elle est donc faible en expressivité. D'autre part, SL est la logique la plus puissante pour le raisonnement stratégique, mais le problème du model checking n'est pas élémentaire. Ainsi, la logique complète ne peut pas avoir d'applications pratiques.

L'objectif de ce projet de thèse est divisé en deux étapes principales :

1. Définir une nouvelle logique pour le raisonnement stratégique qui puisse intégrer les caractéristiques positives d'ATL en termes de complexité et celles de SL en termes d'expressivité. Par conséquent, une étude approfondie de la sémantique de ces logiques est nécessaire pour trouver le bon compromis.
2. Développer un outil de model checking capable de résoudre le problème de vérification pour la nouvelle logique proposée.

Compétences requises

Compétences et qualifications attendues : Master en informatique, mathématiques ou domaines connexes Solides connaissances en informatique et/ou mathématiques (avec une attention particulière aux méthodes formelles et aux logiques) Bonnes compétences en programmation Bon niveau d'anglais écrit et parlé

Bibliographie

[1] Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press, 1999.
[2] R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-Time Temporal Logic. JACM, 49(5):672–713, 2002.
[3] F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning About Strategies: On the Model-Checking Problem. TOCL, 15(4):34:1--34:47, 2014.

Mots clés

Logiques stratégiques, Vérification formelle, Raisonnement stratégique, Systèmes multi-agents