# strategic_coalitions_with_perfect_recall__fbbf2123.pdf

Strategic Coalitions with Perfect Recall

Pavel Naumov Department of Computer Science Vassar College Poughkeepsie, New York 12604 pnaumov@vassar.edu

Jia Tao Department of Computer Science Lafayette College Easton, Pennsylvania 18042 taoj@lafayette.edu

The paper proposes a bimodal logic that describes an interplay between distributed knowledge modality and coalition know-how modality. Unlike other similar systems, the one proposed here assumes perfect recall by all agents. Perfect recall is captured in the system by a single axiom. The main technical results are the soundness and the completeness theorems for the proposed logical system.

Introduction Autonomous agents such as self-driving cars and robotic vacuum cleaners are facing the challenge of navigating without having complete information about the current situation. Such a setting could be formally captured by an epistemic transition system where an agent uses instructions to transition the system between states without being able to distinguish some of these states. In this paper we study properties of strategies in such systems. An example of such a system is the epistemic transition system T1, depicted in Figure 1. It has six states named w0, w 0, w1, w 1, w2, w 2 and two instructions 0 and 1 that an agent a can use to transition the system from one state to another. For instance, if an instruction 0 is given in state w0, then the system transitions into state w1. The system is called epistemic because the agent cannot distinguish state wi from state w i for each i = 0, 1, 2. The indistinguishability relation is shown in the ﬁgure using dashed lines. Atomic proposition p is true only in state w2.

w0 w1 w2 1 0

w0 w1 w2 0 0 ' '

Figure 1: Epistemic Transition System T1.

The logical system that we propose consists of two modalities. The ﬁrst is the knowledge modality K. Imagine that

Copyright c 2018, Association for the Advancement of Artiﬁcial Intelligence (www.aaai.org). All rights reserved.

the system starts in state w2. Since agent a cannot distinguish state w2 from state w 2 where statement p is not satisﬁed, the agent does not know if p is true or not. We write this as (w2) Kap. Next, suppose that the system started in state w1 and the agent used instruction 0 to transition the system into state w2. In this paper we assume that all agents have perfect recall, so in state w2 the agent remembers history (w1, 0, w2). However, such a history is indistinguishable from history (w 1, 0, w 2) because the agent cannot distinguish state w1 from state w 1 and state w2 from state w 2. Thus, the agent does not know that proposition p is true in the state w2 even with history (w1, 0, w2). We denote this by (w1, 0, w2) Kap. Finally, assume that the system started in state w0 and the agent ﬁrst used instruction 1 to transition it into state w1 and later instruction 0 to transition it to state w2. Thus, the history of the system is (w0, 1, w1, 0, w2). The only history that the agent cannot distinguish from this one is history (w 0, 1, w1, 0, w2). Since both of these histories end in a state where proposition p is satisﬁed, agent a does know that proposition p is true in state w2, given history (w0, 1, w1, 0, w2). We write this as (w0, 1, w1, 0, w2) Kap. The other modality that we consider is the strategic power. In system T1, the agent can transition the system from state w1 to state w2 by using instruction 0. Similarly, the agent can transition the system from state w 1 to state w2 by using instruction 1. In other words, given either history (w1) or history (w 1) the agent can transition the system to a state in which atomic proposition p is satisﬁed. We say that, given either history, agent a has a strategy to achieve p. Histories (w1) and (w 1) are the only histories indistinguishable by agent a from history (w1). Since she has a strategy to achieve p under all histories indistinguishable from history (w1), we say that given history (w1) the agent knows that she has a strategy. Similarly, given history (w 1), she also knows that she has a strategy. However, since indistinguishable histories (w1) and (w 1) require different strategies to achieve p, given history (w1) she does not know what the strategy is. We say that she does not have a know-how strategy. We denote this by (w1) Hap, where H stands for know-How. Of course, it is also true that (w 1) Hap. The situation changes if the transition system starts in state w0 instead of state w1 and transitions to state w1 under instruction 1. Now the history is (w0, 1, w1) and the histo-

The Thirty-Second AAAI Conference on Artificial Intelligence (AAAI-18)

ries that the agent cannot distinguish from this one are history (w 0, 1, w1) and history (w0, 1, w1) itself. Given both of these two histories, agent a can achieve p using the same transition 0. Thus, (w0, 1, w1) Hap. Finally note that there are only two histories: (w0) and (w 0) indistinguishable from (w0). Given either history, agent a can achieve Hap using instruction 1. Thus, (w0) Ha Hap. That is, given history (w0) agent a knows how to transition to a state in which formula Hap is satisﬁed.

Multiagent Systems Like many other autonomous agents, self-driving cars are expected to use vehicle-to-vehicle communication to share trafﬁc information and to coordinate actions (Harding et al. 2014). Thus, it is natural to consider epistemic transition systems that have more than one agent. An example of such a system T2 is depicted in Figure 2. This

Figure 2: Epistemic Transition System T2.

