Systèmes multi-agents avancés

Description du cours

Cette unité d’enseignement porte sur la conception formelle et l’analyse des interactions au sein des systèmes multi-agents (SMA). L’objectif est de présenter des outils théoriques pour modéliser, raisonner et vérifier les comportements collectifs d’agents autonomes. Le cours s’organise en deux grandes parties : Théorie des jeux. La première partie des cours introduit les bases de la théorie des jeux, en abordant à la fois les jeux non coopératifs et coopératifs. Les jeux non coopératifs étudient des situations où chaque agent agit indépendamment pour maximiser son utilité. Les jeux coopératifs, quant à eux, modélisent des interactions où les agents peuvent former des coalitions. Spécification et vérification de SMA. La seconde partie des cours est dédiée à la vérification formelle des propriétés dans les SMA. Il s’agit de garantir que les comportements des agents respectent des contraintes logiques à l’aide de méthodes comme la vérification de modèles (model checking) et la preuve de théorèmes (theorem proving). Les travaux pratiques visent à expérimenter, afin de mieux les appréhender, les concepts théoriques vus en cours en les implémentant.

Modalités d'évaluation

Session 1 :

• Contrôle continu (CC1) : Il s’agit de deux travaux à rendre. Sur la partie théorie des jeux, les implémentations réalisées en travaux pratiques seront évaluées. Sur la partie spécification et vérification formelle de SMA, l’évaluation prend la forme d’un problème original à modéliser formellement et à prouver grâce à des outils de vérification automatique.
• Contrôle terminal (CT1) : Il s’agit d’un écrit de 2 heures avec des exercices et questions de modélisation et réflexion. Les documents sont autorisés.
• Note finale : la note finale est calculée de la façon suivante : 21 × CC1 + 21 × CT 1.

Session 2 :

• Contrôle terminal (CT2) : Il s’agit d’un écrit de 2 heures avec des exercices et questions de modélisation et réflexion. Les documents sont autorisés.
• Note finale : la note finale est calculée de la façon suivante : 21 × CC1 + 21 × CT 2.