Reasoning About Agents That May Know Other Agents’ Strategies

1 Introduction

Reasoning about strategic abilities of agents and groups of agents is a topic of great interest in the formal study of multiagent systems. To that end many logics have been introduced, such as Game Logic [Pauly and Parikh, 2003], STIT [Herzig and Lorini, 2010], and ATL [Alur et al., 2002].

Among these logics, Strategy Logic (SL) [Chatterjee et al., 2010; Mogavero et al., 2014] has proved very successful in recent years, as it combines a natural syntax with high expressive power that allow it to easily express complex gametheoretic notions such as existence of Nash equilibria. Its model checking problem is decidable, and model-checking algorithms can usually be used to synthesize strategies that satisfy a given specification. Because imperfect information is a crucial aspect of multi-agent systems, SL has recently been extended to take into account imperfect information [Berthon et al., 2021] and allow for epistemic reasoning [Maubert and Murano, 2018; Belardinelli et al., 2020].

As discussed in [Maubert and Murano, 2018], defining the semantics of knowledge in a strategic context involves subtleties with far-reaching consequences, that have often gone unheeded. Two semantics exist in the literature, and most works adopt one or the other without mentioning it. One corresponds to agents that do not know each other's strategies (called uninformed semantics in [Maubert and Murano, 2018]), while the other corresponds to agents who know everyone's strategies (informed semantics). The former is used in all existing epistemic extensions of ATL and SL (e.g., [van der Hoek and Wooldridge, 2003; Jamroga and van der Hoek, 2004; Guelev et al., 2011; Belardinelli et al., 2017b]), while the latter is adopted in works on distributed synthesis [van der Meyden and Wilke, 2005] and knowledge-based policies in POMDPs [Saffidine et al., 2018].

Intuitively, the uninformed semantics corresponds to situations where agents do not collaborate, or cannot communicate information about their strategies, and have no a priori knowledge of how other agents behave. On the other hand, the informed semantics corresponds to situations where the strategies followed by each agent are common knowledge. Knowing others' strategies gives additional power to agents, as it allows them to infer more information than what they learn from their observations alone. One can think for instance of the Hanabi card game, where by knowing how other players choose their actions, one can interpret them and infer valuable information. However, this refined notion of knowledge comes at a price in terms of computational complexity.

Indeed some problems are decidable with the uninformed semantics and undecidable with the informed one. This is the case for distributed synthesis. This central problem in multi-agent systems is, in general, undecidable, already for simple reachability objectives without epistemic content [Peterson et al., 2001]. But it becomes decidable if there is a hierarchy of information among agents, or when all actions are observed similarly by all agents (see [Berthon et al., 2021] for a discussion). When objectives are no longer purely temporal but can also refer to knowledge, distributed synthesis for systems with hierarchical information remains decidable with the uninformed semantics of knowledge [Puchala, 2010], but it becomes undecidable for the informed semantics [van der Meyden and Wilke, 2005]. This gives even more reason to consider carefully, when studying a system, the assumptions made on the knowledge agents have of each other's strategies.

Part of these results have been generalized to logics for strategic reasoning that capture distributed synthesis, but only for the uninformed semantics. Decidability has been generalized to an epistemic extension of SL in the case of hierarchical information [Maubert and Murano, 2018], and decidability in the case of public actions has been generalized to epistemic extensions of ATL [Belardinelli et al., 2017b] and SL [Belardinelli et al., 2020]. However no result exists for the informed semantics which, as far as we know, has never been formalized in the context of logics for strategic reasoning.

Contribution. We address this issue and propose a novel semantics of SL with imperfect information and epistemic operators (SLK) in which one can specify, for each agent, the set of agents whose strategy she is informed of. This allows us to capture the case where all agents know everyone's strategies (informed semantics) and the case where no one knows anyone else's strategy (uninformed semantics), as well as intermediate situations (for instance, some agents may be allowed to privately communicate their strategies). We illustrate in detail the impact that knowing others' strategies has on the agents' knowledge as well as on their strategizing power. Doing so, we also shed light on an inconsistency in existing semantics of SL with knowledge, which is solved by our semantics. We then show that for the new semantics, model checking SLK is already undecidable under hierarchical information, but is decidable when all actions are public.