system has ﬁve epistemic states: w0, w1, w2, w3, and w4 and three agents: a, b, and c. In each state the agents vote either 0 or 1 and the system transitions into the next state based on the majority vote. For example, since the directed edge from state w0 to state w4 is labelled with 1, if the majority of agents in state w0 votes 1, then the system transitions into state w4. Since coalition {a, b} forms a majority, this coalition has a strategy to transition the system from state w0 to state w4 and, thus, to achieve p. Note that agent a cannot distinguish state w0 from state w1 and thus agent a does not know what she should vote for to achieve p. Similarly, agent b also does not know what she should vote for to achieve p because she cannot distinguish state w0 from state w2. In this paper, we assume that members of a coalition make the decisions based on combined (distributed) knowledge of the whole coalition. In our example, coalition {a, b} can distinguish state w0 from both state w1 and state w2. Thus, given history (w0) the coalition {a, b} knows how to achieve p. We denote this by (w0) H{a,b}p, or simply as (w0) Ha,bp.

Universal Principles We have discussed a statement being true or false given a certain history. This paper focuses on the logical principles that are true for each history in each epistemic transition system. An example of such a principle is the strategic positive introspection: HCϕ KCHCϕ. This principle says that if a coalition knows how to achieve ϕ, then the coalition knows that it knows how to achieve ϕ.

Informally, this principle is true because in order for statement HCϕ to be satisﬁed for a given history h, coalition C must have a strategy to achieve ϕ that works under any history h indistinguishable from history h by the coalition. Thus, the same strategy must work for any history h indistinguishable from history h by the coalition. In other words, it is also true that h HCϕ. Recall that h is an arbitrary history indistinguishable from history h by coalition C. Hence, h KCHCϕ according to the standard semantics of the epistemic modality KC. A similar argument can be used to justify the strategic negative introspection: HCϕ KC HCϕ. Another universal principle is the empty coalition principle: K ϕ H ϕ. Indeed, K ϕ means that statement ϕ is true under any history indistinguishable from the given history by an empty coalition. Since an empty coalition cannot distinguish any two histories, the assumption K ϕ means that statement ϕ is true under any history. In particular, this statement is true after the next transition no matter how agents vote. Hence, H ϕ. The epistemic modality KC also satisﬁes axioms of epistemic logic S5 for distributed knowledge. Know-how modality satisﬁes the unachievability of falsehood principle: HC , stating that no coalition can achieve . Knowhow modality also satisﬁes a form of cooperation principle (Pauly 2001; 2002):

HC(ϕ ψ) (HDϕ HC Dψ), where C D = .

Perfect Recall A complete trimodal logical system describing the interplay between distributed knowledge modality KC, coalition know-how modality HC, and standard (not know-how) strategic power modality in the imperfect recall setting was proposed by (Naumov and Tao 2017c). We provide a complete axiomatization of the interplay between modalities KC and HC in the perfect recall setting. Surprisingly, the assumption of perfect recall by all agents is captured by a single principle that we call the perfect recall principle: HDϕ HDKCϕ, where D C = . This principle says that if a sub-coalition D C can achieve ϕ, then after the vote the whole coalition will know that ϕ is true. Informally, this principle is true because coalition C is able to recall how sub-coalition D voted and, thus, will deduce that formula ϕ is true after the transition. As an empty coalition has no memory even in the perfect recall setting, it is essential for coalition C to be nonempty. However, the sub-coalition D can be empty.

Literature Review Non-epistemic logics of coalition power were developed by (Pauly 2001; 2002), who also proved the completeness of the basic logic of coalition power. His approach has been widely studied in the literature (Goranko 2001; van der Hoek and Wooldridge 2005; Borgo 2007; Sauro et al. 2006; Agotnes et al. 2010; Agotnes, van der Hoek, and Wooldridge 2009; Belardinelli 2014; Goranko, Jamroga, and Turrini 2013). An alternative logical system for coalition power was proposed by (More and Naumov 2012). (Alur, Henzinger, and Kupferman 2002) introduced Alternating-Time Temporal Logic (ATL) that combines

temporal and coalition modalities. (van der Hoek and Wooldridge 2003) proposed to combine ATL with epistemic modality to form Alternating-Time Temporal Epistemic Logic. They did not prove the completeness theorem for the proposed logical system. Aminof, Murano, Rubin and Zuleger (Aminof et al. 2016) studied modelchecking problems of an extension of ATL with epistemic and prompt eventually modal operators. ( Agotnes and Alechina 2012) proposed a complete logical system that combines the coalition power and epistemic modalities. Since their system does not have epistemic requirements on strategies, it does not contain any axioms describing the interplay of these modalities. In the extended version, ( Agotnes and Alechina 2016) added a complete axiomatization of an interplay between single-agent knowledge and know-how modalities. Know-how strategies were studied before under different names. While (Jamroga and Agotnes 2007) talked about knowledge to identify and execute a strategy , (Jamroga and van der Hoek 2004) discussed difference between an agent knowing that he has a suitable strategy and knowing the strategy itself . (van Benthem 2001) called such strategies uniform . (Broersen 2008) investigated a related notion of knowingly doing , while (Broersen, Herzig, and Troquard 2009) studied modality know they can do . (Wang 2015; 2016) captured the knowing how as a binary modality in a complete logical system with a single agent and without the knowledge modality. Coalition know-how strategies for enforcing a condition indeﬁnitely were investigated by (Naumov and Tao 2017a). Such strategies are similar to (Pauly 2001, p. 80) goal maintenance strategies in extended coalition logic . A similar complete logical system in a single-agent setting for knowhow strategies to achieve a goal in multiple steps rather than to maintain a goal is developed by (Fervari et al. 2017). (Naumov and Tao 2017c) also proposed a complete trimodal logical system describing an interplay between distributed knowledge modality KC, coalition know-how modality HC, and standard (not know-how) strategic power modality in the imperfect recall setting. In this paper we provide a complete axiomatization of an interplay between modalities KC and HC in the perfect recall setting. The main challenge in proving the completeness, compared to ( Agotnes and Alechina 2016; Fervari et al. 2017; Naumov and Tao 2017c; 2017a), is the need to construct not only possible worlds , but the entire possible histories , see the proof of Lemma 15.

