Trouver l'écart entre les logiques stratégiques existantes pour le processus de vérification // Find the gap between the existing strategic logics for the verification process

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.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Game theory in AI is a powerful mathematical framework for reasoning about reactive systems. These systems are characterized by ongoing interactions between two or more entities, called agents, and the behavior of the system depends entirely on this interaction. Game theory has been widely studied in a number of fields, such as economics, biology, and computer science.

An important application of game theory in computer science and, more recently, in AI, is formal system verification. In particular, game theory has become a powerful tool for verifying the correct functioning of reactive and embedded systems. This success story dates back to the late seventies with the introduction of model checking [1]. The idea behind model checking is both simple and powerful. Specifically, instead of checking whether a system satisfies a desired behavior directly, we check whether a mathematical model of the system satisfies a formal specification. Temporal logics, such as LTL and CTL, are typically used for this purpose.

However, the first applications of model checking focused solely on closed systems, which are characterized by the fact that their behavior is entirely determined by their internal states. Unfortunately, all model checking techniques developed for closed systems turned out to be largely ineffective in practice, as most systems are open in the sense that they interact continuously with other systems. To address this issue, model checking has been extended to multi-agent systems. Key contributions in this area include the introduction of logics for strategic reasoning, such as Alternating-time Temporal Logic (ATL) [2], Strategy Logic (SL) [3], and their extensions. ATL is a generalization of CTL, where the existential E and universal A path quantifiers are replaced by strategic modalities of the form and [A], where A is a set of agents. On the other hand, SL is an extension of LTL that treats strategies as first-order objects, which can be determined using the existential Ex and universal Ax quantifiers, which are read as 'there exists a strategy x' and 'for all strategies x,' respectively.

However, ATL and SL both have significant limitations. ATL has polynomial model checking complexity, but it cannot express several solution concepts, such as Nash equilibrium. Its main limitation is that it treats strategies implicitly within the semantics of its modalities, making it weak in terms of expressivity. In contrast, SL is a more powerful logic for strategic reasoning, but its model checking problem is non-elementary, making the full logic impractical for many real-world applications.

The aim of this thesis project is divided into two main steps:

1. Define a new logic for strategic reasoning that combines the positive features of ATL in terms of complexity with the strengths of SL in terms of expressivity. To achieve this, a detailed study of the semantics of these logics will be necessary to find the right balance.
2. Develop a model checking tool capable of solving the verification problem for the newly proposed logic.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Début de la thèse : 01/10/2025