2 SLK with Informed Semantics

Fix AP a finite set of atomic propositions, Ag a finite set of agents, and Var a finite set of variables.

2.1 Syntax

We consider the flat fragment of SL with Boolean Goals [Mogavero et al., 2014] extended with knowledge operators. This simple syntax allows us to focus on the most important aspects of the new semantics, avoiding technical issues that would arise with the full syntax of SL and diminish the clarity of the exposition (see Remark 2 for more detail).

Definition 1. The syntax of SLKinf[BG] is given by the following grammar:

where p ∈ AP, s ∈ Var, ¯ s ∈ Ag → Var×{〈〉, []} and a ∈ Ag.

X and U are the temporal operators "next" and "until", ∃s is the existential quantifier on strategies, and Ka is the individual knowledge operator for agent a. The group binding (Ag, ¯ s) assigns to each agent a strategy variable and a symbol indicating how the uniformity constraint should be treated. Intuitively, 〈〉 (resp. []) indicates a strategy that was quantified existentially (resp. universally). We may write a group binding as a sequence of individual bindings 〈a1, s1〉 . . . [an, sn], where symbols 〈〉 and [] are split and used as delimiters.

We use abbreviations ⊤ = p ∨ ¬p, ⊥= ¬⊤ and ϕ → ϕ′ = ¬ϕ∨ϕ′ for boolean connectives, Fϕ = ⊤Uϕ, Gϕ = ¬F¬ϕ for temporal operators, and finally ∀s.ϕ = ¬∃s.¬ϕ.

A variable s appears free in a formula ϕ if it appears out of the scope of a strategy quantifier, and an agent a appears free in ϕ if a temporal operator (either X or U) appears in ϕ out of the scope of any binding (in which case all agents are free, since group bindings treat all agents at once). We let free (ϕ) be the set of variables and players that appear free in ϕ. If free (ϕ) is empty, ϕ is a sentence.

2.2 Models

We present concurrent game structures with imperfect information on both positions and actions. Towards our definition of the informed semantics, we specify for each agent a a set of agents Aa whose strategies agent a is informed of.

Definition 2. A concurrent game structure (CGS) is a tuple G = (Ac, V,E, ℓ, Vι, {∼a}a∈Ag, {Aa}a∈Ag) where Ac is a finite set of actions, V is a finite set of positions, E : V × Ac Ag → V is a transition function, ℓ : V → 2AP is a valuation function, Vι ⊆ V is a set of initial positions, ∼a ⊆ (V × V ) ∪ (Ac × Ac) is an equivalence relation called an observation relation, and Aa ⊆ Ag is the set of agents whose strategies agent a is informed of.

As in [Puchala, 2010] we consider equivalence relations on positions and actions. This, together with the inclusion of actions in histories (see below), allows us to model public actions in a very natural way.

Joint actions. In a position v ∈ V , each player a chooses an action αa ∈ Ac and the game proceeds to position E(v,α), where α ∈ Ac Ag stands for the joint action (αa )a∈Ag. Given a joint action α = (αa )a∈Ag and a ∈ Ag, we let αa = αa .

Histories, plays and strategies. A history (resp. play) is a finite (resp. infinite) sequence of positions and joint actions ρ = v0α1v1 . . . αnvn (resp. π = v0α1v1 . . .) such that v0 ∈ Vι and for all i with 0 ≤ i < n (resp. i ≥ 0), E(vi, αi+1) = vi+1. For a history ρ = v0α1v1 . . . αnvn we let last(ρ) = vn and |ρ| = n. For a play π = v0α1v1 . . . and i ≥ 0, we write π≤i = v0 . . .αivi for its prefix history ending at position i. We define ρ≤i similarly for histories ρ when i ≤ |ρ|. We let Hist be the set of histories. A strategy is a function σ : Hist → Ac, and we let Str be the set of all strategies.

