Intelligence in Strategic Games (Extended Abstract)

1 Introduction

The Battle of the Atlantic was a classical example of the matching pennies game. British (and American) admirals were choosing routes of the allied convoys and the Germans picked routes of their U-boats. If their trajectories crossed, the Germans scored a win, if not the allies did. Neither of the players appeared to have a strategy that would guarantee a victory.

The truth, however, was that during the most of the battle one of the sides had exactly such a strategy. First, it was the British who broke German Enigma cipher in summer of 1941. Although the Germans did not know about the British success, they changed codebook and added fourth wheel to Enigma in February 1942 thus preventing the British from decoding German messages. The very next month, in March 1942, German navy cryptography unit, B-Dienst, broke the allied code and got access to convoy route information. The Germans lost their ability to read allied communication in December 1942 due to a routine change in the allied codebook. The same month, the British were able to read German communication as a result of capturing codebook from a Uboat inMediterranean. InMarch 1943, the Germans changed codebook again and, unknowingly, disabled British ability to read German messages. Simultaneous, the Germans caught up and started to decipher British transmissions again [Budiansky, 2002; Showell, 2003].

∗This paper is an extended abstract of an article in Journal of Artificial Intelligence Research [Naumov and Yuan, 2021].

At almost any moment during these two years one of the sides was able to read the communications of the other side. However, the two sides never have been able to read each other's messages at the same time to notice that the other side knows more than it should have known. As a result, neither of themwas able to figure out that their own code is insecure. Finally, in May 1943, with the help of US Navy, the British cracked German messages while the Germans still were reading British. It was the first time the allies understood that their code was insecure. A new convoy cipher was immediately introduced and the Germans have never been able to break it again, while the allies continued reading Enigma-encrypted transmissions till the end of the war [Budiansky, 2002].

In this article, we study coalition power in strategic games assuming that the coalition has intelligence information about the moves of all or some of its opponents. Throughout the article, we refer to the information about the future actions of the other agents simply as "the intelligence". We write [C]Iϕ if a coalition C has a strategy to achieve an outcome ϕ in one step as long as the coalition has the intelligence about the move of each agent in set I. For example,

Strategic games could be generalized to strategic games with imperfect information. Unlike perfect information strategic games, the initial state in an imperfect information game could be unknown to the players. For example, consider a hypothetical setting in which a British convoy and a German U-boat have to choose between three routes from point A to point B: route 1, route 2, and route 3, see Figure 1. Let us furthermore assume that it is known to both sides that one of these routes is blocked by Russian naval mines. Although the mines are located along route 1, neither the British nor the Germans know this. If the British have an access to the intelligence about German U-boats, then, in theory, they have a strategy to save the convoy. For example, if the Germans will use route 2, then the British can use route 3. However, since the British do not know the location of the Russian mines, even after they receive information about German plans, they still would not know how to save the convoy.

Modality [C]∅ϕ is the coalitional power modality proposed by Marc Pauly [Pauly, 2001; Pauly, 2002]. He gave a sound and complete axiomatization of this modality in the case of perfect information strategic games. It has been suggested in several recent works that, in the case of the games with imperfect information, strategic power modality in Marc Pauly logic should be restricted to existence of knowhow 1 strategies [ ˚Agotnes and Alechina, 2019; Naumov and Tao, 2017a; Fervari et al., 2017; Naumov and Tao, 2018b; Naumov and Tao, 2018c; Naumov and Tao, 2018a; Cao and Naumov, 2020]. That is, modality [C]ϕ should stand for "coalition C has a strategy, it distributively knows that it has a strategy, and it distributively knows what the strategy is". In this article we adopt this approach to strategic power with intelligence. For example, in the imperfect information setting depicted in Figure 1, after receiving the intelligence report, the British have a strategy, they know that they have a strategy, but they do not know what the strategy is:

At the same time, since the Russians presumably know the location of their mines,

This article contains two main technical results. First, we show that know-how with intelligence modality [C]Iϕ cannot be defined through the standard know-how modality. Second, we give a complete logical system that describes the interplay between the coalition power with intelligence modality [C]I and the distributed knowledge modality KC in the imperfect information setting. The most interesting axiom of our system is a generalized version of Marc Pauly's [Pauly, 2001; Pauly, 2002] Cooperation axiom that connects intelligence I and coalition C parameters of the modality [C]I .