Outline First, we introduce the syntax and semantics of our logical system. Next, we list the axioms and give examples of proofs in the system. Then, we prove the completeness of this system. The proof of the soundness is available in the full version of this paper (Naumov and Tao 2017b).

Syntax and Semantics Throughout the rest of the paper we assume a ﬁxed set of agents A. By XY we denote the set of all functions from set Y to set X, or in other words, the set of all tuples of elements from set X indexed by the elements of set Y . If t XY is

such a tuple and y Y , then by (t)y we denote the y-th component of tuple t. We now proceed to describe the formal syntax and semantics of our logical system starting with the deﬁnition of a transition system. Although our introductory examples used voting to decide on the next state of the system, in this paper we investigate universal properties of an arbitrary nondeterministic action aggregation mechanism.

Deﬁnition 1 A tuple (W, { a}a A, V, M, π) is called an epistemic transition system, if

1. W is a set of epistemic states, 2. a is an indistinguishability equivalence relation on W for each a A, 3. V is a nonempty set called domain of choices, 4. M W V A W is an aggregation mechanism, 5. π is a function that maps propositional variables into subsets of W.

For example, in the transition system T1 depicted in Figure 1, the set of states W is {w0, w1, w2, w 0, w 1, w 2} and relation a is a transitive reﬂexive closure of {(w0, w 0), (w1, w 1), (w2, w 2)}. Informally, an epistemic transition system is regular if there is at least one next state for each outcome of the vote.

Deﬁnition 2 An epistemic transition system (W, { a}a A, V, M, π) is regular if for each w W and each s V A, there is w W such that (w, s, w ) M.

A coalition is a subset of A. A strategy proﬁle of coalition C is any tuple in the set V C.

Deﬁnition 3 For any states w1, w2 W and any coalition C, let w1 C w2 if w1 a w2 for each agent a C.

Lemma 1 For each coalition C, relation C is an equivalence relation on the set of epistemic states W.

Deﬁnition 4 For all strategy proﬁles s1 and s2 of coalitions C1 and C2 respectively and any coalition C C1 C2, let s1 =C s2 if (s1)a = (s2)a for each a C.

Lemma 2 For any coalition C, relation =C is an equivalence relation on the set of all strategy proﬁles of coalitions containing coalition C.

Deﬁnition 5 A history is an arbitrary sequence h = (w0, s1, w1, s2, w2, . . . , sn, wn) such that n 0 and

1. wi W for each i n, 2. si V A for each i n, 3. (wi, si+1, wi+1) M for each i < n.

In this paper we assume that votes of all agents are private. Thus, an individual agent only knows her own votes and the equivalence classes of the states that the system has been at. This is formally captured in the following deﬁnition of indistinguishability of histories by an agent.

Deﬁnition 6 For any history h = (w0, s1, w1, . . . , sn, wn), any history h = (w 0, s 1, w 1, . . . , s m, w m), and any agent a A, let h a h if n = m and

1. wi a w i for each i n,

2. (si)a = (s i)a for each i n.

Deﬁnition 7 For any histories h1, h2 and any coalition C, let h1 C h2 if h1 a h2 for each agent a C.

Lemma 3 For any coalition C, relation C is an equivalence relation on the set of histories.

The length |h| of a history h = (w0, s1, w1, . . . , sn, wn) is the value of n. By Deﬁnition 7, the empty coalition cannot distinguish any two histories, even of different lengths. Lemma 4 |h1| = |h2| for each histories h1 and h2 such that h1 C h2 for some nonempty coalition C. For any sequence x = x1, . . . , xn and an element y, by sequence x :: y we mean x1, . . . , xn, y. If sequence x is nonempty, then by hd(x) we mean element xn. Lemma 5 If (h1 :: s1 :: w1) C (h2 :: s2 :: w2), then h1 C h2, s1 =C s2, and w1 C w2.

Deﬁnition 8 Let Φ be the language speciﬁed as follows ϕ := p | ϕ | ϕ ϕ | KCϕ | HCϕ, where C A.

Boolean constants and are deﬁned as usual.

Deﬁnition 9 For any history h of an epistemic transition system (W, { a}a A, V, M, π) and any formula ϕ Φ, let satisﬁability relation h ϕ be deﬁned as follows 1. h p if hd(h) π(p) and p is a propositional variable, 2. h ϕ if h ϕ, 3. h ϕ ψ if h ϕ or h ψ, 4. h KCϕ if h ϕ for each history h s.t. h C h , 5. h HCϕ if there is a strategy proﬁle s V C such that for any history h :: s :: w , if h C h and s =C s , then h :: s :: w ϕ.