Assignments. An assignment χ : Ag ∪ Var ⇀ Str is a partial function assigning strategies to agents and variables. Given a tuple of strategies ¯σ ∈ Str Ag , χ[Ag ↦→ ¯σ] is the assignment that maps each agent a to ¯σa , and is equal to χ on variables; similarly, χ[s ↦→ σ] is the assignment that maps variable s to σ and is otherwise equal to χ. When χ is defined for all agents and variables we call it total. Given a total assignment χ and a set of agents A ⊆ Ag, we let χ ↾A be the restriction of χ to A ∪ Var. A history ρ = v0α1 . . . αnvn is consistent with χ if, for every i < n and agent a in the domain of χ, αai+1 = χ(a)(ρ≤i).

Outcomes. For a total agent assignment χ and a history ρ, we let Out(χ, ρ) be the only play π that extends ρ consistently with χ: π = ρ·α1v1α2v2 . . . where for all i ≥ 0 and a ∈ Ag, αai+1 = χ(a)(π≤|ρ|+i) and vi+1 = E(vi, αi+1).

Indistinguishability. Two positions v, v′ are indistinguishable to agent a if v ∼a v′ , and similarly for actions. Two joint actions α and β are indistinguishable to agent a, written α ∼a β, if they are component-wise indistinguishable, i.e., if αb ∼a βb for each b ∈ Ag.

Synchronous perfect recall. We consider agents that remember their observations of all past positions and actions. Each observation relation ∼a is thus extended to histories as follows: given two histories ρ = v0α1 . . .αnvn and ρ′ = v′0α′1 . . .α′mv′m we write ρ ∼a ρ′ if m = n, vi ∼a v′i for all i ∈ {0, . . . , n}, and αi ∼a α′i for all i ∈ {1, . . . , n}.

2.3 Informed Semantics

We now define the informed semantics.

Informed perfect recall. To model agents that know some of the agents' strategies, we refine the observation relation on histories as follows. Let χ be a total assignment, a an agent and Aa the subset of agents whose strategies a knows. Two histories ρ and ρ′ are indistinguishable for agent a, written ρ ∼χa ρ′ , if the following two conditions hold:

Given an agent a and total agent assignment χ, we say that a strategy σ is ∼χa -uniform if for all histories ρ and ρ′ such that ρ ∼χa ρ′ it holds that σ(ρ) = σ(ρ′ ).

Remark 1. Relation ∼χa is not an equivalence relation (it is not reflexive): histories inconsistent with χ ↾Aa are not related to any history; it is an equivalence relation plus isolated points. The only impact this has on the semantics concerns nested knowledge operators, on which it has interesting consequences that we do not discuss here for lack of space.

Indistinguishable assignments. When evaluating an epistemic formula Kaϕ in a history ρ and assignment χ, existing variants of SL with knowledge such as [Maubert and Murano, 2018] and [Belardinelli et al., 2017a] evaluate ϕ in all equivalent histories ρ′ ∼a ρ with the same assignment χ. While quantifying on equivalent histories for the usual (uninformed) relation ∼a models agents that do not know the strategies being used, fixing the assignment χ indicates on the other hand agents that know all agents' strategies. As a consequence of this clash, this semantics neither properly captures the knowledge of agents who are unaware of each other's strategies, nor does it properly model the knowledge of agents who do know each other's strategies, as we show in the next section.

To remedy this we introduce an equivalence relation on assignments. Two assignments χ and χ′ are indistinguishable to agent a, written χ ∼a χ′ , if they agree on all variables, and on the agents' strategies that a is informed of. Formally, χ ∼a χ′ if χ′ ↾Aa = χ↾Aa . The semantics of knowledge will quantify over all equivalent histories and assignments.

Interpreting strategy quantification. In introducing imperfect information to Strategy Logic, it is difficult to determine for whom a strategy should be uniform, at the level of strategy quantification. One solution is to specify it explicitly, as in [Berthon et al., 2021; Maubert and Murano, 2018]. Another is to require that it be uniform for all agents that are bound to it after the quantification, as in [Belardinelli et al., 2020]. However neither of these solutions can be used to define the informed semantics. Indeed, the informed perfectrecall relation ∼χa depends on the assignment χ, which is only known after all agents have been bound to their strategy.

