# armstrongs_axioms_and_navigation_strategies__99676dcc.pdf

Armstrong s Axioms and Navigation Strategies

Kaya Deuser, Pavel Naumov Vassar College 124 Raymond Avenue Poughkeepsie, NY 12604 {kdeuser, pnaumov}@vassar.edu

The paper investigates navigability with imperfect information. It shows that the properties of navigability with perfect recall are exactly those captured by Armstrong s axioms from database theory. If the assumption of perfect recall is omitted, then Armstrong s transitivity axiom is not valid, but it can be replaced by a weaker principle. The main technical results are soundness and completeness theorems for the logical systems describing properties of navigability with and without perfect recall.

Introduction Navigation is a commonly encountered task by autonomous agents that need to reach a destination or, more generally, to ﬁnd a solution to a problem, where the solution is a sequence of instructions that transition a system from one state to another. This task is often performed when the agent does not have precise information about her current location. Examples of such agents are self-navigating missiles, self-driving cars, and robotic vacuum cleaners. Figure 1 depicts an example T0 of a transition system. This system consists of eight states a, . . . , h represented by the vertices of the graph. The agent cannot distinguish state a from state b and state c from state d, which is denoted by dashed lines connecting the indistinguishable states. The directed edges of the graph represent transitions that the system can make and the labels on these edges represent the instructions that the agent must give to do this. For example, if in state a the agent executes instruction 0, then the system transitions into state g, if, instead, the agent executes instruction 1, the system transitions into state e. Although in this paper we consider non-deterministic transition systems where the execution of the same instruction can transition the system into one of the several states, for the sake of simplicity the transition system T0 is deterministic. Note that, in system T0 the agent can navigate from state a to state c by using instruction 1 in state a and the same instruction 1 again in state e. However, a different sequence of instructions is required to reach state c from state b. As the agent cannot distinguish state a from state b, in state a she does not know which instructions to use to accomplish her

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

Figure 1: Transition System T0.

goal. Moreover, if the agent does reach state c, she cannot verify that the task is completed, because she cannot distinguish state c from state d. For this reason, in this paper instead of navigation between states, we consider navigation between equivalence classes of states with respect to the indistinguishability relation. For example, the agent can navigate from class ras ta, bu to class rcs tc, du by using instruction 1 in each state she passes.

Perfect Recall In order to achieve a goal, the agent would need to follow a certain strategy that must be stored in her memory. We assume that the strategy is permanently stored ( hardwired ) in the memory and cannot be changed during the navigation. For example, a robotic vacuum cleaner might be programmed to change direction when it encounters a wall, to make a circle when the dirt sensor is triggered, and to follow a straight path otherwise. A crucial question for us is if the vacuum cleaner can remember the walls and the dirty spots it has previously encountered. In other words, we distinguish an agent that can keep track of the classes of states she visited and the instructions she used from an agent who only knows her current state. We say that in the former case the agent has perfect recall and in the later she does not. A strategy of an agent without perfect recall can only use information available to her about the current state to decide which instruction to use. In other words, a strategy of such an agent is a function that maps classes of indistinguishable states into instructions. A strategy of an agent with perfect recall can use information about the history of previous tran-

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

sitions to decide which instruction to use. In other words, a strategy of such an agent is a function that maps classes of indistinguishable histories into instructions. We call the former memoryless strategies and the later recall strategies. In theory, a robotic vacuum cleaner without perfect recall is only equipped with read-only memory to store the strategy. A theoretical robotic vacuum with perfect recall in addition to read-only memory that contains the strategy also has an unlimited read-write memory that contains logs of all previous transitions. In practice, the most popular brand of robotic vacuum cleaners, Roomba, is only using read-write memory to store information, such as a cleaning schedule, that is not used for navigation. This means that Roomba is using a memoryless strategy. The other popular robotic vacuum cleaner, Neato, is scanning the room before cleaning to use this information for navigation purposes. Although, of course, Neato only has a read-write memory of a limited size, the navigation strategy used by Neato is an example of a recall strategy.

