Comparing variants of strategic ability: how uncertainty and memory influence general properties of games

Alternating-time temporal logic (ATL) is a modal logic that allows to reason about agents’ abilities in game-like scenarios. Semantic variants of ATL are usually built upon different assumptions about the kind of game that is played, including capabilities of agents (perfect vs. imperfect information, perfect vs. imperfect memory, etc.). ATL has been studied extensively in previous years; however, most of the research focused on model checking. Studies of other decision problems (e.g., satisfiability) and formal meta-properties of the logic (like axiomatization or expressivity) have been relatively scarce, and mostly limited to the basic variant of ATL where agents possess perfect information and perfect memory. In particular, a comparison between different semantic variants of the logic is largely left untouched. In this paper, we show that different semantics of ability in ATL give rise to different validity sets. The issue is important for several reasons. First, many logicians identify a logic with its set of true sentences. As a consequence, we prove that different notions of ability induce different strategic logics. Secondly, we show that different concepts of ability induce different general properties of games. Thirdly, the study can be seen as the first systematic step towards satisfiability-checking algorithms for ATL with imperfect information. We introduce sophisticated unfoldings of models and prove invariance results that are an important technical contribution to formal analysis of strategic logics.

1. Note that “always” is not definable from “until” in ATL [48], and has to be added explicitly to the language.

2. We would like to note that it is essential for this work that we do not require a finite set of states or actions. We give a more detailed discussion in Sect. 2.3.

3. An interested reader may observe that the preliminary versions of the semantics (in alternating transition systems) did not assume models explicitly to be finite [7, 8]. However, the authors de facto considered only finite models since they were solely interested in the model checking problem, where the input must be finite.

4. We thank an anonymous JAAMAS reviewer for suggesting this.

5. As commonly done we assume an implicit order on the elements in \({\mathbb{A }\mathrm{gt }} \) allowing to conveniently represent collective strategies as tuples. In our setting where agents are represented by natural numbers the order is apparent. In the general case, a collective strategy for \(A\) is a function that associates individual strategies to the agents in \(A\).

6. The issue is closely related to epistemic feasibility of plans, cf. e.g. [22, 49].

7. The proof in [31] was for the class of finitely branching \(\mathbf{CGS _{\mathbf{}}}\) (with possibly infinite state spaces) but it extends to the case of infinite branching in a straightforward way.

8. The equivalence of \(\mathfrak{M },q\models _{_{{{ IR }}}}\varphi \) and \(T(\mathfrak{M },q),q\models _{_{{{ IR }}}}\varphi \) follows also from the results on alternating bisimulation, cf. [10] for the bisimulation in finite models, and [3] for the general case. We present the construction nevertheless, as it will be adapted in the following sections to the case of imperfect information.

9. We thank an anonymous reviewer of JAAMAS for the excellent terminological suggestion. An \({{{\textit{i}}_{\textit{s}}}{{\textit{R}}}}\) unfolding is not a tree, as it usually consists of several transition trees. On the other hand, it is not a typical forest because the trees are not separate—they are intimately connected by epistemic relations. For the biological Pando, see for example http://en.wikipedia.org/wiki/Pando(tree).

10. The example depicts some simple traps that await a married man if he happens to be absent-minded. If he doesn’t kiss his wife in the morning, he is likely to make her angry. However, if he kisses her more than once, she might get suspicious. It is easy to see that the absent-minded (i.e., memoryless) husband does not have a strategy to survive safely through the morning, though a safe path through the model does exist (\(\lambda =q_0q_1q_1q_1\ldots \)).

The authors would like to express their thanks to Jan Broersen for the argument that triggered this study, Valentin Goranko for discussions on (non-) validity of fixpoint properties in various semantics of ATL, and anonymous reviewers of EUMAS’10, IJCAI’11 and JAAMAS for their valuable remarks. Wojciech Jamroga acknowledges the support of the FNR (National Research Fund) Luxembourg under projects S-GAMES—C08/IS/03 and GALOT—INTER/DFG/12/06.

Authors and Affiliations

1. Department of Informatics, Clausthal University of Technology, Clausthal-Zellerfeld, Germany

   Nils Bulling

2. Computer Science and Communication Research Unit, and Interdisciplinary Centre on Security, Reliability and Trust, University of Luxembourg, Luxembourg, Luxembourg

   Wojciech Jamroga

Corresponding author

Correspondence to Nils Bulling.

Appendix: Proofs

1.1 Proofs of Sect. 4.2

The following Lemma is obvious by the definition of \({{{\textit{i}}_{\textit{o}}{\textit{R}}}} \)-tree unfoldings. It states that that nodes group indistinguishable in the tree unfolding are also group indistinguishable in the model if interpreted as histories.

Lemma 1

Let \(\mathfrak{M }\) be an i \(\mathbf{CGS _{\mathbf{}}}\), \(h_1\) and \(h_2\) two nodes in its \({{{\textit{i}}_{\textit{o}}{\textit{R}}}} \)-tree unfolding, and \(A\subseteq {\mathbb{A }\mathrm{gt }} \) a group of agents. If \(h_1\sim ^{T_o(\mathfrak{M },q)}_A h_2\) then \(h_1\approx ^{\mathfrak{M }}_Ah_2\).

Moreover, we have that all histories indistinguishable in the model are also indistinguishable in the tree if only states reachable from the current state are considered.

Lemma 2

Let \(\mathfrak{M }\) be an i \(\mathbf{CGS _{\mathbf{}}}\), \(A\subseteq {\mathbb{A }\mathrm{gt }} \) and \(h\) a node in \({T_o(\mathfrak{M },q)}\). Then, for all \(h_1,h_2\in \varLambda _{\mathfrak{M }}(last(h))\) we have that

Theorem 2 For every i CGS \(\mathfrak{M }\), state \(q\) in \(\mathfrak{M }\), and \({{\varvec{ATL}}}^{*}\) -formula \(\varphi \) we have:

Proof

We show that, for every node \(h\) in \(T_o (\mathfrak{M },q)\), it holds that \(\mathfrak{M },last(h)\models _{{{\textit{i}}_{\textit{o}}{\textit{R}}}} \varphi \) iff \(T_o (\mathfrak{M },q),h\models _{{{\textit{i}}_{\textit{o}}}{\textit{r}}}\varphi \). Then, the claim follows by Propositions 4 and  5 and for \(h=q\). The proof is done by induction on the structure of \(\varphi \).

Base cases:

• Propositional case: Straightforward.