Axioms In additional to propositional tautologies in language Φ, our logical system consists of the following axioms: 1. Truth: KCϕ ϕ, 2. Negative Introspection: KCϕ KC KCϕ, 3. Distributivity: KC(ϕ ψ) (KCϕ KCψ), 4. Monotonicity: KCϕ KDϕ, if C D, 5. Strategic Positive Introspection: HCϕ KCHCϕ, 6. Cooperation: HC(ϕ ψ) (HDϕ HC Dψ), where C D = , 7. Empty Coalition: K ϕ H ϕ, 8. Perfect Recall: HDϕ HDKCϕ, where D C = , 9. Unachievability of Falsehood: HC . We write ϕ if formula ϕ is provable from the axioms of our logical system using Necessitation, Strategic Necessitation, and Modus Ponens inference rules:

ϕ KCϕ ϕ HCϕ ϕ, ϕ ψ ψ .

We write X ϕ if formula ϕ is provable from the theorems of our logical system and a set of additional axioms X using only Modus Ponens inference rule.

The next lemma follows from a well-known observation that the Positive Introspection axiom is provable from the other axioms of S5. The proof can be found in the full version of this paper (Naumov and Tao 2017b).

Lemma 6 KCϕ KCKCϕ.

The proof of the following soundness theorem is also given in (Naumov and Tao 2017b).

Theorem 1 If ϕ, then h ϕ for each history of each regular epistemic transition system.

Derivation Examples This section contains examples of formal proofs in our logical system. The results obtained here are used in the proof of completeness. The proof of Lemma 7 is based on the one proposed to us by Natasha Alechina.

Lemma 7 (Alechina) HCϕ KC HCϕ.

Proof. By the Positive Strategic Introspection axiom, HCϕ KCHCϕ. Thus, KCHCϕ HCϕ by the contrapositive. Hence, KC( KCHCϕ HCϕ) by the Necessitation inference rule. Then, by the Distributivity axiom and the Modus Ponens inference rule KC KCHCϕ KC HCϕ. Thus, by the Negative Introspection axiom and the laws of propositional reasoning, KCHCϕ KC HCϕ. Note that HCϕ KCHCϕ is the contrapositive of the Truth axiom. Therefore, by the laws of propositional reasoning, HCϕ KC HCϕ.

Lemma 8 HCϕ HDϕ, where C D.

Proof. Note that ϕ ϕ is a propositional tautology. Thus, ϕ ϕ. Hence, HD\C(ϕ ϕ) by the Strategic Necessitation inference rule. At the same time, by the Cooperation axiom, HD\C(ϕ ϕ) (HCϕ HDϕ) due to the assumption C D. Therefore, HCϕ HDϕ by the Modus Ponens inference rule.

Lemma 9 If ϕ1, . . . , ϕn ψ, then

1. KCϕ1, . . . , KCϕn KCψ, 2. HC1ϕ1, . . . , HCnϕn H n i=1 Ciψ, where sets C1, . . . , Cn are pairwise disjoint.

Proof. To prove the second statement, apply deduction lemma for propositional logic n time. Then, we have ϕ1 ( (ϕn ψ)). Thus, by the Strategic Necessitation inference rule, H (ϕ1 ( (ϕn ψ))) Hence, HC1ϕ1 HC1(ϕ2 (ϕn ψ)) by the Cooperation axiom and the Modus Ponens inference rule. Then, HC1ϕ1 HC1(ϕ2 (ϕn ψ)) by the Modus Ponens inference rule. Thus, again by the Cooperation axiom and the Modus Ponens inference rule we have HC1ϕ1 HC2ϕ2 HC1 C2(ϕ3 (ϕn ψ)). Therefore, by repeating the last two steps n 2 times, HC1ϕ1, . . . , HCnϕn H n i=1 Ciψ. The proof of the ﬁrst statement is similar, but it uses the Distributivity axiom instead of the Cooperation axiom.

Completeness In the rest of this paper we focus on the completeness theorem for our logical system with respect to the class of regular epistemic transition systems. We start the proof of completeness by ﬁxing a maximal consistent set of formulae X0 and deﬁning a canonical epistemic transition system ETS(X0) = (W, { a}a A, Φ, M, π) using the unravelling technique (Sahlqvist 1975). Note that the domain of choices in the canonical model is the set of all formulae Φ.

Canonical Epistemic Transition System Deﬁnition 10 The set of epistemic states W consists of all sequences X0, C1, X1, . . . , Cn, Xn, such that n 0 and 1. Xi is a maximal consistent subset of Φ for each i 1, 2. Ci A for each i 1, 3. {ϕ | KCiϕ Xi 1} Xi, for each i 1.

Deﬁnition 11 Suppose that w = X0, C1, X1, . . . , Cn, Xn and w = X0, C 1, X 1 . . . , C m, X m are epistemic states. For any agent a A, let w a w if there is a non-negative integer k min{n, m} such that 1. Xi = X i for each i such that 0 < i k, 2. Ci = C i for each i such that 0 < i k, 3. a Ci for each i such that k < i n, 4. a C i for each i such that k < i m.