2 Games with Imperfect Information

For any sets X and Y , by XY we mean the set of all functions from Y to X. Throughout the article we assume a fixed (possibly infinite) set of agents A and a nonempty set of propositional variables.

Definition 1. A game is a tuple (W, {∼a}a∈A,∆,M, π), where

1 Know-how strategies were studied before under different names. While Jamroga and ˚Agotnes talked about "knowledge to identify and execute a strategy" 2007, Jamroga and van der Hoek discussed "difference between an agent knowing that he has a suitable strategy and knowing the strategy itself" 2004. Van Benthem called such strategies "uniform" 2001. Wang gave a complete axiomatization of "knowing how" as a binary modality 2015; 2018, but his logical system does not include the knowledge modality.

1. W is a set of states,
2. ∼a is an "indistinguishability" equivalence relation on set W for each agent a ∈ A,
3. ∆ is a nonempty set, called the "domain of actions",
4. M ⊆ W × ∆A × W is a relation called "aggregation mechanism",
5. π is a function that maps propositional variables to subsets of W.

A function δ from set ∆A is called a complete action profile.

Figure 2 depicts a diagram of the Battle of the Atlantic game with imperfect information as described in the introduction. For the sake of simplicity, we treat the British, the Germans, and the Russians as single agents, not groups of agents. The game has five states: 1, 2, 3, s, and d. States 1, 2, and 3 are three "initial" states that correspond to possible locations of Russian mines along route 1, route 2, or route 3. Neither the British nor the Germans can distinguish these states, which is shown in the diagram by labels on the dashed lines connecting these three states. The Russians know location of the mines, and, thus, they can distinguish these states. The other two states are "final" states s and d that describe if the convoy made it safe (s) or was destroyed (d) by either a U-boat or a mine. The designation of some states as "initial" and others as "final" is specific to the Battle of the Atlantic game. In general, our Definition 1 does not distinguish between such states and we allow games to take multiple consecutive transitions from one state to another.

The domain of actions ∆ in this game is {1, 2, 3}. For the British and the Germans actions represent the choice of routes that they make for their convoys and U-boats respectively. The Russians are passive players in this game. Their action does not affect the outcome of the game. Technically, a complete action profile is a function δ from set {British,Germans, Russians} into set {1, 2, 3}. Since, there are only three players in the Battle of the Atlantic game, it is more convenient to represent function δ by triple bgr ∈ {1, 2, 3}3 , where b is the action of the British, g is the action of the Germans, and c is the action of the Russians.

The mechanism M of the Battle of the Atlantic game is captured by the directed edges in Figure 2 labeled by complete action profiles. Since value r in a profile bgr does not affect the outcome, it is omitted on the diagram. For example, directed edge from state 1 to state s is labeled with 23

and 32. This means that the mechanism M contains triples (1, 231, s), (1, 232, s), (1, 233, s), (1, 321, s), (1, 322, s), and (1, 323, s).

The definition of a game that we use here is more general than the one used in the original Marc Pauly's semantics of the logic of coalition power. Namely, we assume that the mechanism is a relation, not a function. On one hand, this allows us to talk about nondeterministic games where for each initial state and each complete action profile there might be more than one outcome. On the other hand, this also allows no outcome to exist for some combinations of the initial states and the complete action profiles. If in a given state under a given complete action profile there is no next state, then we interpret this as termination of the game. This resembles a user choosing to quit a computer application: once the quit button is pressed, the application terminates without reaching any new state. If needed, games with termination can be excluded and an additional axiom ¬[C]∅⊥ be added to the logical system. The proof of the completeness will remain mostly unchanged.

Definition 2. For any states w, w′ ∈ W and any coalition C, let w ∼C w′ if w ∼a w′ for each agent a ∈ C.

In particular, w ∼∅ w′ for any two states of the game.

Lemma 1. For any coalition C, relation ∼C is an equivalence relation on set W.

3 Syntax and Semantics

In this section, we define the syntax and the semantics of our formal system. By a coalition we mean any finite subset of the set of all agents A. Finiteness of coalitions will be important for the proof of the completeness.

Definition 3. Let Φ be the minimal set of formulae such that

1. p ∈ Φ for each propositional variable p,