• Case: \(\varphi \equiv \langle \!\langle {A}\rangle \!\rangle _{_{\!{ }}}\gamma \) where \(\gamma \) contains no nested strategic modalities. “\(\Rightarrow \)”: Suppose that \(\mathfrak{M },last(h)\models _{_{{{ {{{\textit{i}}_{\textit{o}}{\textit{R}}}} }}}}\langle \!\langle {A}\rangle \!\rangle _{_{\!{ }}}\gamma \). So, there is an \({{{\textit{i}}_{\textit{o}}{\textit{R}}}}\)-strategy \(s_A\) such that

  $$\begin{aligned} (\star )\ \forall \lambda \in out_\mathfrak{M }(last(h),s_A): \mathfrak{M },\lambda \models _{_{{{ {{{\textit{i}}_{\textit{o}}{\textit{R}}}} }}}}\gamma . \end{aligned}$$

  We construct the memoryless strategy \(s_A^{\prime }\) in \(T_o(\mathfrak{M },q)\) as follows: \(s_a^{\prime }(\hat{h}h^{\prime })=s_a(last(h)h^{\prime })\) for every \(a\in A\) and \(\hat{h}\) such that \(h\sim ^{T_o(\mathfrak{M },q)}_A\hat{h}\). For all other histories \(h^{\prime \prime }\) (which do not have the form \(\hat{h}h^{\prime }\)) we define \(s^{\prime }_a(h^{\prime \prime })\) arbitrarily but in a uniform way. It is easy to see that \(s_A^{\prime }\) is uniform: For two histories \(h_1=\hat{h}^{\prime }h^{\prime }\) and \(h_2=\hat{h}^{\prime \prime }h^{\prime \prime }\) with \(\hat{h}^{\prime }\sim _A^{T_o(\mathfrak{M },q)} h\) and \(\hat{h}^{\prime \prime }\sim _A^{T_o(\mathfrak{M },q)} h\) and \(h_1\sim ^{T_o(\mathfrak{M },q)}_Ah_2\) we have \(s^{\prime }_A(h_1)=s^{\prime }_A(h_2)\); for, \(h_1\sim ^{T_o(\mathfrak{M },q)}_Ah_2\) implies \(h_1\approx ^{\mathfrak{M }}_Ah_2\) (by Lemma 1) and thus \(s_A(last(h)h^{\prime })=s_A(last(h)h^{\prime \prime })\). By construction of \(s_A^{\prime }\) we have that

  $$\begin{aligned} last(h)q_1q_2\cdots \in out_\mathfrak{M }(last(h),s_A)\text { iff } (h)(hq_1)(hq_1q_2)\cdots \in out_{T_o(\mathfrak{M },q)}(h,s_A^{\prime }). \end{aligned}$$

  Since the valuation of propositions does only depend on the final state of a history and by \((\star )\) we have \(T_o (\mathfrak{M },q),h\models _{{{\textit{i}}_{\textit{o}}}{\textit{r}}}\langle \!\langle {A}\rangle \!\rangle _{_{\!{ }}}\gamma \). \(\Leftarrow \): Suppose we have \(T_o(\mathfrak{M },q),h\models _{_{{{ {{\textit{i}}_{\textit{o}}}{\textit{r}} }}}}\langle \!\langle {A}\rangle \!\rangle _{_{\!{ }}}\gamma \). So there is an \({{\textit{i}}_{\textit{o}}}{\textit{r}} \)-strategy \(s_A\) such that

  $$\begin{aligned} (\star )\ \forall \lambda \in out_{T_o(\mathfrak{M },q)}(h,s_A): T_o(\mathfrak{M },q),\lambda \models _{{{\textit{i}}_{\textit{o}}}{\textit{r}}}\gamma . \end{aligned}$$

  We construct a witnessing \({{{\textit{i}}_{\textit{o}}{\textit{R}}}} \)-strategy \(s_A^{\prime }\) in \(\mathfrak{M }\) as follows: \(s_a^{\prime }(\hat{h})=s_a(hh^{\prime })\) for every \(a\in A\) and \(\hat{h}\) such that \(last(h)h^{\prime }\approx _a^\mathfrak{M }\hat{h}\) and \(last(h)h^{\prime }\in \varLambda _{\mathfrak{M }}^{fin}(last(h))\). We define \(s_a^{\prime }\) arbitrarily for all other histories with the condition to assign the same actions to indistinguishable histories in \(\mathfrak{M }\). The definition of \(s_a^{\prime }\) does only take into account the subtree starting at \(h\). Then, by Lemma 2 we have that strategy \(s_A^{\prime }\) is uniform by construction. Note, that it may differ from \(s_A\) but only for histories which are not realizable given that the initial state is \({ last }(h)\). By construction of \(s_A^{\prime }\), we also have

  $$\begin{aligned} (h)(hq_1)(hq_1q_2)\cdots \in out_{T_o(\mathfrak{M },q)}(h,s_A)\text { iff } last(h)q_1q_2\cdots \in out_\mathfrak{M }(last(h),s^{\prime }_A). \end{aligned}$$

  Since the valuation of propositions does only depend on the final state of a history and by \((\star )\) we have \(\mathfrak{M },last(h)\models _{{{{\textit{i}}_{\textit{o}}{\textit{R}}}}}\langle \!\langle {A}\rangle \!\rangle _{_{\!{ }}}\gamma \).

Induction step:

• Case: \(\varphi \equiv \psi _1\wedge \psi _2\). Straightforward.

• Case: \(\varphi \equiv \lnot \psi \). \(\mathfrak{M },last(h)\models _{_{{{ {{{\textit{i}}_{\textit{o}}{\textit{R}}}} }}}}\lnot \psi \) iff not \(\mathfrak{M },last(h)\models _{_{{{ {{{\textit{i}}_{\textit{o}}{\textit{R}}}} }}}}\psi \) iff (by induction hypothesis) not \(T_o(\mathfrak{M },q),h\models _{_{{{ {{{\textit{i}}_{\textit{o}}{\textit{R}}}} }}}}\psi \) iff \(T_o(\mathfrak{M },q),h\models _{_{{{ {{{\textit{i}}_{\textit{o}}{\textit{R}}}} }}}}\lnot \psi \).

• Case: \(\varphi \equiv \langle \!\langle {A}\rangle \!\rangle _{_{\!{ }}}\gamma \). By induction hypothesis we have for each history \(h\) in \(T_o(\mathfrak{M },q)\) and each strict state-subformula \(\varphi ^{\prime }\) of \(\gamma \) that \(\mathfrak{M },{ last }(h)\models _{{{\textit{i}}_{\textit{o}}{\textit{R}}}} \varphi ^{\prime }\) iff \(T_o (\mathfrak{M },q),h\models _{{{\textit{i}}_{\textit{o}}}{\textit{r}}}\varphi ^{\prime }\). For any maximal strict subformula \(\varphi ^{\prime }\) of \(\varphi \) we label all states \(h\) in \(T_o(\mathfrak{M },q)\) and states \(last(h)\) in \(\mathfrak{M }\) with a new proposition \(\mathsf{{p} }_{\varphi ^{\prime }}\) iff \(\varphi ^{\prime }\) holds in this very state. Then, we replace each \(\varphi ^{\prime }\) in \(\varphi \) with proposition \(\mathsf{{p} }_{\varphi ^{\prime }}\). This yields a formula without nested modalities and the claim follows by induction.\(\square \)

1.2 Proofs of Sect. 4.3

In this section we give all details needed to prove Theorem 3. The structure of the proof is shown in Fig. 9.

The following lemma is essential to show that truth in \({{{\textit{i}}_{\textit{s}}}{{\textit{R}}}} \)-pando-like models is insensitive to the type of available strategies (memoryless vs. perfect recall). The lemma is needed to show that a uniform perfect recall strategy in the pando-like model gives rise to a uniform memoryless strategy. Therefore, we have to show that two states which are indistinguishable in the model give rise to indistinguishable histories.