The next lemma states the basic property of the indistinguishability relation a. The proof of this lemma is standard. See (Naumov and Tao 2017b) for details. Lemma 10 For any epistemic states w, w W such that w C w , if KCϕ hd(w), then ϕ hd(w ). Next, we specify the aggregation mechanism of the canonical epistemic transition system. Informally, if a coalition has a know-how strategy to achieve ϕ and all members of the coalition vote for ϕ, then ϕ must be true after the transition. Deﬁnition 12 For any states w, w W and any complete strategy proﬁle s ΦA, let (w, s, w ) M if

{ϕ | (HDϕ hd(w)) a D((s)a = ϕ)} hd(w ).

Deﬁnition 13 π(p) = {w W | p hd(w)}.

This concludes the deﬁnition of the canonical epistemic transition system ETS(X0) = (W, { a}a A, Φ, M, π). We prove that this system is regular in Lemma 18.

K-child Lemmas The following technical results (Lemmas 11 15) about the knowledge modality K are used in the proof of completeness. Lemma 11 For any epistemic state w W if KCϕ hd(w), then there is an epistemic state w W such that w C w and ϕ hd(w ). Proof. Consider the set X = { ϕ} {ψ | KCψ hd(w)}. First, we show that set X is consistent. Assume the opposite. Then, there exist formulae KCψ1, . . . , KCψn hd(w) such that ψ1, . . . , ψn ϕ. Thus, KCψ1, . . . , KCψn KCϕ by Lemma 9. Therefore, hd(w) KCϕ by the choice of formulae KCψ1, . . . , KCψn, which contradicts the consistency of the set hd(w) due to the assumption KCϕ hd(w).

Let ˆX be a maximal consistent extension of set X and let w be sequence w :: C :: X. Note that w W by Deﬁnition 10 and the choice of set X. Furthermore, w C w by Deﬁnition 11. To ﬁnish the proof, note that ϕ X ˆX = hd(w ) by the choice of set X.

History h is a sequence whose last element hd(h) is an epistemic state. Epistemic state hd(h), by Deﬁnition 10, is also a sequence. Expression hd(hd(h)) denotes the last element of the sequence hd(h). Lemma 12 For any history h, if KCϕ hd(hd(h)), then ϕ hd(hd(h )) for each history h such that h C h . Proof. Assumption h C h by Deﬁnition 6 implies that hd(h) C hd(h ). Therefore, ϕ hd(hd(h )) by Lemma 10 and the assumption KCϕ hd(hd(h)).

Figure 3: Illustration for Lemma 13.

Lemma 13 For any nonempty coalition C, any states w1, w2, w3 W, and any complete strategy proﬁle s such that (w1, s, w2) M and w2 C w3, see Figure 3, there is a state w4 and a complete strategy proﬁle s such that w1 C w4, (w4, s , w3) M, and s =C s . Proof. Let s be a complete strategy proﬁle such that

(s )a = (s)a, if a C, , otherwise. (1)

Consider the set of formulae

X = {ϕ | KCϕ hd(w1)} { HDψ | ψ hd(w3) a D((s )a = ψ)}.

First, we show that set X is consistent. Indeed, set

{ HDψ | ψ hd(w3) a D((s )a = ψ)}

is equal to the union of the following two sets

{ HDψ | ψ hd(w3) D C a D((s )a = ψ)}, { HDψ | ψ hd(w3) D C a D((s )a = ψ)}.

The second set is a subset of { HD | D A} by the choice of strategy s , see (1). Thus, set X is a subset of

{ϕ | KCϕ hd(w1)} { HD | D A} { HDψ | ψ hd(w3) D C a D((s )a = ψ)}.

Hence, by the Unachievability of Falsehood axiom, to show the consistency of set X it sufﬁces to prove the consistency of the union of the set {ϕ | KCϕ hd(w1)} and the set

{ HDψ | ψ hd(w3) D C a D((s )a = ψ)}.

Suppose the opposite. In other words, assume that there are

formulae KCϕ1, . . . , KCϕn hd(w1), (2) formulae ψ1, . . . , ψm hd(w3), (3) and sets D1, . . . , Dm C, (4) such that i m a Di ((s )a = ψi), (5) and ϕ1, . . . , ϕn, HD1ψ1, . . . , HDmψm .

By Lemma 9 and the Truth axiom,

KCϕ1, . . . , KCϕn, KC HD1ψ1, . . . , KC HDmψm .

Hence, statement (2) and the consistency of the set hd(w1) imply that there exists k m such that KC HDkψk / hd(w1). Thus, KC HDkψk hd(w1) due to the maximality of the set hd(w1). Then, KDk HDkψk hd(w1) by statement (4) and the contrapositive of the Monotonicity axiom. Then, hd(w1) HDkψk by the contrapositive of Lemma 7. Thus, hd(w1) HDk KCψk by the Perfect Recall axiom, statement (4), and the assumption of the lemma that C = . Hence, HDk KCψk hd(w1) due to the maximality of the set hd(w1). Note that statements (1) and (4) imply s =Dk s . Then, (s)a = ψk for each agent a Dk by statement (5). Thus, KCψk hd(w2) by assumption (w1, s, w2) M, statement (4), and Deﬁnition 12. Hence, ψk hd(w3) by the assumption w2 C w3 of the lemma and Lemma 10. This contradicts statement (3) and the consistency of the set hd(w3). Therefore, set X is consistent. Let ˆX be any maximal consistent extension of set X. Deﬁne w4 to be the sequence w1 :: C :: ˆX. Note that w4 W by Deﬁnition 10 and the choice of set X. At the same time, w1 C w4 by Deﬁnition 11 and Deﬁnition 3. Finally, let us show that (w4, s , w3) M using Deﬁnition 12. Consider any D A and any HDψ hd(w4) = ˆX such that s (a) = ψ for each a D. We need to show that ψ hd(w3). Suppose the opposite. Then, ψ hd(w3) by the maximality of set hd(w3). Thus, HDψ X by the choice of set X. Hence, HDψ X ˆX. Therefore, HDψ / ˆX due to the consistency of set ˆX, which contradicts the choice of formula HDψ.