1. ϕ → ψ, ¬ϕ ∈ Φ for all ϕ, ψ ∈ Φ,
2. KCϕ ∈ Φ for each formula ϕ ∈ Φ and each coalition C ⊆ A,
3. [C]Bϕ ∈ Φ for each formula ϕ ∈ Φ and all disjoint coalitions B, C.

In other words, the language of our logical system is defined by grammar:

where coalitions C and B are disjoint. Formula KCϕ stands for "coalition C distributively knows ϕ" and formula [C]Bϕ for "coalition C distributively knows strategy to achieve ϕ as long as it gets the intelligence on actions of coalition B". We assume that Boolean constants ⊤ and ⊥ are defined through negation, implication, and a propositional variable in the standard way.

By an action profile of a coalition C we mean any function from set ∆C . For any two functions f, g, we write f =X g if f(x) = g(x) for each x ∈ X.

Next is the key definition of this article. Its part 5 gives the semantics of modality [C]B. This part uses state w′ to capture the fact that the strategy succeeds in each state indistinguishable by coalition C from the current state w. In other words, the coalition C knows that this strategy will succeed. Except for the addition of coalition B and its action profile β, this is essentially the same definition as the one used in [ ˚Agotnes and Alechina, 2019; Naumov and Tao, 2017a; Fervari et al., 2017; Naumov and Tao, 2017b; Naumov and Tao, 2018c; Naumov and Tao, 2018b; Naumov and Tao, 2018a].

Definition 4. For any game (W, {∼a}a∈A,∆,M, π), any state w ∈ W, and any formula ϕ ∈ Φ, let satisfiability relation w ⊩ ϕ be defined as follows:

1. w ⊩ p, if w ∈ π(p), where p is a propositional variable,
2. w ⊩ ¬ϕ, if w ⊮ ϕ,
3. w ⊩ ϕ→ψ, if w ⊮ ϕ or w ⊩ ψ,
4. w ⊩ KCϕ, if w′ ⊩ ϕ for each w′ ∈ W such that w ∼C w′ ,
5. w ⊩ [C]Bϕ, if for any action profile β ∈ ∆B of coalition B there is an action profile γ ∈ ∆C of coalition C such that for any complete action profile δ ∈ ∆A and any states w′ , u ∈ W if β =B δ, γ =C δ, w ∼C w′ , and (w′ , δ, u) ∈ M, then u ⊩ ϕ.

For example, for the game depicted in Figure 2,

1 ⊩ [British, Russians]Germans(Convoy is saved).

Indeed, statement 1 ∼British, Russians w′ is true only for one state w′ ∈ W, namely state 1 itself. Then, for any action profile β ∈ {1, 2, 3}{Germans} of the singlemember coalition {Germans} we can define action profile γ ∈ {1, 2, 3}{British, Russians} as, for example,

In other words, if profile β assigns the Germans route 2, then profile γ assigns the British route 3 and vice versa. Assignment of an action to the Russians in not important. This way, no matter what the Germans' action is, the British convoy will avoid both the German U-boat and the Russian mines in the game that starts from state w′ = 1. At the same time,

because the British cannot distinguish states 1, 2, and 3 without the Russians. In other words, 1 ∼British w′ for any state w′ ∈ {1, 2, 3}. Thus, for each action profile β ∈ {1, 2, 3}{Germans} we need to have a single action profile γ ∈ {1, 2, 3}{British, Russians} that would bring the convoy to state s from any of the states 1, 2, and 3. Such profile γ does not exist because, even if the British know where the Germans U-boat will be, there is no single strategy to choose path that would avoid Russian mines from all three indistinguishable states 1, 2, and 3.

Note that item 4 of Definition 4 interprets the knowledge modality KC as distributed knowledge of coalition C. Similarly, the knowledge of "how", implicitly referred to by item 5 of the same definition through indistinguishability relation ∼C, is also distributed knowledge of coalition C. Thus, even if a coalition knows how to achieve ϕ, it is possible that no single individual member of the coalition might know how to do this. In order for the coalition to execute a strategy that it knows, its members might need to communicate with each other to "assemble" the distributed knowledge. The mechanism and the result of such a communication is not a trivial issue. For example, if a statement ϕ is distributively known to a coalition, then ϕ might even be false after such a communication [ ˚Agotnes andW´ang, 2017]. In this article, following the existing tradition in the logics of distributively knowing strategy, we investigate the properties of distributed knowledge on an abstract level, without considering the communication between the agents required to execute the strategy. Of course, one can potentially consider the other forms of group knowledge such as individual knowledge (each agent in the group knows) and common knowledge. However, know-how strategies based on either of the last two forms of knowledge do not satisfy the Cooperation axiom listed in Section 4. As a result, they are significantly less interesting from the logical point of view.