Lemma 3

Let \(\mathfrak{M }\) be an \({{{\textit{i}}_{\textit{s}}}{{\textit{R}}}} \)-pando like i \(\mathbf{CGS _{\mathbf{}}}\) and \(q,q_1,\hat{q}_1,q_2,\hat{q}_2\in { St } \) where \(q_i\) is reachable from \(\hat{q}_i\), i.e. \({{\rho _{}}{(\hat{q}_i,q_i)}}\ne \epsilon \), for \(i=1,2\). Moreover, let \(\hat{q}_1\sim _b^{\mathfrak{M }}q\sim _c^{\mathfrak{M }}\hat{q}_2\) for some \(b,c\in A\) and \(q_1\sim _a^\mathfrak{M }q_2\). Then, we have that \({{\rho _{}}{(\hat{q}_1,q_1)}}\approx _a^\mathfrak{M }{{\rho _{}}{(\hat{q}_2,q_2)}}\).

General setting of the proof of Proposition 7

Full size image

Proof

The setting is illustrated in Fig. 15. In the following we consider all possibilities how \(q\), \(\hat{q}_1\), \(\hat{q}_2\), \(q_1\), and \(q_2\) can be located. We recall that \({{\rho _{\mathfrak{M }_k}}{(q^{\prime })}}=q^{\prime }\) means that \(q^{\prime }\) is the root node of model \(\mathfrak{M }_k\). We assume that \(k,l,m\in I\) where \(I\) is the index set from Definition 16.

• Case 1: \(q_1\hat{\sim }_a q_2\). Let \(q_1\in \mathfrak{M }_k\) and \(q_2\in \mathfrak{M }_l\), \(k\ne l\).

  • Case 1.1: \({{\rho _{\mathfrak{M }_k}}{(q_1)}}=q_1\). That is, \(q_1\) is the root node of \(\mathfrak{M }_k\). We have \(\hat{q}_1=q_1\sim _b^\mathfrak{M }q\). Then, by Definition 16.5 \(|{{\rho _{}}{(\hat{q}_2)}}|=|{{\rho _{}}{(q_2)}}|\) which implies \(\hat{q}_2=q_2\). Hence, we have \({{\rho _{\mathfrak{M }_k}}{(\hat{q}_1,q_1)}}= q_1\approx _a^\mathfrak{M }{{\rho _{\mathfrak{M }_l}}{(\hat{q}_2,q_2)}}=q_2\) and are done.

  • Case 1.2 \({{\rho _{\mathfrak{M }_k}}{(q_2)}}=q_2\). Analogously to Case 1.1.

  • Case 1.3 \({{\rho _{\mathfrak{M }_k}}{(q_1)}}\hat{\approx }_a^\mathfrak{M }{{\rho _{\mathfrak{M }_l}}{(q_2)}}\) and both \(q_1\) and \(q_2\) are not root nodes.

    • Case 1.3.1 \(\hat{q}_1\hat{\sim }_b^\mathfrak{M }q\). Let \(q\in { St } _m\) with \(m\ne k\).

      • Case 1.3.1.1 \({{\rho _{\mathfrak{M }_k}}{(\hat{q_1})}}=\hat{q}_1\). Then, \(\hat{q}_1\hat{\sim }_a^\mathfrak{M }q^{\prime }\) where \(q^{\prime }\in { St } _l\) is the root node of \(\mathfrak{M }_l\). But then, by Definition 16.5 we have \(|{{\rho _{}}{(q^{\prime })}}|=|{{\rho _{}}{(\hat{q}_2)}}|\) and thus \({{\rho _{\mathfrak{M }_l}}{(\hat{q}_2)}}=\hat{q}_2\). This proves that \({{\rho _{\mathfrak{M }_k}}{(\hat{q}_1,q_1)}}\approx _a^\mathfrak{M }{{\rho _{\mathfrak{M }_l}}{(\hat{q}_2,q_2)}}\).

      • Case 1.3.1.2 \({{\rho _{\mathfrak{M }_m}}{({q})}}={q}\). Again, by Definition 16.5 following the same reasoning as in Case 1.3.1.1 we obtain \({{\rho _{\mathfrak{M }_l}}{(\hat{q}_2)}}=\hat{q}_2\). Showing that \({{\rho _{\mathfrak{M }_k}}{(\hat{q}_1,q_1)}}\approx _a^\mathfrak{M }{{\rho _{\mathfrak{M }_l}}{(\hat{q}_2,q_2)}}\).

      • Case 1.3.1.3 \({{\rho _{\mathfrak{M }_k}}{(\hat{q}_1)}}\hat{\approx }^\mathfrak{M }_a{{\rho _{\mathfrak{M }_m}}{(q)}}\) and neither \(\hat{q}_1\) nor \(q\) are root nodes. Then, we either have that \(l=m\) and \({{\rho _{\mathfrak{M }_l}}{(\hat{q}_2)}}{\approx }_a^\mathfrak{M }{{\rho _{\mathfrak{M }_l}}{(q)}}\) which implies that \({{\rho _{\mathfrak{M }_k}}{(\hat{q}_1,q_1)}}\hat{\approx }_a^\mathfrak{M }{{\rho _{\mathfrak{M }_l}}{(\hat{q}_2,q_2)}}\). Or, \(l\ne m\) and we have to distinguish again two cases. If \(\hat{q}_2\) is the root node; then, it is connected with the root \(q^{\prime }\in { St } _k\) of \(\mathfrak{M }_k\) by \(\sim _a^\mathfrak{M }\). We have \(q^{\prime }\sim _a^\mathfrak{M }\hat{q}_2\sim _c^\mathfrak{M }q\sim _b^\mathfrak{M }\hat{q}_1\) and by Definition 16.5 it must be the case that \(|{{\rho _{}}{(q^{\prime })}}|=|{{\rho _{}}{(\hat{q}_1)}}|\). Contradiction. Hence, we can safely assume that \(\hat{q}_2\) is not a root. Then, \({{\rho _{\mathfrak{M }_l}}{(\hat{q}_2)}}{\approx }_c^\mathfrak{M } {{\rho _{\mathfrak{M }_m}}{(q)}}\approx _b^\mathfrak{M }{{\rho _{\mathfrak{M }_k}}{(\hat{q}_1)}}\). So, all these states are on the same height level which implies that \({{\rho _{\mathfrak{M }_k}}{(\hat{q}_1,q_1)}}\approx _a^\mathfrak{M }{{\rho _{\mathfrak{M }_l}}{(\hat{q}_2,q_2)}}\).

    • Case 1.3.2 \(\hat{q}_2\hat{\sim }_a^\mathfrak{M }q\). Analogously to Case 1.3.1.

    • Case 1.3.3 \(\hat{q}_1\sim _a^{\mathfrak{M }_k} q\) or \(\hat{q}_2\sim _a^{\mathfrak{M }_l} q\). In each of these cases it means that either \(q\not \in { St } _k\) or \(q\not \in { St } _l\) as \(k\ne l\). Case 1.3.1 or Case 1.3.2 applies.

