Raisonnement stratégique avec dépendances : logique d'hyperteam, stratégies réalisables, matrices de dépendance

Strategy Logic (SL for short) has been introduced by Chatterjee, Henzinger and Piterman as a logic to reason about strategies. This powerful setting can express complex strategic notions like the existence of a Nash equilibrium in a game or the existence of a defensive strategy, etc. However, this expressiveness comes with a price as the associated model-checking problem has a nonelementary complexity and the satisfiability problem is undecidable. A careful analysis relates this high complexity with the monolithic nature of strategy quantifiers in SL, where strategies are the first lass citizen of the logic. Consequently, in a formula, a quantified strategy not surprisingly depends on all strategy quantified before, but on their entirety which include counter-factuals and future decisions. This monolithic feature of SL-quantifiers prevents from enforcing strategies to depend only .g. on the history of the current play and may lead to solutions with unrealizable strategies, i.e. hat cannot be implemented. It is therefore reasonable to investigate new semantics/new logics that guarantee the realizability of strategies and ideally that reduce decision problem complexities. In our work, we took inspiration from logics with so-called team semantics, that rely on a team (a set of assignments) instead of a single assignment. Formally, a team satisfies an atomic formula if every assignment in the team satisfies the said formula. Teams are convenient objects to represent all possible situations – so that the team semantics captures imperfect information. They also enable to express constraints on the quantified variable values. For instance, property "the value of a variable x depends only on the value of another variable y" is characterized by teams in which every two assignments giving the same value to y, also give the same value to x. However, logics with team semantics generally lead to undeterminacy (there are formulas neither true nor false) because dependency constraints apply only to variables with the same quantifier-type (either existential or universal).The core idea of our work is to replace team semantics by hyperteam semantics, where a hyperteam is a set of teams. This approach enables to express dependence in a compositional manner with symmetric treatment of existential and universal quantifiers. For a start, we successfully apply the approach to several logical setting: first, to first-order-like languages by designing Alternating Dependence/Independence Friendly Logic (ADIF), and second to Quantified Propositional Temporal Logic (QPTL). Next, we adapt hyperteam semantics to strategic reasoning by considering plans (sequences of actions), objects that are much simpler than strategies, as first-class citizens of the logic. Aside our contributions on hyperteam semantics for various logics, we develop a setting with a new kind of games with delays between player actions, that generalizes Delay Games, and that offers another way to express dependencies between strategies in multi-player games.