Examples Transition system T0 has a recall strategy to navigate from class ras to class res. This might be surprising, because the same strategy must work to navigate from both state a and state b of class ras to the only state e of class res. Yet, one would expect to use instruction 1 in state a and instruction 0 in state b to get to e. The recall strategy to navigate from class ras to class res consists in ﬁrst using instruction 0 once no matter what the starting state is, and then using instruction 1 until state e is reached. When this strategy is used starting from a state in class ras, the system ﬁrst transitions into state g, then into state a, and then ﬁnally into state e. This is a recall strategy because it uses a different instruction in state a depending if the system has already visited a state in class rgs or not. To show that there is no memoryless strategy to navigate from class ras to class res note that any such strategy will have to use the same instruction i0 at every visit to states a and b. If i0 0, then when the navigation starts in state b, the system stays locked in set of states ta, g, bu and never reaches state e. Similarly, if i0 1, then when the navigation starts in state b, the system stays locked in set of states tb, f, d, hu and never reaches state e. Thus, there is no memoryless strategy to navigate from class ras to class res. In some situation, even when there is a path between appropriate states, there might be no memoryless strategy and no recall strategy. For example, transition system T0 has no recall strategy to navigate from class rcs to class rgs. Indeed, if such a recall strategy exists, it would have to use the same instruction i0 when the system starts in either state c or state d. Suppose i0 0. Thus, if the system starts in state c it is locked in state h. Assume now that i0 1. Hence, if the system starts in state d it is locked in state h. Therefore, there is no recall strategy from class rcs to class rgs. Table 1 shows when memoryless strategies and recall strategies between classes of states of transition system T0 exist. In this table, letter m at the intersection of row x and column y denotes the existence of a memoryless strategy from class x to class y. Letter r denotes the existence of a recall strategy, but no memoryless strategy, and dash -

ta, bu tc, du teu tfu tgu thu ta, bu m m r r m r:

tc, du - m - - - r:

teu m m m r: m m tfu m m r: m m m tgu m m m m m m: thu - - - - - m

Table 1: Navigability between classes in system T0.

denotes that neither memoryless strategy nor recall strategy exist. Symbol : marks the cases that we have found to be interesting to think about.

Navigability between Sets As we have seen, there is a recall strategy, but no memoryless strategy, to navigate from class ras to class res. One can similarly show that there is no memoryless strategy to navigate from class ras to class rfs. However, if the goal is to navigate from class ras to either class res or to class rfs, then there is a memoryless strategy to do this. Indeed, consider a memoryless strategy that uses instruction 1 in every state. This strategy can transition the system from a state of class ras to a state of a class in set tres, rfsu. Thus, navigability between sets of classes can not be reduced to navigability between classes. For this reason, in this paper we study properties of navigability between sets of classes. If there is a strategy to navigate from a set of classes A to a set of classes B, then we write A B. It will be clear from the context if we refer to the existence of a memoryless strategy or a recall strategy.

Universal Properties of Navigability In the examples above we talked about properties of navigability for the transition system T0. In the rest of this paper we study universal properties of navigability between sets of classes that are true in all transition systems. An example of such a property is reﬂexivity: A B, where A Ď B. This property is true for both memoryless and recall strategies because absolutely any strategy can be used to navigate from a subset to the whole set. In fact, in this case the goal is achieved before the navigation even starts. Another example of a property of navigation which is universally true for both memoryless and recall strategies is augmentation: A B Ñ p A Y Cq p B Y Cq. It says that if there is a strategy to navigate from set A to set B, then there is a strategy to navigate from set A Y C to set B Y C. An example of a property which is universally true for recall strategies, but is not universally true for memoryless strategies is transitivity: A B Ñ p B C Ñ A Cq. It states that if there is a strategy to navigate from set A to set B and a strategy to navigate from set B to set C, then there is a strategy to navigate from set A to set C. To see that this property is not universally true for memoryless strategies, note that, in transition system T0, memoryless strategy that always uses instruction 0 can be used to navigate from set trasu to set trgsu and memoryless strategy that always uses instruction 1 can be used to navigate from set trgsu to set tresu. At the same time, as we have shown earlier, there is no

memoryless strategy to navigate from set trasu to set tresu. In this paper we show that reﬂexivity, augmentation, and transitivity principles form a sound and complete logical system that describes all universal properties of navigability by recall strategies. These are the three principles known in database theory as Armstrong s axioms (Garcia Molina, Ullman, and Widom 2009, p. 81), where they give a sound and complete axiomatization of functional dependency (Armstrong 1974). We also give a sound and complete axiomatization of universal properties of navigability by memoryless strategies. It consists of the reﬂexivity and augmentation principles mentioned above as well as the monotonicity principle p A Y Cq B Ñ A B. The latter principle is true for the recall strategies as well, but it is provable from Armstrong s axioms.

