Designing languages for expressing dependencies in strategic reasoning

Strategy Logique (SL, en abrégé) a été introduite par Chatterjee, Henzinger et Piterman comme un outil pour raisonner sur les stratégies. Ce formalisme puissant peut exprimer des notions stratégiques complexes telles que l'existence d'équilibre de Nash dans un jeu ou l'existence d'une stratégie défensive, etc. Cependant, cette expressivité vient à un prix, car le problème de vérification associé a une complexité non élémentaire et le problème de satisfaisabilité est indécidable. Une analyse soignée montre que cette haute complexité est liée à la nature monolithique des quantificateurs stratégiques dans SL, où les stratégies sont des citoyens de premier rang de la logique. En conséquence, dans une formule, une stratégie quantifiée dépend de toutes les stratégies quantifiées avant elle, dans leur intégralité, ce qui inclut leurs décisions futures. Cette caractéristique monolithique des quantificateurs SL empèche les stratégies considérée de ne dépendre que de l'histoire du jeu en cours et peut mener à des solutions avec des stratégies irréalisables, c'est-à-dire qui ne peuvent pas être mises en œuvre. Il est donc raisonnable d'investiguer de nouvelles sémantiques ou logiques qui garantissent la réalisabilité des stratégies et réduisent les complexités de problèmes de décision.

    Dans notre travail, nous nous sommes inspiré des logiques dotées de sémantiques d'équipe, qui se basent sur un équipe (un ensemble d'assignation) au lieu d'une seule assignation. De manière formelle, une équipe satisfait une formule atomique si chaque assignation dans l'équipe satisfait la dite formule. Les équipes sont des objets pratiques pour représenter toutes les situations possibles – de sorte que les sémnatiques d'équipe capturent l'imperfection de l'information. Elles permettent également d'exprimer des contraintes sur les valeurs des variables quantifiées. Par exemple, la propriété "la valeur d'une variable x dépend uniquement de la valeur d'une autre variable y" est caractérisée par les équipes dans lesquelles chaque deux assignations qui donnent la même valeur à y, donnent également la même valeur à x. Cependant, les logiques avec sémantiques d'équipe sont souvent indéterminées (il existe des formules ni vraies ni fausses) car les contraintes de dépendance s'appliquent uniquement aux variables qui ont le même type de quantificateur (soit existentiel ou universel).

    L'idée centrale de notre travail est de remplacer les sémantiques d'équipe par des sémantiques hyperteam, où une hyperteam est un ensemble d'équipes. Cette approche permet d'exprimer la dépendance de manière compositionnelle avec un traitement symétrique des quantificateurs existentiels et universels. Pour commencer, nous avons appliqué cet approche à plusieurs logiques : tout d'abord, aux langages du premier ordre en concevant une logique Alternating Dependence/Independence Friendly (ADIF), puis à la Logique Temporelle Propositionnelle Quantifiée (QPTL). Ensuite, nous avons adapté les sémantiques hyperteam pour le raisonnement stratégique en considérant des plans (séquences d'actions), des objets qui sont beaucoup plus simples que les stratégies, comme citoyens de premier rang de la logique.

    Enfin, à part nos contributions sur les sémantiques hyperteam pour diverses logiques, nous développons un nouveau genre de jeux avec des retards entre les actions des joueurs, qui généralise les Jeux de Retard et qui offre une autre façon d'exprimer les dépendances entre les stratégies dans les jeux à plusieurs joueurs.

**ATTENTION dans le cadre du plan VIGIPIRATE : l’accès du public à cette soutenance est contraint à une inscription préalable obligatoire auprès de Sophie MAUPILE (sophie [*] maupileirisa [*] fr)
L’accès ne sera pas autorisé sans inscription préalable. Par ailleurs, les visiteurs ne porteront ni bagage ni sac.**