We thus propose a new way of interpreting the uniformity of strategies: instead of putting the uniformity constraint at the level of strategy quantification, we postpone it until after the group binding. In addition to allowing for a natural definition of the informed semantics, it is also a neat solution to defining the semantics of SL with imperfect information, independent of the matter of informed knowledge.

There are two dual ways of dealing with the uniformity constraint. Either we require that the strategy being assigned should be uniform and the remaining subformula should hold, or we say that if the strategy being assigned is uniform, then the subformula should hold. The first case corresponds to existentially quantified strategies, the second to universally quantified ones. Given a group binding (Ag, ¯ s), we let Ag〈〉 ¯ s = {a ∈ Ag | ¯ s(a) = (s, 〈〉) for some s} and Ag[] ¯ s = {a ∈ Ag | ¯ s(a) = (s, []) for some s}.

Definition 3. Let G = (Ac, V,E, ℓ, Vι, {∼}a∈Ag, {Aa}a∈Ag) be a CGS, χ a total assignment, ρ a history and ϕ an SLKinf[BG]-formula. We define G, χ, ρ |= ϕ as follows:

We explain the case for the binding operator, which is the novelty of this semantics. The idea is that the two dual bindings 〈〉 and [] are used so that the first line restricts universal quantifications to uniform strategies by ignoring those that are not, while the second line forces existential quantifiers to pick uniform strategies. In both cases, uniformity of strategies is evaluated with respect to informed perfect recall.

The semantics of a sentence ϕ does not depend on χ, and we write G, vι |= ϕ if G, χ, vι |= ϕ for some χ.

Public actions. A CGS has public actions if for all α ∈ Ac and a ∈ Ag, ∼a ∩ Ac × Ac is the identity relation, meaning that all agents observe all actions perfectly.

Hierarchical information. A CGS has hierarchical information if there exists an enumeration Ag = {a1, . . . , an} of the agents such that ∼ai+1 ⊆∼ai for all 1 ≤ i < n.

Remark 2. The reason why we base our logic on the flat fragment of SL with Boolean Goals is twofold. First, to express the uniformity constraint on strategies for the informed semantics, we need to know the strategies that will be used by all agents. The group binding of the Boolean Goals fragment makes this possible. Second, if agents can change strategy after time 0, as is possible in the non-flat fragment, it becomes unclear how to define the informed semantics: should agents know only the current strategy of other agents, and believe that they have been using it from the start? Or should they know the sequence of strategies that other agents have used? Both interpretations could be defined and studied, but we leave this matter for future work. Besides, the flat fragment of SL with Boolean Goals is already very expressive and can express, for instance, distributed synthesis, rational synthesis, and existence of Nash equilibria.

3 Illustrating the Informed Semantics

We discuss some aspects of our semantics, that we illustrate in the classic scenario of matching pennies.

Consider the game of matching pennies G illustrated in Figure 1, where the players are called 1 and 2 (loops on final positions are omitted). Each player has a coin that only they can see. First, player one places her hidden coin heads or tails up, then player 2 does the same with her hidden coin. The proposition m stands for the coins matching. We suppose that the players only observe their own actions, so v3 ∼1 v4, v5 ∼1 v6, v1 ∼2 v2, v3 ∼2 v5, and v4 ∼2 v6. In this example we omit the action names in the histories without ambiguity.

3.1 Impact on Knowledge

We first illustrate how restricting the quantification on equivalent plays to those that are consistent with known strategies affects the knowledge of the agents. The usual semantics for the knowledge operator in epistemic extensions of SL, that we can find for instance in [Maubert and Murano, 2018] and [Belardinelli et al., 2020], and that we shall refer to as "uninformed semantics" and denote |=u, is the following:

It differs from our semantics in two respects: (i) it uses the usual "uninformed" equivalence relation ∼a on histories instead of the informed one ∼χa , and (ii) it does not quantify over indistinguishable assignments.

To illustrate the first difference (i), consider the formula