Finally, observe that the formula K∅ϕ means that statement ϕ is satisfied in all states of the game. Modality K∅ is sometimes referred to as universal modality.

4 Axioms

In this section, we present our formal logical system, KnowHow Logic with the Intelligence, for reasoning about the interplay between distributed knowledge modality KC and know-how with intelligence modality [C]B.

Definition 5. In addition to the propositional tautologies in language Φ, the axioms of the Know-How Logic with the Intelligence are

1. Truth: KCϕ→ϕ,
2. Distributivity: KC(ϕ→ψ) → (KCϕ→KCψ),
3. Negative Introspection: ¬KCϕ→KC¬KCϕ,
4. Epistemic Monotonicity: KCϕ → KDϕ, where C ⊆ D,
5. Strategic Introspection: [C]Bϕ→KC[C]Bϕ,
6. Empty Coalition: K∅ϕ→ [∅]∅ϕ,
7. Cooperation: for any pairwise disjoint sets B,C, and D, [C]B(ϕ→ψ) → ([D]B,Cϕ→ [C,D]Bψ),
8. Intelligence Monotonicity: [C]Bϕ → [C]B′ϕ, where B ⊆ B′ ,
9. None to Analyze: [∅]Bϕ→ [∅]∅ϕ.

Note that in the Cooperation axiom above and often throughout the rest of the article we abbreviate B∪C as B, C. However, we keep writing B ∪ C when notation B, C could be confusing.

Next, we define two derivability relations. A unary relation ⊢ ϕ and a binary relation X ⊢ ϕ, where X ⊆ Φ is a set of formulae and ϕ ∈ Φ is a formula.

Definition 6. ⊢ ϕ if there is a finite sequence of formulae that ends with ϕ such that each formula in the sequence is either an axiom or could be obtained from the previous formulae using the Modus Ponens, the Epistemic Necessitation, or the Strategic Necessitation inference rules:

If ⊢ ϕ, then we say that ϕ is a theorem of our logical system.

Definition 7. X ⊢ ϕ if there is a finite sequence of formulae that ends with ϕ such that each formula in the sequence is either a theorem, or an element of X, or could be obtained from the previous formulae using only the Modus Ponens inference rules.

Note that if set X is empty, then statement X ⊢ ϕ is equivalent to ⊢ ϕ. Thus, instead of ∅ ⊢ ϕ we write ⊢ ϕ. We say that set X is consistent if X ⊬ ⊥.

5 Main Results

By Φ- we denote the fragment of language Φ in which modality in occurrences of modality [B]Cϕ set C is empty. The proofs of the following results appear in the full version of this paper [Naumov and Yuan, 2021].

Theorem 1 (undefinability). The modality [C]Bϕ is not definable in language Φ-.

Theorem 2 (soundness). For any state w ∈ W of any game (W, {∼a}a∈A,∆,M, π), any set of formulae X ⊆ Φ, and any formula ϕ ∈ Φ, if w ⊩ χ for each formula χ ∈ X and X ⊢ ϕ, then w ⊩ ϕ.

Theorem 3 (completeness). If Y ⊬ ϕ, then there is a state w of a game such that w ⊩ χ for each χ ∈ Y and w ⊮ ϕ.

6 Conclusion

In this article, we proposed the notion of a strategy with intelligence, proved that corresponding know-how modality is not definable through the standard know-how modality, and gave a sound and complete axiomatization of a bimodal logic that describes the interplay between the strategic power with intelligence and the distributed knowledge modalities in the setting of strategic games with imperfect information.

A natural question is decidability of the proposed logical system. Unfortunately, the standard filtration technique [Gabbay, 1972] can not be easily applied here to produce a finite model. Indeed, it is crucial for the proof of the completeness that for each action there is another action with a higher value of the "key" component. Thus, for the proposed construction to work, the domain of choices must be infinite. One perhaps might be able to overcome this by changing the second component of the action from an infinite linear ordered set to a finite circularly "ordered" set as in rock-paper-scissors game, but we have not been able to prove this.