• Case 2: \(q_1\sim _a^{\mathfrak{M }_k} q_2\). Then, by definition \(k=l\) and \({{\rho _{\mathfrak{M }_k}}{(q_1)}}\approx _a^\mathfrak{M }{{\rho _{\mathfrak{M }_k}}{(q_2)}}\).

  • Case 2.1: \(q\in { St } _k\). We have \(|{{\rho _{\mathfrak{M }_k}}{(\hat{q}_1)}}|=|{{\rho _{\mathfrak{M }_k}}{({q})}}|=| {{\rho _{\mathfrak{M }_k}}{(\hat{q}_2)}}|\) which follows from the assumption \(\hat{q}_1\sim _b^{\mathfrak{M }_k} q\sim _c^{\mathfrak{M }_k}\hat{q}_2\); hence also, \({{\rho _{\mathfrak{M }_k}}{(\hat{q}_1,q_1)}}\hat{\approx }_a^\mathfrak{M }{{\rho _{\mathfrak{M }_k}}{(\hat{q}_2,q_2)}}\).

  • Case 2.2: \(q\in { St } _m,\ m\ne k\). Then, we have \(\hat{q}_1\hat{\sim }_b^\mathfrak{M }q\hat{\sim }_c^\mathfrak{M }\hat{q}_2\). Again we have to distinguish the different cases how \(q\) is connected to \(\hat{q}_1\) and \(\hat{q}_2\) respectively.

    • Case 2.1.1 \({{\rho _{\mathfrak{M }_m}}{(q)}}=q\). That is, we assume that \(q\) is a root node. By Definition 16.5 we have \(|{{\rho _{}}{(\hat{q}_1)}}|=|{{\rho _{}}{(\hat{q_2})}}|\) and \({{\rho _{}}{(\hat{q}_1,q_1)}}\approx _a^\mathfrak{M }{{\rho _{}}{(\hat{q}_2,q_2)}}\) follows.

    • Case 2.1.2 \({{\rho _{\mathfrak{M }_m}}{(q)}}\!\ne \! q\). We have \({{\rho _{\mathfrak{M }_k}}{(\hat{q}_1)}}\hat{\approx }_b^\mathfrak{M }{{\rho _{\mathfrak{M }_l}}{({q})}}\) and \({{\rho _{\mathfrak{M }_k}}{(\hat{q}_2)}}\hat{\approx }_c^\mathfrak{M }{{\rho _{\mathfrak{M }_l}}{({q})}}\) which implies \(|{{\rho _{\mathfrak{M }_k}}{(\hat{q}_1)}}|\!=\!|{{\rho _{\mathfrak{M }_m}}{({q})}}|\!=\!|{{\rho _{\mathfrak{M }_k}}{(\hat{q}_2)}}|\) and hence \({{\rho _{\mathfrak{M }_k}}{(\hat{q}_1,q_1)}}\approx _a^\mathfrak{M }{{\rho _{\mathfrak{M }_k}}{(\hat{q}_2,q_2)}}\).\(\square \)

The next lemma analyses the structure of two indistinguishable nodes from subsequent tree levels.

Lemma 4

Let \(\mathfrak{M }\) be an i \(\mathbf{CGS _{\mathbf{}}}\), \(q\) a state in it, \(h_1\in \Delta ^{i}_\mathfrak{M }(q)\), \(h_2\in \Delta ^{i+1}_\mathfrak{M }(q)\), and \(h_1\sim _a^{T_s(\mathfrak{M },q)}h_2\) for some \(i\in \mathbb N _0\). Then, we have that \({ lastr }(h_1)\sim _a^\mathfrak{M }{ rel }(h_2)\).

Proof

By definition, we have that \( ref (h_2)\sim _a^{T_s(\mathfrak{M },q)}h_1\) and \({ lastr }( ref (h_2))\sim _a^\mathfrak{M }{ rel }(h_2)\). Because \( ref (h_2)\in \Delta ^i_\mathfrak{M }(q)\) we also have \({ rel }(h_1)\approx _a^\mathfrak{M }{ rel }( ref (h_2))\), and hence \({ lastr }(h_1)\sim _a^\mathfrak{M }{ lastr }( ref (h_2))\). The claim follows because \({ lastr }( ref (h_2))\sim _a^\mathfrak{M }{ rel }(h_2)\) and by the transitivity of \(\sim _a^\mathfrak{M }\). \(\square \)

The next lemma states that nodes which are indistinguishable for a group of agents must be located on subsequent or the same level of the pando unfolding; moreover, it characterizes the structure of these nodes.

Lemma 5

Let \(\mathfrak{M }\) be an i \(\mathbf{CGS _{\mathbf{}}}\), \(q\) a state in it, and \(A\subseteq {\mathbb{A }\mathrm{gt }} \) be a group of agents. Then, for all \(h\in { St } _{T_s(\mathfrak{M },q)}\) there is an \(i\in \mathbb N _0\) such that for all \(h^{\prime }\in { St } _{T_s(\mathfrak{M },q)}\) with \(h(\sim _A^{T_s(\mathfrak{M },q)})^* h^{\prime }\) we have that \(h,h^{\prime }\in \Delta _\mathfrak{M }^i(q)\cup \Delta _\mathfrak{M }^{i+1}(q)\); moreover, if \(h^{\prime }\in \Delta ^{i+1}_\mathfrak{M }(q)\) \(h(\sim _A^{T_s(\mathfrak{M },q)})^* h^{\prime }\) and there is an \(h^{\prime \prime }\in \Delta ^{i}_\mathfrak{M }(q)\) with \(h(\sim _A^{T_s(\mathfrak{M },q)})^* h^{\prime \prime }\) then \({ rel }(h^{\prime })\in { St } _\mathfrak{M }\) and \({ jump }(h^{\prime })\in A\).

Proof

We write \(T_s\) for \({T_s(\mathfrak{M },q)}\) and \(\Delta ^i\) for \(\Delta ^i_\mathfrak{M }(q)\) and so on. We proceed by induction on the length of the epistemic path \(h^{\prime }=h_1\sim _{a_1}\cdots \sim _{a_{l+1}}h_{{l+1}}\). We show the following: (i) if \(h_j\in \Delta ^i\) for all \(j=1,\ldots , l\) then \(h_{l+1}\in \Delta ^{i-1}\cup \Delta ^i\cup \Delta ^{i+1}\); if this is not the case then (ii) if \(h_j\in \Delta ^i\cup \Delta ^{i+1}\) for all \(j=1,\ldots , l\) then \(h_{l+1}\in \Delta ^i\cup \Delta ^{i+1}\) and for each \(h_j\in \Delta ^{i+1}\) we have that \({ rel }(h_j)\in { St } \), \({ jump }(h_j)\in A\), and \( ref (h_j)\in \Delta ^{i}\).

Base case The case for \(h\sim _a h^{\prime }\) is clear by definition.

Induction step Suppose we have \(h^{\prime }=h_1\sim _{a_1}\cdots \sim _{a_{l}}h_{{l}}\) satisfying the assumption and assume that \(h_l\sim _{a_{l+1}}h_{l+1}\). Firstly, assume that case (i) applies; that is, that all \(h_j\in \Delta ^i\) for \(j=1,\ldots , l\). By definition \(h_{l+1}\in \Delta ^{i-1}\cup \Delta ^i\cup \Delta ^{i+1}\). Moreover, if \(h_{l+1}\in \Delta ^{i+1}\) then it must have the required form \(h^{\prime \prime }\hat{a}q^{\prime }\) by Definition 17(c).