which means that no matter which strategies are used, in the end player 1 knows whether the coins match or not. With the uninformed semantics it clearly does not hold, as player 1 does not observe player 2's coin (so that v0v1v3 ∼1 v0v1v4 and v0v2v5 ∼1 v0v2v6), nor does she know her strategy, so G, v0 ̸|=u α. Now with the informed semantics, it is enough to assume that player 1 knows player 2's strategy (i.e. 2 ∈ A1) to make the formula true. Indeed, for any strategies s1 and s2 for players 1 and 2, the only history that player 1 considers possible with the uninformed relation ∼1 besides the actual outcome, is not consistent with strategy s2 and is thus discarded by ∼χ1 . For instance if the outcome is v0v1v3, i.e. s1 and s2 are the strategies that play heads, then the only history equivalent for ∼1 is v0v1v4, in which player 2 plays tails, which is not consistent with s2. So G, v0 |= α.

We now illustrate the second difference (ii). Since the assignment does not impact the truth value of a formula without temporal operators, the only case in which considering equivalent assignments makes a difference is for formulas that involve knowledge about the future. So consider formula

which means that for any pair of strategies s1 and s2, player 1 knows, before any move is made, whether in the end the coins will match. Intuitively this can only be the case if player 1 knows the strategies of both players. We check that indeed, with our semantics, the formula holds if we assume that A1 = {1, 2}, and it does not if A1 ⊊ {1, 2}. Fix a pair of strategies (s1, s2), let χ assign s1 to 1 and s2 to 2, and assume for instance that these strategies lead to matching coins, i.e. G, χ, v0 |= XXm. First, note that the only history indistinguishable from v0 via ∼χ1 is v0. Now if A1 ⊊ {1, 2}, meaning that player 1 does not know one of the strategies, then there exists at least one assignment χ′ ∼1 χ that has a different outcome, i.e. such that G, χ′ , v0 |= XX¬m. The same reasoning can be made if (s1, s2) lead to coins that do not match. As a result, G, v0 ̸|= β. Now assume that player 1 knows both strategies, i.e., A1 = {1, 2}. For any assignment χ, χ ∼1 χ′ implies that χ′ = χ. It follows that either G, χ, v0 |= K1XXm, if G, χ, v0 |= XXm, or G, χ, v0 |= K1XX¬m, if G, χ, v0 |=XX¬m. So G, v0 |= β.

One can see that also with the usual "uninformed" semantics, it holds that G, v0 |= β: indeed, since it only considers the actual assignment, it corresponds in the previous paragraph to the case where A1 = {1, 2}, i.e., the case where 1 knows both strategies. This is in contrast with what we illustrated with point (i), where the uninformed semantics corresponds to agents that do not know each other's strategies, and it demonstrates an inconsistency in the usual semantics. The semantics we propose solves this problem.

3.2 Impact on Strategizing Power

Our semantics also makes a difference for agents' strategic ability. Consider the following alternate "uninformed" semantics, which uses relation ∼a instead of ∼χ′ a :

Consider again the example from Figure 1, and assume that player 2 knows player 1's strategy, i.e., 1 ∈ A2. Formula

means that player 2 has a strategy to ensure that the coins match. Knowing player 1's strategy, intuitively this should be true: if player 1 plans to play heads, then play heads, otherwise play tails. However with the semantics that uses the usual "uninformed" notion of uniformity, this formula does not hold: indeed, because v1 and v2 are indistinguishable to player 2, any ∼2-uniform strategy s2 must play the same action in histories v0v1 and v0v2. If it is heads, then the coins will not match if 1 plays tails, and vice versa. So G, v0 ̸|=u γ.

However with our informed semantics, the formula holds. Indeed consider the strategy s2 such that s2(v0.v1) = h and s2(v0.v2) = t. Clearly it ensures that the coins match. We just need to see that it is also uniform for the informed notion of uniformity. Let s1 be a strategy and χ = [1 ↦→ s1, 2 ↦→ s2]. To see that s2 is ∼χ2 -uniform, observe that either v0v1 or v0v2 is not consistent with s1. Therefore it is not the case that v0v1 ∼χ2 v0v2, and s1 does not have to assign the same action in both histories. As a result, G, v0 |= γ.

4 Model Checking SLKinf[BG]