Literature Review Most of the existing literature on logical systems for reasoning about strategies is focused on modal logics. Logics of coalition power were developed by (Pauly 2001; 2002), who also proved the completeness of the basic logic of coalition power. Pauly s approach has been widely studied in 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). Alternative logical system were proposed by (More and Naumov 2012), (Wang 2015; 2016), and (Li and Wang 2017). (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. A completeness theorem for a logical system that combines coalition power and epistemic modalities was proven by ( Agotnes and Alechina 2012). The notion of a strategy that we consider in this paper is much more restrictive than the notion of strategy in the works mentioned above. Namely, we assume that the strategy must be based only on the information available to the agent. This is captured in our setting by requiring the strategy to be the same in all indistinguishable states or histories. This restriction on strategies has been studied before under different names. (Jamroga and Agotnes 2007) talk about knowledge to identify and execute a strategy , (Jamroga and van der Hoek 2004) discuss difference between an agent knowing that he has a suitable strategy and knowing the strategy itself . (van Benthem 2001) calls such strategies uniform . (Naumov and Tao 2017a) use the term executable strategy . (Naumov and Tao 2017b) proposed a complete trimodal logical system describing an interplay between distributed knowledge, uniform strategic power modality, and standard strategic power modality for achieving a goal by a coalition in one step. (Fervari et al. 2017) developed a complete logical system in a single-agent setting for uniform strategies to achieve a goal in multiple steps. (Naumov and Tao 2017a) developed a similar system for maintaining a goal in multi-agent setting. Our contribution is different from all of the above papers by being the ﬁrst to propose complete logical systems for recall strategies and memoryless strategies.

Paper Outline In the next section we deﬁne transition systems and the syntax of our logical systems. This section applies equally to recall and memoryless strategies. The rest of the paper is split into two independent sections. The ﬁrst of them proves the completeness of Armstrong s axioms for navigability under recall strategies and the second gives an axiomatization for memoryless strategies. The soundness of Armstrong s axioms with respect to the perfect recall semantics is given in the full version of this paper (Deuser and Naumov 2017).

Syntax and Semantics

In this section we formally deﬁne the language of our logical system, the notion of a transition system, and the related terminology. In the introduction, relation was viewed as a relation between equivalence classes of a given transition system. Thus, our language depends on these classes and changes from transition system to transition system. In order to have a single language for all transition systems we introduce a ﬁxed ﬁnite set of views V , whose elements act as names of the equivalence classes in any given transition system.

Deﬁnition 1 Φ is the minimal set of formulae such that

1. A B P Φ for all nonempty1 sets A, B Ď V , 2. ϕ, ϕ Ñ ψ P Φ for all formulae ϕ, ψ P Φ.

Each transition system speciﬁes a mapping of views into equivalence classes of states. Transitions between states under an instruction i are captured by a transition function Δi.

Deﬁnition 2 p S, , , I, tΔiui PIq is a transition system, if

1. S is a set of states, 2. is an equivalence (indistinguishability) relation on S, 3. is a function from V to S{ , 4. I is an arbitrary nonempty set of instructions , 5. Δi maps set S into nonempty subsets of S for each i P I.

We write a instead of paq, where a P V . An example of a transition system is system T0 depicted in Figure 1.

Deﬁnition 3 A ﬁnite sequence w0, i1, w1, . . . , in, wn, where n ě 0, is called a history if

1. wk P S for each k such that 0 ď k ď n, 2. ik P I, for each k such that 1 ď k ď n, 3. wk P Δikpwk 1q, for each k such that 1 ď k ď n.

For example, sequence g, 1, a, 1, e, 1, c, 0, h is a history for system T0. The set of all histories is denoted by H.

Deﬁnition 4 History h w0, i1, w1, . . . , in, wn is indistinguishable from history h1 w1 0, i1, w1 1, . . . , in, w1 n if wk w1 k for each k such that 0 ď k ď n.

1If one allows sets A and B to be empty, most of the proofs in this paper will remain unchanged, but both logical systems will need an additional axiom p A q for each nonempty set A.

For example, histories a, 0, g and b, 0, g are indistinguishable in transition system T0. Indistinguishability of histories of h and h1 is denoted by h h1. The equivalence class of history h with respect to this equivalence relation is denoted by vhw. Equivalence class of a state w with respect to equivalence relation is denoted by rws.

Lemma 1 If w0, i1, w1, . . . , wn w1 0, i1, w1 1, . . . , w1 n, then rwks rw1 ks for each k ď n. b

Deﬁnition 5 A memoryless strategy is a function from set S{ to set I. A recall strategy maps set H{ to set I.

We write srws and svhw instead of sprwsq and spvhwq.

Deﬁnition 6 An inﬁnite sequence w0, i1, w1, i2, w2 . . . is called a path under a memoryless strategy s if for each k ě 1

1. w0, i1, w1, i2, w2 . . . , wk 1 P H, 2. ik srwk 1s.

Lemma 2 For any history w0, i1, w1, . . . , in, wn and any memoryless strategy s, if ik srwk 1s for each k such that 1 ď k ď n, then there are states wn 1, wn 2, . . . and instructions in 1, in 2, . . . such that sequence w0, i1, w1, . . . , in, wn, in 1, wn 1, in 2, wn 2, . . . is a path under strategy s.

Proof. Elements in 1, wn 1, in 2, wn 2, . . . can be constructed recursively because (a) there is a state wk 1 P Δik 1pwkq for any state wk and any ik 1 P I by item 5 of Deﬁnition 2; (b) I by item 4 of Deﬁnition 2. b

Deﬁnition 7 An inﬁnite sequence w0, i1, w1, i2, w2 . . . is called a path under a recall strategy s if for each k ě 1

1. w0, i1, w1, i2, w2 . . . , wk 1 P H, 2. ik svw0, i1, w1, i2, w2 . . . , wk 1w.

Deﬁnition 8 A ta | a P Au, for all sets A Ď V .

Deﬁnition 9 For a given memoryless strategy or recall strategy s, let Pathsp Aq be the set of all paths w0, i1, w1, i2, w2 . . . under s such that rw0s P A .

Deﬁnition 10 Let set V isitsp Bq be the set of all paths w0, i1, w1, i2, w2 . . . under s such that rwks P B for some k ě 0.

We write V isitp Bq instead of V isitsp Bq when value of s is clear from the context.

Navigation with Recall Strategies

In this section we show that Armstrong s axioms give a complete axiomatization of navigability between sets of classes with recall strategies. We start with a formal semantics of navigability relation under recall strategies.

Deﬁnition 11 T ( A B if Pathsp Aq Ď V isitp Bq for some recall strategy s of transition system T.

Axioms The axioms of the logical system that we consider in this section are the tautologies in language Φ and the following additional principles known as Armstrong s axioms (Garcia-Molina, Ullman, and Widom 2009, p. 81):

1. Reﬂexivity: A B, where A Ď B,

2. Augmentation: A B Ñ p A Y Cq p B Y Cq,

3. Transitivity: A B Ñ p B C Ñ A Cq.

We write $ ϕ if formula ϕ is provable from these axioms using the Modus Ponens inference rule. We write X $ ϕ if ϕ is provable using a set of additional axioms X. A relatively straightforward proof of the following soundness theorem for this logical system can be found in the full version of this paper (Deuser and Naumov 2017).

Theorem 1 If $ ϕ, then T ( ϕ for every system T. b

Completeness In the rest of this section we prove the completeness of Armstrong s axioms with respect to the perfect recall semantics. We start by deﬁning a canonical transition system Tp Xq p V Y töu, , , I, tΔiui PIq for an arbitrary maximal consistent set of formulae X Ď Φ. The set of states of this transition system consists of a single state for each view, plus one additional state that we denote by symbol ö. Informally, the additional state is a sink or a black hole state from which there is no way out. State h in transition system T0 depicted in Figure 1 is an example of a black hole state. Note that the indistinguishability relation on the states of the canonical transition system is equality relation . That is, the agent has an ability to distinguish any two different states in the system. The fact that equality is suitable as an indistinguishability relation for the canonical transition system with perfect recall is surprising. The indistinguishability relation for the canonical transition system for memoryless strategies, discussed in the next section, is different from equality. Each view v P V is also a state in the canonical transition system. The equivalence class of state v consists of the state itself: rvs tvu. We deﬁne v to be class rvs.

Lemma 3 u P A iff rus P A for each view u P V and each set A Ď V . b

Informally, if set X contains formula A B, then we want the canonical transition system Tp Xq to have a recall strategy to navigate from set A tras | a P Au ttau | a P Au to set B trbs | b P Bu ttbu | b P Bu. It turns out that it is sufﬁcient to have just a single instruction that transitions the system from any state in set A to a state in set B. We denote this instruction by pair p A, Bq.

Deﬁnition 12 I tp A, Bq | A B P Xu.

Recall that assumption A B P X requires sets A and B to be nonempty due to Deﬁnition 1. As discussed above, for any instruction p A, Bq we deﬁne the nondeterministic transition function Δp A,Bq to transition the system from a state in A to a state in B. If used outside of set of states A, instruction p A, Bq transitions the system into black hole state ö:

Deﬁnition 13

Δp A,Bqpwq "B, if w P A, töu, otherwise.

This concludes the deﬁnition of the transition system Tp Xq. Next, for any recall strategy s and any set of states G Ď V , we deﬁne a family of sets of states t Gs nuně0. Informally, set Gs n is the set of all states from which strategy s draws the system into set G after at most n transitions. For any history h w0, i1, w1, . . . , in, wn, by hdphq we mean the state wn. Deﬁnition 14 For any recall strategy s and any nonempty set G Ď V , let chain of Gs 0 Ď Gs 1 Ď Ď V Y töu be deﬁned as 1. Gs 0 G, 2. Gs n 1 Gs n Y hdphq ˇˇ h P H and Δsvhwphdphqq Ď Gs n (

for all n ě 0. Note that this deﬁnition, in essence, has an existential quantiﬁer over history h. Thus, informally, strategy s is allowed to manipulate the history in order to draw the system into set G.

Lemma 4 ö R Gs n for each n ě 0.

Proof. We prove this statement by contradiction. Let n be the smallest non-negative integer number such that ö P Gs n. Note that n 0 because Gs 0 G Ď V by Deﬁnition 14. Thus, n ą 0. Hence, by Deﬁnition 14, there exists a history h such that hdphq ö and Δsvhwpöq Ď Gs n 1. Note that Δsvhwpöq töu by Deﬁnition 13. Therefore, ö P Gs n 1, which contradicts the choice of integer n. b

Deﬁnition 15 Gs 8 Ť

We now prove properties of the family of sets t Gs nuně0 that are needed to ﬁnish the proof of the completeness. Lemma 5 X $ tgu Gs n 1 for each integer n ě 1 and each state g P Gs n. Proof. By Deﬁnition 14, assumptions n ě 1 and g P Gs n imply that there is a history h such that hdphq g and

Δsvhwpgq Ď Gs n 1. (1)

Furthermore, by Deﬁnition 12, there are nonempty sets A, B Ď V such that svhw p A, Bq. Case I: g R A. Then, Δsvhwpgq töu by Deﬁnition 13. Hence, töu Ď Gs n 1 by equation (1), which contradicts Lemma 4. Case II: g P A. Then, $ tgu A by the Reﬂexivity axiom. At the same time, X $ A B by Deﬁnition 12. Thus, by the Transitivity axiom, X $ tgu B. Assumption g P A implies Δsvhwpgq B, by Deﬁnition 13. Thus, B Ď Gs n 1 due to equation (1). Hence, $ B Gs n 1 by the Reﬂexivity axiom. Finally, statements X $ tgu B and $ B Gs n 1 by the Transitivity axiom imply, using Modus Ponens inference rule twice, that X $ tgu Gs n 1. b

Lemma 6 For any n ě 1 and any views a1, . . . , an P V , if X $ taku B for each k ď n, then X $ ta1, . . . , anu B.

Proof. We prove this statement by induction on n. In the base case, X $ ta1u B due to the assumption of the lemma. By the induction hypothesis, X $ ta1, . . . , an 1u B. Thus, by the Augmentation axiom,

X $ ta1, . . . , an 1, anu B Y tanu. (2)

At the same time, X $ tanu B by the assumption of the lemma. Hence, by the Augmentation axiom X $ B Y tanu B. Thus, X $ ta1, . . . , an 1, anu B by statement (2) and the Transitivity axiom. b

Lemma 7 X $ Gs n Gs n 1 for each n ě 1. Proof. The statement of the lemma follows from Lemma 5 and Lemma 6. b

Lemma 8 X $ Gs n G for each n ě 0. Proof. We prove this statement by induction on integer n. In the base case, due to Deﬁnition 14, it sufﬁces to show that $ G G, which is an instance of the Reﬂexivity axiom. For the induction step, note that X $ Gs n Gs n 1 by Lemma 7. At the same time, X $ Gs n 1 G by the induction hypothesis. Hence, X $ Gs n G by the Transitivity axiom. b

Lemma 9 There is n ě 0, such that Gs 8 Gs n. Proof. Since Gs 0 Ď Gs 1 Ď Gs 2 Ď Ď V Y töu and set V is ﬁnite, there must exist an integer n such that Gs n Ť

kě0 Gs k. Therefore, Gs n Gs 8 by Deﬁnition 15. b

Lemma 10 Set pΔsvhwphdphqqqz Gs 8 is non-empty for each history h such that hdphq R Gs 8. Proof. Suppose Δsvhwphdphqq Ď Gs 8 for some history h. It sufﬁces to show that hdphq P Gs 8. Indeed, by Lemma 9 there is n such that Gs 8 Gs n. Thus, Δsvhwphdphqq Ď Gs n. Hence, hdphq P Gs n 1 by Deﬁnition 14. Then, hdphq P Gs 8 by Deﬁnition 15. b

Lemma 11 For any positive integer k and any history w0, i1, w1, . . . , wk 1, if wk 1 R Gs 8, then there is a state wk R Gs 8 such that w0, i1, w1, . . . , wk 1, ik, wk is a history, where ik svw0, i1, w1, . . . , wk 1w. Proof. By Lemma 10, set pΔikpwk 1qqz Gs 8 is not empty. Let wk be any state such that wk P Δikpwk 1q and wk R Gs 8. Then, w0, i1, w1, . . . , wk 1, ik, wk is a history by Deﬁnition 3. b

Lemma 12 For each state w0 R Gs 8 there exists a path w0, i1, w1, . . . under recall strategy s such that wk R Gs 8 for each k ě 0. Proof. Note that single-element sequence w0 is a history by Deﬁnition 3. Due to Lemma 11, there is an inﬁnite sequence w0, i1, w1, . . . such that for each integer k ě 1, 1. w0, i1, w1, . . . , wk 1 is a history,

2. ik svw0, i1, w1, . . . , wk 1w, 3. wk R Gs 8. By Deﬁnition 7, sequence w0, i1, w1, . . . is a path under recall strategy s. b

Lemma 13 If X $ A B, then Tp Xq ( A B. Proof. Assumption X $ A B implies p A, Bq P I by Deﬁnition 12. Consider recall strategy s such that svhw p A, Bq for each class of histories vhw. Consider any path w0, i1, w1, . . . under recall strategy s where rw0s P A . Then, w0 P A by Lemma 3. By Deﬁnition 11 and Deﬁnition 10 it sufﬁces to show that rw1s P B . Indeed, i1 p A, Bq by choice of recall strategy s. Thus, Δi1pw0q Δp A,Bqpw0q B by Deﬁnition 13 and due to the assumption w0 P A. By Deﬁnition 7, sequence w0, i1, w1 is a history. Hence, w1 P Δi1pw0q by Deﬁnition 3. Thus, w1 P Δi1pw0q B. Then, rw1s P B by Lemma 3. b

Lemma 14 If Tp Xq ( E G, then X $ E G. Proof. By Deﬁnition 11, assumption Tp Xq ( E G implies Pathsp Eq Ď V isitp Gq for some recall strategy s. Case I: E Ď Gs 8. By Lemma 9 there exists an integer n ě 0, such that E Ď Gs n. Thus, $ E Gs n by the Reﬂexivity axiom. At the same time, X $ Gs n G by Lemma 8. Therefore, X $ E G by the Transitivity axiom. Case II: E Ę Gs 8. Then, there is an element w0 P E such that w0 R Gs 8. Thus, by Lemma 12 there is a path π w0, i1, w1, . . . under recall strategy s such that wk R Gs 8 for all k ě 0. Hence, wk R G for all k ě 0 because G Gs 0 Ď Gs 8 by Deﬁnition 14 and Deﬁnition 15. Thus, rw0s P E and rwks R G for all k ě 0 by Lemma 3. Then, states in path π P Pathsp Eq by Deﬁnition 9 and π R V isitp Gq by Deﬁnition 10. Therefore, Pathsp Eq Ę V isitp Gq, which contradicts the choice of strategy s. b

Lemma 15 X $ ϕ iff Tp Xq ( ϕ for each ϕ P Φ. Proof. We prove this lemma by induction on the structural complexity of ϕ. The base case follows from Lemma 13 and Lemma 14. The induction case follows from the maximality and the consistency of set X in the standard way. b

We are now ready to state and prove the completeness theorem for the recall strategies. Theorem 2 If T ( ϕ for every system T, then $ ϕ. Proof. Suppose & ϕ. Let X be a maximal consistent set containing formula ϕ. Thus, Tp Xq ( ϕ by Lemma 15. Therefore, Tp Xq * ϕ. b

Navigation with Memoryless Strategies In this section we give a sound and complete axiomatization of navigability under memoryless strategies. We start by modifying Deﬁnition 11 to refer to memoryless strategies instead of recall strategies:

Deﬁnition 16 T ( A B if Pathsp Aq Ď V isitp Bq for some memoryless strategy s of a transition system T.

Axioms The logical system for memoryless strategies is the same as for recall strategies with the exception that the Transitivity axiom is replaced by the following principle:

3. Monotonicity: A1 B Ñ A B, where A Ď A1.

This principle can be derived from Armstrong s axioms.

Theorem 3 If $ ϕ, then T ( ϕ for every system T.

Proof. Soundness of the Reﬂexivity axiom and the Augmentation axiom is similar to the case of perfect recall, see Theorem 1. Soundness of the Monotonicity axiom follows from Pathsp Aq Ď Pathsp A1q, where A Ď A1. b

Completeness In the rest of this section we prove completeness of our logical system with respect to the memoryless semantics. First, we deﬁne a canonical transition system Tp Xq p S, , , I, tΔiui PIq for an arbitrary maximal consistent set of formulae X Ď Φ. Like in the perfect recall case, the canonical system has one state for each view and an additional black hole state ö. Unlike the previous construction, the new canonical transition system has more additional states besides state ö. Drawing on our original intuition of a transition system as a maze, we think about these new states as wormholes . For any sets of states A and B in the maze there is a wormhole state wp A, Bq that can be used to travel one-way from set A to set B. Then, S V Y töu Y twp A, Bq | A, B Ď V u. The agent can distinguish any two different nonwormhole states, but she can not distinguish wormholes. In other words, each non-wormhole state v P V Y töu forms its own indistinguishability class rvs tvu, while all wormholes belong to the same single indistinguishability class of wormholes. Like in the perfect recall case, for each v P V , we deﬁne v to be class rvs.

Lemma 16 u P A iff rus P A for each view u P V and each set A Ď V . b

Like in the canonical model for the perfect recall case, for sets A, B Ď V such that X $ A B, we introduce an instruction p A, Bq that can be used to navigate from set A to set B. Unlike the perfect recall case, we introduce such an instruction only if sets A and B are disjoint. This is an insigniﬁcant technical restriction that we use to simplify the proof of Lemma 19.

Deﬁnition 17

I tp A, Bq | X $ A B and A X B u.

Recall that assumption X ( A B implies that sets A and B are nonempty due to Deﬁnition 1. In the perfect recall case, instruction p A, Bq can be used to transition the system directly from a state in set A to a state in set B. In our case, this transition happens via the wormhole state wp A, Bq. In other words, when instruction p A, Bq is invoked in a state from set A, the system transitions into state wp A, Bq. When the same instruction is invoked in wp A, Bq, the system transitions into a state in B.

Deﬁnition 18

twp A, Bqu, if u P A, B, if u wp A, Bq, töu, otherwise.

Lemma 17 If X $ A B and sets A and B are disjoint, then Tp Xq ( A B. Proof. Assumptions X $ A B and A X B imply that p A, Bq P I, by Deﬁnition 17. Consider a memoryless strategy s such that spxq p A, Bq for each class x. By Definition 16, it sufﬁces to show that Pathsp Aq Ď V isitp Bq. Consider any w0, i1, w1, P Pathsp Aq. Then, by Definition 9, sequence w0, i1, w1, . . . is a path under strategy s such that rw0s P A . Hence, w0 P A by Lemma 16. Thus,

Δp A,Bqpw0q twp A, Bqu (3)

by Deﬁnition 18. At the same time, w1 P Δi1pw0q by Deﬁnition 3. Hence, w1 P Δsrw0spw0q by Deﬁnition 6. Thus, w1 P Δp A,Bqpw0q by the choice of strategy s. Then, w1 wp A, Bq by equation (3). Hence, Δp A,Bqpw1q B (4) by Deﬁnition 18. Similarly, w2 P Δi2pw1q by Deﬁnition 3. Hence, w2 P Δsrw1spw1q by Deﬁnition 6. Thus, w2 P Δp A,Bqpw1q by the choice of strategy s. Then, w2 P B by equation (4). Hence, rw2s P B by Lemma 16. Therefore, w0, i1, w1, i2, w2, P V isitp Bq by Deﬁnition 10. b

Lemma 18 If X $ A B, then Tp Xq ( A B. Proof. Suppose that X $ A B. If Az B . Thus, X $ Az B B by the Monotonicity Axiom. Hence, Tp Xq ( Az B B by Lemma 17. Therefore, Tp Xq ( A B due to the soundness of the Augmentation axiom, see Theorem 3. If Az B , then A Ď B. Therefore, Tp Xq ( A B due to the soundness of the Reﬂexivity axiom. b

Recall that all wormhole states belong to a single indistinguishability class of wormholes. For any memoryless strategy s, let p As, Bsq be the instruction assigned by strategy s to the class of wormholes. Once strategy s is ﬁxed, the states of the canonical transition system can be partitioned into ﬁve groups: set As, set V z As, the single element set töu containing the black hole state, the single element set twp As, Bsqu containing the wormhole state wp As, Bsq, and the set twp C, Dq | p C, Dq p As, Bsqu of all other wormholes. Deﬁnition 18 restricts transitions under strategy s that are possible between these ﬁve groups of states. For example, from set V z As one can transition either into set töu or into set twp C, Dq | p C, Dq p As, Bsqu. The arrows in Figure 2 show all possible transitions between these ﬁve groups of states allowed under Deﬁnition 18. These ﬁve groups of states can be further classiﬁed into above the line and below the line states, as shown. Notice that once the system transitions into one of the below the line states, it is trapped there and it will never be able to transition under the memoryless strategy s into an above the line state.

below the line

above the line

Figure 2: Transitions under memoryless strategy s.

Lemma 19 If Tp Xq ( E G, then X $ E G.

Proof. If E Ď G, then $ E G by the Reﬂexivity axiom. In the rest of the proof we suppose that there is e0 P Ez G. By Deﬁnition 16, assumption Tp Xq ( E G implies that there exists a memoryless strategy s such that Pathsp Eq Ď V isitp Gq. First, we show that Ez G Ď As. Suppose there is a view e1 P E such that e1 R G and e1 R As. By Deﬁnition 3, single-element sequence e1 is a history. Thus, by Lemma 2, there is a path π P Pathsp Eq that starts with state e1. Since path π starts in a state from set V z As, all non-initial states of this path are below the line , see Figure 2. Hence, neither of the states in path π belong to set G, because e1 R G and none of the states below the line are in set G either. Thus, π P Pathsp Eq and π R V isitp Gq, which contradicts the choice of strategy s. Therefore, Ez G Ď As. In particular e0 P As. Second, we show that sre0s p As, Bsq. Suppose that sre0s p C, Dq, where p C, Dq p As, Bsq. If e0 R C, then π e0, p C, Dq, ö, srös, ö, srös, . . . is a path under strategy s by Deﬁnition 6 and Deﬁnition 18. Note that π R V isitp Gq because e0 R G and π P Pathsp Eq. This contradicts Pathsp Eq Ď V isitp Gq. Similarly, if e0 P C, then sequence π e0, p C, Dq, wp C, Dq, p As, Bsq, ö, srös, . . . is a path such that π R V isitp Gq and π P Pathsp Eq, which again contradicts Pathsp Eq Ď V isitp Gq. Third, we prove that Bs Ď G. Suppose that there is a state b0 P Bsz G. By Deﬁnition 3, Deﬁnition 18, and the choice of instruction p As, Bsq, sequence e0, p As, Bsq, wp As, Bsq, p As, Bsq, b0 is a history. Thus, by Lemma 2, there is a path π P Pathsp Eq that starts as e0, p As, Bsq, wp As, Bsq, p As, Bsq, b0. Assumption b0 P Bsz G implies that b0 P V z As because sets As and Bs are disjoint by Deﬁnition 17. Thus, path π after state b0 contains only states below the line , see Figure 2, none of which are in set G Ď V . Recall also that e0, b0 R G by the choice of states e0 and b0. Thus, π P Pathsp Eq and π R V isitp Gq, which again contradicts Pathsp Eq Ď V isitp Gq. Note that X $ As Bs by Deﬁnition 17. Hence, X $ p As Y Gq p Bs Y Gq by the Augmentation axiom. Thus, X $ p As Y Gq G because Bs Ď G. At the same time,

Ez G Ď As implies that E Ď As YG. Therefore, X $ E G by the Monotonicity axiom. b

Lemma 20 X $ ϕ iff Tp Xq ( ϕ for each ϕ P Φ.

Proof. We prove this lemma by induction on the structural complexity of ϕ. The base case follows from Lemma 18 and Lemma 19. The induction case follows from the maximality and the consistency of set X in the standard way. b

We are now ready to state and prove the completeness theorem for memoryless strategies.

Theorem 4 If T ( ϕ for every system T, then $ ϕ.

Proof. Suppose & ϕ. Let X be a maximal consistent set containing formula ϕ. Thus, Tp Xq ( ϕ by Lemma 20. Therefore, Tp Xq * ϕ. b

In this paper we have shown that the properties of navigability under perfect recall strategies are exactly those described by Armstrong s axioms for functional dependency in database theory. In the absence of perfect recall, the Transitivity axiom is no longer valid, but it could be replaced by the Monotonicity axiom.

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.; 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. Armstrong, W. W. 1974. Dependency structures of data base relationships. In Information Processing 74 (Proc. IFIP Congress, Stockholm, 1974). Amsterdam: North-Holland. 580 583. 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.

Deuser, K., and Naumov, P. 2017. Armstrong s axioms and navigation strategies. ar Xiv:1707.04106. 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. Garcia-Molina, H.; Ullman, J.; and Widom, J. 2009. Database Systems: The Complete Book. Prentice-Hall, second edition. 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. 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. Li, Y., and Wang, Y. 2017. Achieving while maintaining: A logic of knowing how with intermediate constraints. In Logic and Its Applications: Proceedings of 7th Indian Conference, ICLA 2017, Kanpur, India, January 5-7, 2017, 154 167. Springer. 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. 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. 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.