Description

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.

Compétences requises

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.

Bibliographie

[1] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. 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
[4] Angelo Ferrando, Vadim Malvone: VITAMIN: VerIficaTion of A MultI ageNt system. AAMAS 2025: 3023-3025.
[5] Angelo Ferrando, Vadim Malvone: VITAMIN: A Compositional Framework for Model Checking of Multi-Agent Systems. ICAART (1) 2025: 648-655.
[6] R. H. Thaler and C. R. Sunstein, Nudge: improving decisions about health, wealth, and happiness. New Haven: Yale University Press, 2008.
[7] Alchourrón, C.E., P. Gärdenfors, and D. Makinson, 1985, “On the Logic of Theory Change: Partial Meet Contraction and Revision Functions”, Journal of Symbolic Logic, 50: 510–530.
[8] Tutić, A., Voss, T. (2020). Trust and game theory. In The Routledge Handbook of Trust and Philosophy (1st ed.) 175-188. Routledge.
[9] Luca Congiu, Ivan Moscati (2022). “A review of nudges: Definitions, justifications, effectiveness”, Journal of Economic Surveys, Volume 36, Issue 1.
[10] Kulkarni, S., & Brunswicker, S. (2024). Learning Nudges for Conditional Cooperation: A Multi-Agent Reinforcement Learning Model. ArXiv Preprint.
[11] Winfield, A. F. T. (2018). Experiments in Artificial Theory of Mind: From Safety to Story-Telling. Frontiers in Robotics and AI, 5, 75.

Mots clés

Systèmes multi-agents, Vérification formelle, Raisonnement stratégique, Nudge theory