We consider case (ii). Firstly, suppose that \(h_l\in \Delta ^{i+1}\) and \(h_l=h^{\prime }\hat{a}_{l}q^{\prime }\). We consider \(h_l\sim _{a_{l+1}}h_{l+1}\). By definition \(h_{l+1}\in \Delta ^{i}\cup \Delta ^{i+1}\cup \Delta ^{i+2}\). If \(h_{l+1}\in \Delta ^{i+1}\) it also has the required form. For the sake of contradiction, suppose that \(h_{l+1}\in \Delta ^{i+2}\). Then, \(h_{l+1}=h^{\prime \prime }\hat{a}_{l+1}q^{\prime \prime }\) for some \(h^{\prime \prime }\in \Delta ^{i+1}\) with \(h^{\prime \prime }\sim _{a_{l+1}}h_l\). In this case, \(h^{\prime \prime }\) does also have the form \(h^{\prime \prime }=h^{\prime \prime \prime }\hat{a}_{l}q^{\prime \prime \prime }\) and therewith \(h_{l+1}=h^{\prime \prime \prime }\hat{a}_{l}q^{\prime \prime \prime }\hat{a}_{l+1}q^{\prime \prime }\) contradicting \(h_{l+1}\in \Delta ^{i+2}\) by definition of the sets \(\Delta ^j \).

Secondly, if \(h_l\in \Delta ^i\) we have that \(h_{l+1}\in \Delta ^{i-1}\Delta ^i\cup \Delta ^{i+1}\) and that \(h_{l+1}\) has the required form if \(h_{l+1}\in \Delta ^{i+1}\) following the very same reasoning as in case (i). Moreover, it cannot be the case that \(h_{l+1}\in \Delta ^{i-1}\). To see this, we observe that there is some \(h_u\) with \(1\le u<l+1\), \(h_u\in \Delta ^{i+1}\) and \(h_{l+1}(\sim _A^{T_s})^*h_u\). Now the reasoning of the previous case can be applied to obtain a contradiction. \(\square \)

The next lemma states that the relevant parts (i.e. histories) of two states of the pando unfolding are group indistinguishable in the model if the states are group indistinguishable in the pando unfolding and are located within the same tree (i.e. share the same root node).

Lemma 6

Let \(h_1(\sim _A^{T_s})^* h_2\). If there is an \(i\in \mathbb N _0\) with \(h_1,h_2\in \Delta ^i\) then \({ rel }(h_1){(\approx _A^\mathfrak{M })^*} { rel }(h_2)\).

Proof

The poof is done by induction on the number of epistemic steps between \(h_1\) and \(h_2\). More precisely, we show that for all \(h^{\prime }\) with \(h_1(\sim ^{T_s}_A)^*h^{\prime }\) we have that

1. (i)

   \({ rel }(h_1)(\approx _A^\mathfrak{M })^* { rel }(h^{\prime })\) if \(h^{\prime }\in \Delta ^i\);

2. (ii)

   \( ref (h^{\prime })(\sim ^{T_s}_A)^*h_1\) and \({ lastr }({h_1})(\sim _A^\mathfrak{M })^*{ lastr }( ref (h^{\prime }))\) if \(h^{\prime }\in \Delta ^{i+1}\);

3. (iii)

   and \({ rel }(h_1)(\sim _A^\mathfrak{M })^*{ lastr }(h^{\prime })\) if \(h^{\prime }\in \Delta ^{i-1}\) (and \(i>0\)).

The base cases are clear by definition. We assume that \(h_1(\sim ^{T_s}_A)^*h^{\prime }\), \(i>0\) and we show that \(h_2\) with \(h_1(\sim _A^{T_s})^*h^{\prime }\sim _a^{T_s}h_2\) for \(a\in A\) satisfies the property of the lemma.

• Case: \(h^{\prime }\in \Delta ^i\) and \(h_2\in \Delta ^i\). By definition \({ rel }(h^{\prime })\approx _a^\mathfrak{M }{ rel }(h_2)\) and by induction \({ rel }(h_1)(\approx _A^\mathfrak{M })^*{ rel }(h^{\prime })\); hence, \({ rel }(h_1)(\approx _A^\mathfrak{M })^*{ rel }(h_2)\).

• Case: \(h^{\prime }\in \Delta ^i\) and \(h_2\in \Delta ^{i+1}\). By induction, \({ rel }(h_1)(\approx ^\mathfrak{M }_A)^*{ rel }(h^{\prime })\) and in particular, \({ lastr }(h_1)\sim _A^*{ lastr }(h^{\prime })\). By Lemma 4 \({ lastr }(h^{\prime })\sim _a^\mathfrak{M }{ rel }(h_2)\). This shows that, \({ lastr }(h_1)(\sim _A^\mathfrak{M })^*{ rel }(h_2)\sim _a^\mathfrak{M }{ lastr }( ref (h_2))\).

• Case: \(h^{\prime }\in \Delta ^i\) and \(h_2\in \Delta ^{i-1}\). By definition \({h_2}\sim _A^{T_s} ref (h^{\prime })\) and \({ rel }(h^{\prime })\sim _A^\mathfrak{M }{ lastr }(h_2)\); hence, \({ rel }(h^{\prime })\in { St } _\mathfrak{M }\). Thus, by induction \({ rel }(h_1)(\sim _A^\mathfrak{M })^*{ rel }(h^{\prime })\) and by Lemma 4 \({ rel }(h^{\prime })\sim _a^\mathfrak{M }{ lastr }(h_2)\). This shows that \({ rel }(h_1)(\sim _A^\mathfrak{M })^*{ lastr }(h_2)\).

• Case: \(h^{\prime }\in \Delta ^{i-1}\) and \(h_2\in \Delta ^{i-1}\). Follows immediately.

• Case: \(h^{\prime }\in \Delta ^{i-1}\) and \(h_2\in \Delta ^{i}\). We have \({ rel }(h_1)(\sim _A^\mathfrak{M })^*{ lastr }(h^{\prime })\). By Lemma 4 \({ rel }(h_2)\sim _a^\mathfrak{M }{ lastr }(h^{\prime })\) and hence \({ rel }(h_1)(\sim _A^\mathfrak{M })^*{ rel }(h_2)\). The claim follows as \({ rel }(h_1),{ rel }(h_2)\in { St } _\mathfrak{M }\).

Cases where \(h^{\prime }\in \Delta ^j\) and \(h_2\in \Delta ^k\) with \(|j-k|>1\) are not possible due to Lemma 5. \(\square \)

Lemma 7

For all \(q\) in \(\mathfrak{M }\) and all \(i,j\in \mathbb N _0\) with \(i\ne j\) we have that \(\Delta ^i_\mathfrak{M }(q)\cap \Delta ^j_\mathfrak{M }(q)=\emptyset \).

Lemma 8

