Améliorer le Model Checking dans les Systèmes Multi-Agents via Runtime Verification // Improve Model Checking in Multi-Agent Systems via Runtime Verification

La vérification de modèle [1] est une technique de vérification formelle bien connue, qui vérifie si un modèle mathématique d'un système satisfait une propriété spécifiée par des logiques temporelles, avec de nombreuses applications (voir [2]). Cependant, cette technique est coûteuse en calcul et devient vite infaisable pour de grands systèmes (explosion de l'espace d'état). Heureusement, il existe des techniques de vérification plus légères, comme la vérification en temps réel [3], qui effectue la vérification en temps réel sur le système réel (plutôt que sur son modèle).

Pour résoudre le problème de vérification où plusieurs systèmes interagissent, la vérification par modèle a été étendue aux systèmes multi-agents. Dans ce contexte, les logiques temporelles ont été adaptées pour le raisonnement stratégique [4,5]. Ici, l'explosion de l'espace d'état reste un problème, et l'ajout d'agents, chacun avec sa propre visibilité, rend la vérification très difficile, souvent indécidable. Certaines approches ont tenté d'apporter des approximations sur la visibilité [6,7], les stratégies [8] ou les formules [9].

La vérification en temps réel pourrait aider à surmonter les difficultés de la vérification par modèle, mais elle n'a pas été appliquée aux scénarios stratégiques. Elle est surtout utilisée pour vérifier des protocoles d'interaction entre agents [10,11], où des propriétés formelles spécifient les protocoles de communication, et des moniteurs en temps réel vérifient la conformité des communications des agents à ces protocoles. De plus, étant donné que la vérification par modèle et la vérification en temps réel sont similaires, mais distinctes, il est pertinent de considérer aussi les intégrations possibles. Bien qu'il existe des travaux sur l'intégration de la vérification par modèle et de la vérification en temps réel (par exemple, [12]), aucune étude ne traite les systèmes multi-agents sous l'angle du raisonnement stratégique.

Objectifs

L'objectif de cette recherche est d'introduire, en théorie et en pratique, la vérification en temps réel dans la vérification par modèle pour les systèmes multi-agents. En intégrant le comportement stratégique dans la vérification en temps réel, des fonctionnalités intéressantes, comme la synthèse dynamique de stratégies, deviennent possibles.

Les défis de ce doctorat incluront les points suivants :

- Étudier la vérification par modèle dans les systèmes monolithiques et multi-agents ;
- Étudier la vérification en temps réel ;
- Développer des intégrations des techniques de vérification par modèle et de vérification en temps réel pour les systèmes multi-agents ;
- Combiner la vérification par modèle et la vérification en temps réel pour aborder la décidabilité dans des contextes indécidables ;
- Améliorer la vérification en temps réel avec un comportement prédictif en vérifiant d'abord les propriétés stratégiques via la vérification par modèle (lors de la phase de conception), puis en appliquant la vérification en temps réel pour les parties temporelles restantes (en temps réel) ;
- Utiliser des moniteurs en temps réel pour synthétiser des stratégies : non seulement pour savoir s'il existe une stratégie, mais aussi pour identifier laquelle ;
- Étendre les fondements théoriques de la vérification en temps réel pour traiter directement les propriétés stratégiques, en se basant sur les recherches actuelles sur la vérification en temps réel dans les logiques temporelles à branches.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Model Checking [1] is a well-known formal verification technique used to check if a mathematical model of a system satisfies a property specified via temporal logics. Therefore, model checking has several applications (e.g., see [2]). Unfortunately, this technique is computationally expensive and becomes infeasible when applied to large systems (state space explosion). Fortunately, other, more lightweight formal verification techniques exist, such as Runtime Verification [3], where the verification of a property is performed at runtime on the actual system (rather than on a model of the system).

To solve the verification problem in which several systems interact with each other, model checking has been extended to multi-agent systems. In this context, temporal logics have been extended to temporal logics for strategic reasoning [4, 5]. However, the state space explosion remains an open problem, and the introduction of a set of agents, each with its own visibility, makes the verification very difficult and often undecidable. Given the relevance of this setting, even partial solutions to the problem can be useful. Some approaches have focused on approximations, either on the visibility [6, 7], on the strategies [8], or on the formulas themselves [9].

Runtime Verification could help overcome the difficulties of model checking, but it has never been applied to strategic scenarios. Instead, it has mainly been used to verify agent interaction protocols [10, 11], where formal properties are used to specify communication protocols, and runtime monitors are used to verify whether the agents' communication conforms to such protocols. Moreover, since model checking and runtime verification are two similar formal verification techniques but differ in principle, it is extremely relevant not only to tackle the computational difficulties independently but also to explore possible integrations. Works on how to integrate model checking and runtime verification exist (e.g., see [12]), but no work in the area of multi-agent systems, especially when considering strategic reasoning, has ever been proposed.

Objectives

The aim of this research is to introduce, in theory and practice, runtime verification into model checking for multi-agent systems. Moreover, by enhancing runtime verification with strategic behavior, very interesting new features can be exploited, such as the dynamic synthesis of strategies for the agents by monitoring the system execution.

The challenges of this PhD will involve tackling (some of) the following points:

- Studying model checking in the context of monolithic systems and multi-agent systems;
- Studying runtime verification;
- Developing integrations of model checking and runtime verification techniques in the context of multi-agent systems;
- Developing techniques for combining model checking and runtime verification to determine the decidability of model checking in undecidable contexts;
- Enhancing runtime verification with predictive behavior by first verifying properties via model checking in the strategic context (at design time) and then applying runtime verification to the remaining temporal part (at runtime);
- Using runtime monitors to synthesize strategies. Existing logics for strategic reasoning aim to answer the question: Is there a strategy? But another important question is: Which strategy?
- Extending the theoretical foundations of runtime verification to handle strategic properties natively. This extension will build on existing research regarding the use of runtime verification in branching-time logics.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

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

Allocation doctorale AMX*

Télécom Paris

626 Ecole Doctorale de l'Institut Polytechnique de Paris

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é
Expected competencies and qualifications: - Master's degree in computer science, mathematics, or related fields - Strong background in computer science and/or mathematics (with particular emphasis on formal methods and logic) - Good programming skills - Good level of written and spoken English