We consider the model-checking problem for SLKinf[BG] which consists in deciding, given a CGS G, an initial position vι ∈ Vι and an SLKinf[BG] sentence Φ, whether G, vι |= Φ.

4.1 Undecidability for Hierarchical Information

It is proved in [van der Meyden and Wilke, 2005] that distributed synthesis for LTL with knowledge is undecidable, even for systems with hierarchical information. The setting there corresponds to agents that know the strategy of everyone but the environment, which we can model in our informed semantics. Since distributed synthesis for LTLK objectives is expressible in SLKinf[BG], we obtain that:

Theorem 1. Model checking SLK is undecidable, even when restricted to CGS with hierarchical information.

4.2 Decidability for Public Actions

We now show that model checking SLKinf[BG] is decidable when all actions are public. This is in line with the results in [van der Meyden and Wilke, 2005], where the informed semantics is used implicitly, and distributed synthesis for LTLK is shown to be decidable on broadcast systems, which are very close to our CGS with public actions.

As in [Laroussinie et al., 2015; Berthon et al., 2021; Belardinelli et al., 2020], we solve the model-checking problem by reducing it to the model-checking problem for QCTL∗ , for which we briefly recall the syntax and semantics.

Definition 4. The syntax of QCTL∗ is defined as follows:

where p ∈ AP.

Note that the set AP may not be the same as in the previous section (in the reduction from SLKinf to QCTL∗ we will use a bigger finite set of atomic propositions for QCTL∗ ).

We consider the tree semantics for QCTL∗ , where formulas are evaluated on infinite trees, typically representing unfoldings of finite Kripke structures.

Trees. Let Σ be a finite alphabet. An infinite tree over Σ and AP is a mapping t : Σ∗ → 2AP . An element x ∈ Σ∗ is a node, the empty word ϵ is the root, a node y is a child of a node x if it is of the form y = x · d with d ∈ Σ, and t(x) is the label of node x. A path λ = x0x1 . . . is an infinite sequence of nodes such that for all i ≥ 0, xi+1 is a child of xi. We let λi = xi denote the node at position i, and λ≥i = xixi+1 . . . is the suffix of λ starting at position i. We say that λ starts in node x0, and let Paths(x) be the set of paths that start in x. The subtree of t rooted in node x is the tree tx : y ↦→ t(x · y). A tree is regular if it has finitely many different subtrees. Finally, given a tree t and an interpretation Xp ⊆ Σ∗ for an atom p ∈ AP, we define the tree

Definition 5. Let t be a tree, x a node and λ a path. The semantics of QCTL∗ is defined as follows (we omit negation and disjunction):

We write t |= ϕ for t, ϵ |= ϕ.

For the rest of this section we fix a CGS G = (Ac, V,E, ℓ, Vι, {∼a}a∈Ag, {Aa}a∈Ag) with public actions and an SLKinf[BG] sentence Φ. The reduction is based on the one in [Belardinelli et al., 2020], where the two main ideas are that when actions are public and transitions deterministic, (1) each history is entirely determined by its initial position and the sequence of joint actions, and (2) two indistinguishable histories share the same sequence of joint actions. Note that only the first point relies on determinism.

We thus work on the tree consisting of all sequences of joint actions. A node x = α1 . . .αn in this tree represents the set of all histories ρ sharing this sequence of joint actions. By point 2 above, two histories that are indistinguishable for some agent are represented by the same node. This makes it possible to check uniformity of strategies locally in the tree.

Formally, let Σ = Ac Ag , and for a node x ∈ Σ∗ and an initial position v ∈ Vι, we let ρxv be the history in G that starts in v and has sequence of joint actions x. This is uniquely defined because the transition function is total and deterministic, and all histories can be written in this form. Point 2 above can be formalized as:

We introduce propositions APact = {pα | α ∈ Ac Ag} that mark in each node the last joint action performed, and propositions APpos = {pν | ν : Vι → V } that indicate the current position ν(vι) given that the initial position was vι. We then define the tree tG over Σ and APact ∪ APpos as