Let \(\mathfrak{M }\) be an i \(\mathbf{CGS _{\mathbf{}}}\), \(q\) a state in it, and \(a\in {\mathbb{A }\mathrm{gt }} \). Every relation \(\sim _a^{T_s(\mathfrak{M },q)}\) is an equivalence relation.

Proof

We write \(T_s\) for \({T_s(\mathfrak{M },q)}\). Reflexivity and symmetry of epistemic relations in \(T_s\) are clear from the definition of \({{{\textit{i}}_{\textit{s}}}{{\textit{R}}}} \)-pando unfoldings, but we need to prove transitivity. Suppose that \(h_1\sim _a^{T_s} h_2\) and \(h_2\sim _a^{T_s} h_3\). We have to show that \(h_1\sim _a^{T_s} h_3\). The proof is done by induction on the level \(\Delta ^i\). The base case for \(\Delta ^0\) is clear from the transitivity of the standard indistinguishability relation \(\approx _a^\mathfrak{M }\). By Lemma 5 (and the symmetry of \(\sim ^{T_s}\)) it is sufficient to consider the following cases (we assume that \(i>0\)):

• \(h_1,h_2,h_3\in \Delta ^i\): Follows by the transitivity of \(\approx _a^\mathfrak{M }\) (induction hypothesis).

• \(h_1,h_2\in \Delta ^i, h_3\in \Delta ^{i+1}\): From \(h_1\sim _a^{T_s} h_2\) it follows that \({ rel }(h_1)\approx _a^\mathfrak{M }{ rel }(h_2)\); and from \(h_2\sim _a^{T_s} h_3\) that \( ref (h_3)\sim _a^{T_s}h_2\) and \({ lastr }( ref (h_3))\sim _a^\mathfrak{M }{ rel }(h_3)\). Furthermore, because \( ref (h_3)\in \Delta ^i\) we can deduce from the transitivity of \(\sim _a ^{T_s}\) (and by induction) that \( ref (h_3)\sim _a^{T_s}h_1\) and hence \({h_3}\sim _a^{T_s}h_1\) by definition.

• \(h_1\in \Delta ^i, h_2, h_3\in \Delta ^{i+1}\): We have that \( ref (h_2)\sim _a^{T_s} h_1\) and \({ lastr }( ref (h_2))\sim _a^{T_s}{ rel }(h_2)\) and \({ jump }(h_2)=a\). Then, we also have that \({ rel }(h_2)\approx _a^{T_s}{ rel }(h_3)\) and \({ jump }(h_3)={ jump }(h_2)=a\) and \( ref (h_2)\sim _a^{T_s} ref (h_3)\) proving that also \(h_1\sim _a^{T_s}h_3\) by induction.

• \(h_1,h_3\in \Delta ^i, h_2\in \Delta ^{i+1}\): We have that \( ref (h_2)\sim _a^{T_s} h_1\) and \({ lastr }( ref (h_2))\sim _a^{T_s}{ rel }(h_2)\) and \({ jump }(h_2)=a\) and \( ref (h_2)\sim _a^{T_s} h_3\) and thus \(h_1\sim _a^{T_s}{h}_3\) (by induction).

• \(h_1,h_3\in \Delta ^{i+1}, h_2\in \Delta ^{i}\): We have that \( ref (h_1)\sim _a^{T_s} h_2\) and \({ lastr }( ref (h_1))\sim _a^{T_s}{ rel }(h_1)\) and \({ jump }(h_1)=a\) and \( ref (h_3)\sim _a^{T_s} h_2\) \({ lastr }( ref (h_3))\sim _a^{T_s}{ rel }(h_3)\) and \({ jump }(h_3)=a\). But then by induction \( ref (h_1)\sim _a^{T_s} ref (h_3)\) and \({ rel }(h_1)\sim _a^\mathfrak{M }{ rel }(h_3)\) which shows that \(h_1\sim _a^{T_s}h_3\). \(\square \)

Proposition 8 The \({{{\textit{i}}_{\textit{s}}}{{\textit{R}}}}\) -pando unfolding of a pointed i CGS is \({{{\textit{i}}_{\textit{s}}}{{\textit{R}}}}\) -pando-like.

Proof

Let \(\mathfrak{M }\) be an i \(\mathbf{CGS _{\mathbf{}}}\) and \(T_s\) its \({{{\textit{i}}_{\textit{s}}}{{\textit{R}}}} \)-pando unfolding. For each \(h\in { St }^{\prime }\) with \(|{ rel }(h)|=1\) we define \({ St } _h\) as the set of states/histories in \({ St }^{\prime }\) reachable from \(h\), i.e. \({ St } _h=\{h^{\prime }\in { St }^{\prime }\mid {{\rho _{T_s}}{(h,h^{\prime })}}\ne \epsilon \}\). Let \(\mathfrak{M }_h\) denote the submodel of \(T_s\) which does only consist of states \({ St } _h\) and in which the domain of all elements is restricted to \({ St } _h\). Moreover, we take \(I=\{h\in { St } \mid |{ rel }(h)|=1\}\).

Claim: We have that \({ St }^{\prime }=\biguplus _{h\in I}{ St } _h\) and each \(\mathfrak{M }_h\) is \({{{\textit{i}}_{\textit{o}}{\textit{R}}}} \)-tree-like.

Proof of claim: Clearly, all sets \({ St } _h\) are mutually disjoint and each \(h\in { St } \) has to occur in some \({ St } _h\). It is also obvious that each \(\mathfrak{M }_h\) has tree-structure. Now suppose \(h_1,h_2\in { St } _h\) with \(h_1\sim _a^{T_s} h_2\); then, by definition also \(h_1\approx _a^{\mathfrak{M }} h_2\).

We proceed with the main proof and define \(\hat{\sim }_a\) as the subset of \(\sim _a^{T_s}\) which exists between sets \({ St } _h\) and \({ St } _{h^{\prime }}\) with \(h\ne h^{\prime }\). From Lemma 8 it follows that \(\sim _a^{T_s}\) is transitive and that \(\hat{\sim }_a\) is symmetric. Moreover, by definition \(\hat{\sim }_a\cap ({ St } _h\times { St } _h)=\emptyset \) for all \(h\in { St }^{\prime }\).

The fourth condition of Definition 16 is obvious from the definition of the \({{{\textit{i}}_{\textit{s}}}{{\textit{R}}}} \)-pando unfolding. It remains to show the fifth condition of Definition 16. Suppose \(h_1,h_1^{\prime }\in { St } _{\bar{h}_1}\) and \(h_1(\sim _{\mathbb{A }\mathrm{gt }})^*h_1^{\prime }\). Then, also \(h_1,h_1^{\prime }\in \Delta _i\) for some \(i\). From Lemma 6 we obtain that \({ rel }(h_1)(\approx _{\mathbb{A }\mathrm{gt }} ^{\mathfrak{M }})^*{ rel }(h_1^{\prime })\), i.e. that both nodes reside on the same level. \(\square \)

The following two lemmata are needed to prove Theorem 3. The first lemma states that the set of epistemic alternatives to any state is the same in the model and in the pando unfolding.

Lemma 9

