Thèse Définir des Stratégies de Nudging dans la Spécification des Propriétés pour les Systèmes Multi-Agents H/F - Doctorat.Gouv.Fr

Établissement : Institut Polytechnique de Paris Télécom Paris École doctorale : Ecole Doctorale de l'Institut Polytechnique de Paris Laboratoire de recherche : Laboratoire de Traitement et Communication de l'Information Direction de la thèse : Vadim MALVONE ORCID 0000000161384229 Début de la thèse : 2026-10-01 Date limite de candidature : 2026-07-31T23:59:59 Assurer la correction des systèmes critiques est essentiel, notamment dans les domaines où les défaillances ont un coût élevé. La vérification formelle traditionnelle est efficace pour les systèmes clos, mais elle présente des limites dans les environnements ouverts et multi-agents où les agents interagissent de manière stratégique. Alors que les logiques temporelles permettent de raisonner sur les stratégies des agents, elles ne capturent pas les interventions subtiles, comme le nudging, où un agent peut influencer le comportement d'un autre sans restreindre ses choix. Le nudging préserve l'autonomie en modifiant l'environnement décisionnel de manière à orienter le comportement de façon prévisible mais sans coercition.Cette recherche vise à formaliser le nudging dans les systèmes multi-agents, en l'intégrant aux cadres de raisonnement stratégique et de révision des croyances. Elle étudiera également comment le nudging interagit avec la dynamique de confiance, en modélisant la manière dont les agents ajustent leurs stratégies en fonction de la confiance envers les intentions des autres. Le projet développera des modèles, des logiques, des algorithmes et des outils de vérification pour analyser ces interactions, offrant un cadre pour concevoir des systèmes multi-agents autonomes, fiables et éthiques. Les résultats attendus feront progresser la vérification formelle, le raisonnement stratégique et les applications pratiques dans les environnements multi-agents. Ensuring the correctness of critical systems is essential, particularly in domains where failure is costly. Traditional model checking verifies closed systems [1] but struggles with open systems involving multiple interacting agents [2,3]. Extensions using strategic temporal logics, such as ATL [2] and Strategy Logic [3], address multi-agent systems, yet they do not capture subtle influences like nudging [6], where one agent can steer another's behavior without limiting choices.Nudging is defined as modifying the choice architecture to influence behavior predictably while preserving autonomy [6,9]. Unlike coercion, nudging respects freedom of action. This concept is increasingly relevant in behavioral sciences and economics [9], and it also has practical implications in multi-agent systems. Applications include promoting cooperation in Public Goods Games [10], algorithmic nudging in technology-driven contexts, and artificial theory of mind for robot swarms [11], enabling agents to anticipate consequences, revise beliefs, and optimize interactions. Despite its importance, the formal integration of nudging into multi-agent system verification remains largely unexplored.This research aims to formalize nudging within multi-agent systems, extending strategic reasoning and belief revision frameworks [7]. It will develop models and logics to represent nudging, design verification algorithms, and implement them in the VITAMIN tool [4,5]. Complete models will be used to ensure agents' maximal freedom, with nudging modeled as transformations that prune or reweight action possibilities while maintaining autonomy.Trust dynamics are also considered, with trust modeled as a risk metric based on transparency, goal alignment, and historical reliability [8]. Agents' belief systems will be represented using belief revision logic [7], replacing propositions with strategies in concurrent games.Expected outcomes include formalizing nudging, creating verification algorithms for dynamic decision-making, and developing tools to support ethical, trustworthy multi-agent environments. These contributions aim to advance the state of the art in formal verification and strategic reasoning, enhancing agent autonomy, interaction, and practical applications in multi-agent systems.

Compétences et Qualifications Attendues :- Master en informatique, mathématiques, intelligence artificielle ou dans un domaine connexe.- Solide formation en informatique et/ou en mathématiques, avec un accent sur les méthodes formelles, la logique ou l'informatique théorique.- Bonnes compétences en programmation et expérience en développement logiciel.- Maîtrise de l'anglais écrit et oral.

• Programmation
• Anglais
• Développement logiciel
• Mathématiques