Lemma 14 For any history h, if K ϕ / hd(hd(h)), then there is a history h s.t. h h and ϕ hd(hd(h )).

Proof. By Lemma 11, there is a state w W such that hd(h) C w and ϕ hd(w). Let h be a one-element sequence w. Note that h h by Deﬁnition 7. Finally, ϕ hd(w) = hd(hd(h )).

Lemma 15 For any nonempty coalition C and any history h, if KCϕ / hd(hd(h)), then there is a history h such that h C h and ϕ hd(hd(h )).

Proof. Let h = (w0, s1, w1, . . . , sn, wn). We prove the lemma by induction on integer n. Base Case. Let n = 0. By Lemma 11, there is w 0 W such that w0 C w 0 and ϕ hd(w 0). Let h be a one-element sequence w 0. Note that w0 C w 0 implies that h C h by Deﬁnition 6. Also, ϕ hd(w 0) = hd(hd(h )).

w0 w1 wn-1 wn s1 sn

w0 w1 wn-1 wn s1 sn

h h_ ' ' ' ' ' ' ' '

Figure 4: Histories h and h .

Induction Step. Let h = (w1, s2, . . . , sn, wn), see Figure 4. By Deﬁnition 5, sequence h is a history. By the induction hypothesis there is a history h such that h C h and ϕ hd(hd(h )). Let h = (w 1, s 2, . . . , s n, w n). By Lemma 13, there is a state w 0 and a complete strategy proﬁle s 1 such that w0 C w 0, (w 0, s 1, w 1) M, and s1 =C s 1. Deﬁne h = (w 0, s 1, w 1, s 2, . . . , s n, w n). By Deﬁnition 5, statement (w 0, s 1, w 1) M implies that h is a history. Note that h C h by Deﬁnition 6 because h C h , w0 C w 0, and s1 =C s 1. Finally, ϕ hd(hd(h )) because hd(h ) = hd(h ) and ϕ hd(hd(h )).

H-child Lemmas Lemmas 16 and 17 are about the knowhow modality H. They are used later in the proof.

Lemma 16 For any history h, if HCϕ hd(hd(h)), then there is a strategy proﬁle s of coalition C s.t. for any history h :: s :: w if h C h and s =C s , then ϕ hd(w ).

Proof. Consider a strategy proﬁle s of coalition C such that (s)a = ϕ for each agent a C. Suppose that HCϕ hd(hd(h)) and sequence h :: s :: w is a history such that h C h and s =C s . It sufﬁces to show that ϕ hd(w ). By the Strategic Positive Introspection axiom, assumption HCϕ hd(hd(h)) implies hd(hd(h)) KCHCϕ. Thus, KCHCϕ hd(hd(h)) by the maximality of set hd(hd(h)). Assumption h C h implies hd(h) C hd(h ) by Definition 6. Thus, HCϕ hd(hd(h )) by Lemma 10 and because KCHCϕ hd(hd(h)). By Deﬁnition 5, assumption that sequence h :: s :: w is a history implies that (hd(h ), s , w ) M. Thus, ϕ hd(w ) by Deﬁnition 12 because HCϕ hd(hd(h )) and (s )a = (s)a = ϕ for each agent a C.

Lemma 17 For any history h and any strategy proﬁle s of a coalition C, if HCϕ hd(hd(h)), then there is a history h :: s :: w such that s =C s and ϕ hd(w ).

Proof. Let w = hd(h). Consider a complete strategy proﬁle s and a set of formulae X such that

(s )a = (s)a, if a C, , otherwise, (6)