where ν : vι ↦→ last(ρα1...αn vι ). So each node is labeled by exactly one atom in APact and one in APpos. Also, since G is finite, the tree tG is regular.

To keep track of strategies we introduce propositions APstr = {pτs | τ : Vι → Ac and s ∈ Var(Φ)}, where τ is called a local strategy and Var(Φ) is the set of strategy variables in Φ (we assume without loss of generality that each variable is quantified at most once in Φ). Proposition pτs in node x means that on history ρxv , strategy s chooses action τ(v). To represent agents' knowledge we introduce propositions AP≈ = {pa≈ | a ∈ Ag and ≈⊆ Vι × Vι}, where ≈ is called a local observation relation. The intended meaning of pa≈ holding in a node x is that histories ρxv and ρxu are indistinguishable to agent a if and only if v ≈ u. By Lemma 2, indistinguishability relations can be completely characterized by such propositions. To capture the interpretation of "indistinguishable to agent a" corresponding to the informed semantics, these propositions will be placed on the tree after those encoding strategies, and consistently with them.

We define for each subformula ϕ of Φ a QCTL∗ formula [ϕ]Bvι . The translation is parameterized by a mapping B : Ag ⇀ Var that represents the current binding of agents to strategy variables, and a position vι ∈ Vι representing the initial position of the current history. For atomic propositions:

This formula grabs the unique ν for which pν holds in the current node, and checks whether p holds in the current position as indicated by ν given that the initial position is vι. Boolean connectives simply distribute:

For strategic quantification, let {τ1, . . . , τk} be an enumeration of the possible local strategies, with k = |Ac||Vι| . Let

checks that each node is labeled by exactly one local strategy. Next comes the binding operator (Ag, ¯ s), which we represent as a mapping B′ : Ag → Var×{〈〉, []}. Let {a1, . . . , am} be an enumeration of the agents and {≈1, . . . ,≈l} an enumeration of the possible equivalence relations over Vι. For each agent a we define the initial local observation relation ≈ιa =∼a ∩Vι × Vι. Also, given a local observation relation ≈a for agent a (in some node x), a tuple ¯ τ of local strategies for each agent, as well as a next joint action α and resulting current positions ν (in node x·α), we define the updated local observation relation for agent a as ≈′a (≈a, ¯ τ , α, ν) =

This definition means that two histories ρx·α vι and ρx·α uι are indistinguishable for a if ρxvι and ρxuι are indistinguishable (vι ≈a uι), the new positions last(ρx·α vι ) and last(ρx·α uι ) are indistinguishable (ν(vι) ∼a ν(uι)), and for each agent b whose strategy is known to a, the last action αb played by b corresponds to strategy τb in both ρxvι and ρxuι (so ρx·α vι and ρx·α uι are consistent with τb). Given a binding B, we let Ag〈〉 B (resp. Ag[]B ) be the set of agents a such that B(a) = (s, 〈〉) (resp.

(s, [])) for some variable s. Define

where uniqa = AG ∨≈(pa≈ ∧ ∧≈′ ̸=≈ ¬pa≈′ ) checks that each node is marked with one unique local observation relation,

checks that the local observation relation is initially correct and that in each step it is updated correctly, and

checks that strategy s is uniform for agent a, with

For the knowledge operator, let

We are left with the temporal operators:

where α(¯ τ, vι) is the joint action where each agent a plays action τa(vι). Similarly, we let

Lemma 3. For every initial position vι ∈ Vι and every initial binding B, it holds that G, vι |= Φ iff tG |= [Φ]Bvι .

Because model checking QCTL∗ on regular trees is decidable [Laroussinie and Markey, 2014], we obtain that

Theorem 4. Model checking SLKinf on CGS with public actions is decidable.

5 Conclusion and FutureWork

In this work we defined the first semantics for Strategy Logic that can model agents that know other agents' strategies. This semantics reflects the intuitive idea that knowing others' strategies refines agents' knowledge about the system, and increases their ability to strategize. It is also general enough to capture both situations found in the literature, which correspond to the two extreme cases. Two important questions left for future work are the implications of the informed semantics on higher-order knowledge, and trying to extend this new informed semantics to the full syntax of SL.