Let \(\mathfrak{M }\) be an i \(\mathbf{CGS _{\mathbf{}}}\) and \(q_0\) a state in it. Then, the following property holds: For all \(A\subseteq {\mathbb{A }\mathrm{gt }} \) and all nodes \(h\) in \(T_{s}(\mathfrak{M },q_0)\) we have that \(\{q\mid { lastr }(h)\sim _A^\mathfrak{M }q,\ q\in { St } _\mathfrak{M }\}=\{{ lastr }({h^{\prime }}) \mid h^{\prime }\sim _A^{T_{s}(\mathfrak{M },q_0)} h,\ h^{\prime }\in { St } _{T_{s}(\mathfrak{M },q_0)}\}\).

Proof

“\(\subseteq \)”: Suppose \(h=h^{\prime }q^{\prime }\in \Delta ^i_\mathfrak{M }(q_0)\) and \(q^{\prime }\sim _A^\mathfrak{M }q\) and \(h^{\prime }\ne \epsilon \) (the case for \(h^{\prime }=\epsilon \) is clear). Then, there is some \(a\in A\) with \(q^{\prime }\sim _a^\mathfrak{M }q\) and thus \(h^{\prime \prime }:=\hat{h}\hat{a}q\in \Delta ^{i+1}_\mathfrak{M }(q_0)\subseteq { St } _{T_{s}(\mathfrak{M },q_0)}\) with \(\hat{h}\sim ^{T_s}_a h\) by definition of the \(\Delta ^j_\mathfrak{M }\)’s. By Definition 17 also \(h^{\prime \prime }\sim _A^{T_{s}(\mathfrak{M },q_0)} h\). The claim follows as \({ lastr }(h^{\prime \prime })=q\).

“\(\supseteq \)”: Suppose \(h^{\prime }\sim _A^{T_{s}(\mathfrak{M },q_0)} h\) and \(h^{\prime }\in { St } _{T_{s}(\mathfrak{M },q_0)}\). The claim is clear if \(h,h^{\prime }\in \Delta ^i_\mathfrak{M }(q_0)\). According to Definition 17 the remaining case is when \(h\in \Delta ^i_\mathfrak{M }(q)\) and \(h^{\prime }\in \Delta _\mathfrak{M }^{i+1}(q)\), or the roles of \(h\) and \(h^{\prime }\) switched. Then, \(h^{\prime }=\hat{h}\hat{a}q\), \(\hat{h}\sim ^{T_s}_ah\) for some \(a\in {\mathbb{A }\mathrm{gt }} \) and \({ lastr }(\hat{h})\sim _a^\mathfrak{M }q\). The claim follows as \({ lastr }(h^{\prime })=q\) and \({ lastr }(h)\sim _A^\mathfrak{M }q\). \(\square \)

The next lemma is needed to show that the witnessing strategy which we shall construct in the invariance Theorem 3 is uniform.

Lemma 10

Let \(\mathfrak{M }\) be an \(\mathbf{i }\mathbf{CGS _{\mathbf{}}} \), \(q\) a state in it, \(T_s=T_s(\mathfrak{M },q)\), \(h,\hat{h}_1, \hat{h}_2\in { St } _{T_s}\), \(A\subseteq {\mathbb{A }\mathrm{gt }} \), and \(a\in {\mathbb{A }\mathrm{gt }} \). If \(\hat{h}_1\sim _A^{T_s} h\sim _A^{T_s}\hat{h}_2\) and \(h_1=\hat{h}_1h_1^F\sim _a\hat{h}_2h_2^F=h_2\) with \(h_1^F,h_2^F\in \varLambda _{}^{fin}\); then, (\({ rel }(h_1)\approx _a^\mathfrak{M }{ rel }(h_2)\), \({{\rho _{}}{(\hat{h}_1,h_1)}}\approx _a^\mathfrak{M }{{\rho _{}}{(\hat{h}_2,h_2)}}\) and \(|h_1^F|=|h_2^F|\)), or \(h_1^F=h_2^F=\epsilon \).

Proof

Suppose \(\hat{h}_1\sim _b^{T_s} h\sim _c^{T_s}\hat{h}_2\) with \(b,c\in A\). From Lemma 3 we obtain \({{\rho _{}}{(\hat{h}_1,h_1)}}\approx _a^\mathfrak{M }{{\rho _{}}{(\hat{h}_2,h_2)}}\) by taking \(\hat{q}_i=\hat{h}_i\) and \(q_i=h_i\) and \(q=h\) for \(i=1,2\).

To prove the lemma, we firstly assume that \(h_1,h_2\in \Delta ^i\) for some \(i\in \mathbb N _0\). Then, by definition \({ rel }(h_1)\approx _a^\mathfrak{M }{ rel }(h_2)\) and the claim follows.

Secondly, suppose w.l.o.g. \(h_1\in \Delta ^i\) and \(h_2\in \Delta ^{i+1}\) for some \(i\in \mathbb N _0\). In this case \({ rel }(h_2)\in { St } \) and thus \(h_2^F=\epsilon \) and \({{\rho _{}}{(\hat{h}_2,h_2)}}={ rel }(h_2)\approx _a^\mathfrak{M }{{\rho _{}}{(\hat{h}_1,h_1)}}\). The latter implies that \(|{{\rho _{}}{(\hat{h}_1,h_1)}}|=1\) and hence \(h_1^F=\epsilon \). \(\square \)

Theorem 3 For every i CGS \(\mathfrak{M }\), state \(q\) in \(\mathfrak{M }\), and \({{\varvec{ATL}}}^{*}\) -formula \(\varphi \), it holds that

Proof

We show that for every node \(h\) in \(T_s:=T_s (\mathfrak{M },q)\) it holds that \(\mathfrak{M },{ lastr }(h)\models _{{{\textit{i}}_{\textit{s}}}{{\textit{R}}}} \varphi \) iff \(T_s (\mathfrak{M },q),h\models _{{{{\textit{i}}_{\textit{s}}}{{\textit{r}}}}}\varphi \). Then, the claim follows from Propositions 7 and 8 for \(h=q\). The proof is done by induction on the structure of \(\varphi \) and is similar to the proof given for Theorem 2.

Base cases:

• Propositional case: Straightforward.