and X = { ϕ} {χ | K χ hd(w)} {ψ | HDψ hd(w) a D((s )a = ψ)}. First, we show that set X is consistent. Indeed, note that set {ψ | HDψ hd(w) a D((s )a = ψ)} is equal to the union of the following two sets {ψ | HDψ hd(w) D C a D((s )a = ψ)}, {ψ | HDψ hd(w) D C a D((s )a = ψ)}. The second of the two sets is a subset of { } by the choice (6) of strategy proﬁle s . Thus, set X is a subset of { } { ϕ} {χ | K χ hd(w)} {ψ | HDψ hd(w) D C a D((s )a = ψ)}. Hence, to show the consistency of set X, it sufﬁces to prove the consistency of the union of { ϕ} {χ | K χ hd(w)} and {ψ | HDψ hd(w) D C a D((s )a = ψ)}. Suppose the opposite. In other words, assume there are formulae K χ1, . . . , K χn hd(w) (7) and formulae HD1ψ1, . . . , HDmψm hd(w) (8) such that D1, . . . , Dm C, (9) i m a Di ((s )a = ψi), (10) and χ1, . . . , χn, ψ1, . . . , ψm ϕ. By Lemma 9, H χ1, . . . , H χn, HD1ψ1, . . . , HDmψm H m i=1Diϕ. Then, by the Empty Coalition axiom, K χ1, . . . , K χn, HD1ψ1, . . . , HDmψm H m i=1Diϕ. Thus, by Lemma 8 and assumption (9), K χ1, . . . , K χn, HD1ψ1, . . . , HDmψm HCϕ. Hence, hd(w) HCϕ by assumption (7) and assumption (8). Then, HCϕ / hd(w) due to the consistency of the set hd(w), which contradicts the assumption HCϕ hd(w) of the lemma. Therefore, set X is consistent. Let set ˆX be a maximal consistent extension of set X and w be the sequence w :: :: ˆX. Note that w W by Deﬁnition 10 and because {χ | K χ hd(w)} X ˆX = hd(w ) by the choice of set X. Also note that (w, s , w ) M by Deﬁnition 12 and because {ψ | HDψ hd(w) a D((s )a = ψ)} X ˆX = hd(w ) by the choice of set X. Thus, h :: s :: w is a history by Deﬁnition 5. Finally, ϕ hd(w ) because ϕ X ˆX = hd(w ) by the choice of set X.

Lemma 18 The system ETS(X0) is regular. Proof. Let w W and s V A. By Deﬁnition 2, it sufﬁces to show that there is an epistemic state w such that (w, s, w ) M. Indeed, let history h be a single-element sequence w. Note that HA hd(w) = hd(hd(h)) by the Unachievability of Falsehood axiom and due to the maximality of set hd(w). Thus, by Lemma 17, there is a history h :: s :: w such that s =A s . Hence, (hd(h), s , w ) M by Deﬁnition 5. At the same time, s =A s implies that s = s by Deﬁnition 4. Thus, (hd(h), s, w ) M. Therefore, (w, s, w ) M because hd(h) = w.

Completeness: Final Steps

Lemma 19 h ϕ iff ϕ hd(hd(h)) for each history h and each formula ϕ Φ.

Proof. We prove the statement by induction on the structural complexity of formula ϕ. If ϕ is an atomic proposition p, then h p iff hd(h) π(p), by Deﬁnition 9. Hence, h p iff p hd(hd(h)) by Deﬁnition 13. The cases when formula ϕ is a negation or an implication follow from Deﬁnition 9 and the maximality and the consistency of the set hd(hd(h)) in the standard way. Next, suppose that formula ϕ has the form KCψ. ( ) : Let KCψ / hd(hd(h)). Then, either by Lemma 14 (when set C is empty) or by Lemma 15 (when set C is nonempty), there is a history h such that h C h and ψ hd(hd(h )). Hence, h ψ by the induction hypothesis. Therefore, h KCψ by Deﬁnition 9. ( ) : Let h KCψ. By Deﬁnition 9, there is a history h such that h C h and h ψ. Thus, ψ / hd(hd(h )) by the induction hypothesis. Then, KCϕ / hd(hd(h)) by Lemma 12. Finally, let formula ϕ be of the form HCψ. ( ) : Assume h HCψ. Then, by Deﬁnition 9, there is a strategy proﬁle s ΦC such that for any history h :: s :: w , if h C h and s =C s , then h :: s :: w ψ. Thus, by Lemma 3,

for any history h :: s :: w , if s =C s , then h :: s :: w ψ. (11)

Suppose that HCψ / hd(hd(h)). Then, HCψ hd(hd(h)) due to the maximality of the set hd(hd(h)). Hence, by Lemma 17, there is a history h :: s :: w such that s =C s and ψ hd(w ). Thus, ψ / hd(w ) due to the consistency of set hd(w ). Hence, by the induction hypothesis, h :: s :: w ψ, which contradicts statement (11). ( ) : Assume that HCψ hd(hd(h)). By Lemma 16, there is a strategy proﬁle s ΦC such that for any history h :: s :: w if h C h and s =C s , then ψ hd(w ). Hence, by the induction hypothesis, for any history h :: s :: w if h C h and s =C s , then h :: s :: w ψ. Therefore, h HCψ by Deﬁnition 9.

Theorem 2 If h ϕ for each history h of each regular epistemic transition system, then ϕ.

Proof. Suppose that ϕ. Consider any maximal consistent set X0 such that ϕ X0. Let h0 be a single-element sequence consisting of just set X0. By Deﬁnition 5, sequence h0 is a history of the canonical epistemic transition system ETS(X0). Then, h0 ϕ by Lemma 19. Therefore, h0 ϕ by Deﬁnition 9. Theorem 2 can be generalized to the strong completeness theorem in the standard way. We also believe that the number of states and the domain of choices in the canonical model can be made ﬁnite using ﬁltration on subformulae.

Conclusion We have extended the recent study of the interplay between knowledge and strategic coalition power ( Agotnes

and Alechina 2016; Fervari et al. 2017; Naumov and Tao 2017c; 2017a) to the case of perfect recall. Our main results are the soundness and the completeness theorems.

References Agotnes, T., and Alechina, N. 2012. Epistemic coalition logic: completeness and complexity. In Proceedings of the 11th International Conference on Autonomous Agents and Multiagent Systems-Volume 2 (AAMAS), 1099 1106. International Foundation for Autonomous Agents and Multiagent Systems. Agotnes, T., and Alechina, N. 2016. Coalition logic with individual, distributed and common knowledge. Journal of Logic and Computation. exv085. Agotnes, T.; Balbiani, P.; van Ditmarsch, H.; and Seban, P. 2010. Group announcement logic. Journal of Applied Logic 8(1):62 81. Agotnes, T.; van der Hoek, W.; and Wooldridge, M. 2009. Reasoning about coalitional games. Artiﬁcial Intelligence 173(1):45 79. Alur, R.; Henzinger, T. A.; and Kupferman, O. 2002. Alternating-time temporal logic. Journal of the ACM 49(5):672 713. Aminof, B.; Murano, A.; Rubin, S.; and Zuleger, F. 2016. Prompt alternating-time epistemic logics. KR 16:258 267. Belardinelli, F. 2014. Reasoning about knowledge and strategies: Epistemic strategy logic. In Proceedings 2nd International Workshop on Strategic Reasoning, SR 2014, Grenoble, France, April 5-6, 2014, volume 146 of EPTCS, 27 33. Borgo, S. 2007. Coalitions in action logic. In 20th International Joint Conference on Artiﬁcial Intelligence, 1822 1827. Broersen, J.; Herzig, A.; and Troquard, N. 2009. What groups do, can do, and know they can do: an analysis in normal modal logics. Journal of Applied Non-Classical Logics 19(3):261 289. Broersen, J. 2008. A Logical Analysis of the Interaction between Obligation-to-do and Knowingly Doing . Berlin, Heidelberg: Springer Berlin Heidelberg. 140 154. Fervari, R.; Herzig, A.; Li, Y.; and Wang, Y. 2017. Strategically knowing how. In Proceedings of the Twenty-Sixth International Joint Conference on Artiﬁcial Intelligence, IJCAI-17, 1031 1038. Goranko, V.; Jamroga, W.; and Turrini, P. 2013. Strategic games and truly playable effectivity functions. Autonomous Agents and Multi-Agent Systems 26(2):288 314. Goranko, V. 2001. Coalition games and alternating temporal logics. In Proceedings of the 8th conference on Theoretical aspects of rationality and knowledge, 259 272. Morgan Kaufmann Publishers Inc. Harding, J.; Powell, G., R.; Yoon, R.; Fikentscher, J.; Doyle, C.; Sade, D.; Lukuc, M.; Simons, J.; and Wang, J. 2014. Vehicle-to-vehicle communications: Readiness of v2v technology for application. Washington, DC: National Highway

Trafﬁc Safety Administration. (Report No. DOT HS 812 014). Jamroga, W., and Agotnes, T. 2007. Constructive knowledge: what agents can achieve under imperfect information. Journal of Applied Non-Classical Logics 17(4):423 475. Jamroga, W., and van der Hoek, W. 2004. Agents that know how to play. Fundamenta Informaticae 63(2-3):185 219. More, S. M., and Naumov, P. 2012. Calculus of cooperation and game-based reasoning about protocol privacy. ACM Trans. Comput. Logic 13(3):22:1 22:21. Naumov, P., and Tao, J. 2017a. Coalition power in epistemic transition systems. In Proceedings of the 2017 International Conference on Autonomous Agents and Multiagent Systems (AAMAS), 723 731. Naumov, P., and Tao, J. 2017b. Strategic coalitions with perfect recall. ar Xiv:1707.04298. Naumov, P., and Tao, J. 2017c. Together we know how to achieve: An epistemic logic of know-how. In 16th conference on Theoretical Aspects of Rationality and Knowledge (TARK), July 24-26, 2017, EPTCS 251, 441 453. Pauly, M. 2001. Logic for Social Software. Ph.D. Dissertation, Institute for Logic, Language, and Computation. Pauly, M. 2002. A modal logic for coalitional power in games. Journal of Logic and Computation 12(1):149 166. Sahlqvist, H. 1975. Completeness and correspondence in the ﬁrst and second order semantics for modal logic. Studies in Logic and the Foundations of Mathematics 82:110 143. (Proc. of the 3rd Scandinavial Logic Symposium, Uppsala, 1973). Sauro, L.; Gerbrandy, J.; van der Hoek, W.; and Wooldridge, M. 2006. Reasoning about action and cooperation. In Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 06, 185 192. New York, NY, USA: ACM. van Benthem, J. 2001. Games in dynamic-epistemic logic. Bulletin of Economic Research 53(4):219 248. van der Hoek, W., and Wooldridge, M. 2003. Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Studia Logica 75(1):125 157. van der Hoek, W., and Wooldridge, M. 2005. On the logic of cooperation and propositional control. Artiﬁcial Intelligence 164(1):81 119. Wang, Y. 2015. A logic of knowing how. In Logic, Rationality, and Interaction. Springer. 392 405. Wang, Y. 2016. A logic of goal-directed knowing how. Synthese.