• Case: \(\varphi \equiv \langle \!\langle {A}\rangle \!\rangle _{_{\!{ }}}\gamma \) where \(\gamma \) contains no nested strategic modalities. “\(\Rightarrow \)”: Suppose we have \(\mathfrak{M },{ lastr }(h)\models _{_{{{ {{{\textit{i}}_{\textit{s}}}{{\textit{R}}}} }}}}\langle \!\langle {A}\rangle \!\rangle _{_{\!{ }}}\gamma \) and let \(s_A\) be an \(iR\)-strategy with

  $$\begin{aligned} (\star )\ \forall \lambda \in out^{{{{\textit{i}}_{\textit{s}}}}}_\mathfrak{M }({ lastr }(h),s_A): \mathfrak{M },\lambda \models _{_{{{ {{{\textit{i}}_{\textit{s}}}{{\textit{R}}}} }}}}\gamma . \end{aligned}$$

  We construct the \({\textit{ir}} \)-strategy \(s_A^{\prime }\) in \(T_s(\mathfrak{M },q)\) as follows: for all \(\hat{h}\in { St } _{T_s}\) with \(h\sim _A^{T_s}\hat{h}\) and all \(h^F\in \varLambda _{\mathfrak{M }}^{fin}({ lastr }(\hat{h}))\) we set

  $$\begin{aligned} s^{\prime }_a(\hat{h}(h^F[1,\infty ])):=s_a(h^F). \end{aligned}$$

  We note that we have to exclude the first state in \(h^F\) because it is already contained in \(\hat{h}\). For all other histories \(h^{\prime \prime }\) (which do not have the prescribed form) we define \(s^{\prime }_a(h^{\prime \prime })\) arbitrarily but in a uniform way. The setting is illustrated in Fig. 16. Clearly, we have that each \(\hat{h}(h^F[1,\infty ])\) is a valid state in \(T_s\) and by Lemma 10, \(s^{\prime }_a\) is well-defined: Suppose, there are \(h_1=\hat{h}_1h_1^F\) and \(h_2=\hat{h}_2h_2^F\) with \(h_1=h_2\). Then, also \(h_1\sim _a^{T_s}h_2\) and by Lemma 10 \(h_1^F=h_2^F\) which shows that \(s_a^{\prime }(h_1)=s_a^{\prime }(h_2)\). In the following we show that \(s_a^{\prime }\) is uniform. Let \(h_1\) and \(h_2\) be two histories with \(h_1\sim _a^{T_s}h_2\).

  1. 1.

     Assume that both nodes have the form from above, i.e. \(h_1=\hat{h}_1h_1^F\), \(h_1=\hat{h}_1h_1^F\) and \(h_1\sim _A^{T_s} h\sim _A^{T_s} h_2\). Then, uniformity follows from Lemma 10.

  2. 2.

     Choices for two histories \(h_1\) and \(h_2\) where at least one does not have the required form can be defined in a uniform way by definition because \(\sim _a^{T_s}\) is an equivalence relation.

  Finally, we show that the sets of outcome paths are isomorphic wrt. both strategies. By Lemma 9 we have that for all states \(q_0\) in \(\mathfrak{M }\) the following holds \(q_0\sim _A^{\mathfrak{M }} { lastr }(h)\) iff there is a history \(h^{\prime }\) with \(h^{\prime }\sim ^{T_s}_A h\) and \({ lastr }(h^{\prime })=q_0\). We denote one of these histories \(h^{\prime }\) by \(h(q_0)\). Then, by construction of \(s_A^{\prime }\) we have that

  $$\begin{aligned}&q_0q_1q_2\cdots \in out^{{{{\textit{i}}_{\textit{s}}}}}_\mathfrak{M }(last(h),s_A)\\&\quad \text {iff}\quad (h^{\prime })(h^{\prime }q_1)(h^{\prime }q_1q_2)\cdots \in out^{{{{\textit{i}}_{\textit{s}}}}}_{T_s(\mathfrak{M },q)}(h,s_A^{\prime })\\&\quad \text { for some }h^{\prime }=h(q_0). \end{aligned}$$

  Since the valuation of propositions does only depend on the final state of a history and by \((\star )\) we have \(T_s (\mathfrak{M },q),h\models _{{{{\textit{i}}_{\textit{s}}}{{\textit{r}}}}}\langle \!\langle {A}\rangle \!\rangle _{_{\!{ }}}\gamma \). \(\Leftarrow \): For the other direction, suppose we have \(T_s(\mathfrak{M },q),h\models _{_{{{ {{{\textit{i}}_{\textit{s}}}{{\textit{r}}}} }}}}\langle \!\langle {A}\rangle \!\rangle _{_{\!{ }}}\gamma \). So, there is an ir-strategy \(s_A\) such that

  $$\begin{aligned} (\star )\ \forall \lambda \in out^{{{{\textit{i}}_{\textit{s}}}}}_{T_s(\mathfrak{M },q)}(h,s_A): T_s(\mathfrak{M },q),\lambda \models _{{{{\textit{i}}_{\textit{s}}}{{\textit{r}}}}}\gamma . \end{aligned}$$

  We construct a witnessing \({\textit{iR}} \)-strategy \(s_A^{\prime }\) in \(\mathfrak{M }\) as follows: \(s_a^{\prime }(h^F)=s_a(\hat{h}\hat{a}h^F)\) for every \(a\in A\), \(\hat{h}\sim ^{T_s}_A h\) for \(h^F\in \Lambda ^{fin}(q^{\prime })\) with \(q^{\prime }\sim _A^\mathfrak{M }{ lastr }(h)\) and arbitrary but in a uniform way for all other histories. It is easy to verify that each strategy \(s_a^{\prime }\) is uniform and well-defined. Moreover, \(s_A^{\prime }\) yields an equivalent (apart from the notational differences) set of outcome paths as above. We have \(\mathfrak{M },{ lastr }(h)\models _{{{{\textit{i}}_{\textit{s}}}{{\textit{R}}}}}\langle \!\langle {A}\rangle \!\rangle _{_{\!{ }}}\gamma \).

Setting of the proof of Theorem 3

Full size image

Induction step:

• Case: \(\varphi \equiv \psi _1\wedge \psi _2\). Straightforward.

• Case: \(\varphi \equiv \lnot \psi \). \(\mathfrak{M },{ lastr }(h)\models _{_{{{ {{{\textit{i}}_{\textit{s}}}{{\textit{R}}}} }}}}\lnot \psi \) iff not \(\mathfrak{M },{ lastr }(h)\models _{_{{{ {{{\textit{i}}_{\textit{s}}}{{\textit{R}}}} }}}}\psi \) iff (by induction hypothesis) not \(T_s(\mathfrak{M },q),h\models _{_{{{ {{{\textit{i}}_{\textit{s}}}{{\textit{R}}}} }}}}\psi \) iff \(T_s(\mathfrak{M },q),h\models _{_{{{ {{{\textit{i}}_{\textit{s}}}{{\textit{R}}}} }}}}\lnot \psi \).

• Case: \(\varphi \equiv \langle \!\langle {A}\rangle \!\rangle _{_{\!{ }}}\gamma \). By induction hypothesis we have for each history \(h\) in \(T_s(\mathfrak{M },q)\) and each strict state-subformula \(\varphi ^{\prime }\) of \(\gamma \) that \(\mathfrak{M },{ lastr }(h)\models _{{{\textit{i}}_{\textit{s}}}{{\textit{R}}}} \varphi ^{\prime }\) iff \(T_s (\mathfrak{M },q),h\models _{{{{\textit{i}}_{\textit{s}}}{{\textit{r}}}}}\varphi ^{\prime }\). For any maximal strict state-subformula \(\varphi ^{\prime }\) we label all states \(h\) in \(T_s(\mathfrak{M },q)\) and states \({ lastr }(h)\) in \(\mathfrak{M }\) with a new proposition \(\mathsf{{p} }_{\varphi ^{\prime }}\) iff \(\varphi ^{\prime }\) holds in this very state. Then, we replace each \(\varphi ^{\prime }\) in \(\varphi \) with proposition \(\mathsf{{p} }_{\varphi ^{\prime }}\) and the claim follows by induction. \(\square \)

Reprints and permissions