Data-Informed Knowledge and Strategies (Extended Abstract)

1 Introduction

With technological progress, more information is either stored in databases and remote servers or exchanged directly between autonomous agents. What machines know and can do will rely more and more on the access to such information rather than the individual memory. Personal assistants, like Amazon Alexa, often use external sources of data such as Wikipedia and Answers.com. Self-driving cars can access map updates in the cloud. Vehicular ad hoc networks (vehicular cloud) are being designed to share traffic and other localised information between nearby vehicles [Ahmed et al., 2019]. Future medical robots will be treating patients with highly contagious diseases relying on knowledge and skills of doctors and nurses placed in safe remote locations [Zhu et al., 2021].

In this article, we formally define and study the properties of knowledge and abilities in a multiagent setting where data is decoupled from the agents.

1.1 Deep Sea Rescue Example

Suppose that three naval rescue robots, Bluewater (b), Lucky (l), and Extreme (e), are sent on a mission to save the crew of a sunk submarine that has one hour of oxygen left. The area in which the submarine sank could be divided into 9 squares depicted in Figure 1. The actual location of the submarine (second row, first column) is not known to the robots and it takes one hour for one robot to search through one square. Note that even a single robot in this setting has a strategy to save the crew (search first square in the second row), but the robot does not know that this strategy would guarantee the success of the rescue operation.

∗This paper is an extended abstract of an article in Artificial Intelligence [Jiang and Naumov, 2022].

Let us now suppose that the rescue robots somehow learned that the sub is located in the second row. Then, they know a joint strategy to save the crew. The strategy consists in three of them searching through different squares in the second row. Moreover, observe that anyone who knows in which row (r) the sub is, knows the strategy that Bluewater, Lucky, and Extreme can use to save the crew:

We write SCX ϕ to state that the knowledge of a strategy that coalition C can use to achieve ϕ could be gained from the values of variables in set X. In other words, anyone who knows the values of the variables in set X knows the strategy that coalition C can use to achieve ϕ. In this context, we refer to the set of variables X as "dataset". We read SCX ϕ as "dataset X informs a strategy of coalition C to achieve ϕ". Note that for SCX ϕ to be true, it is not significant whether the members of the coalition C themselves know values of variables in dataset X. Furthermore, any knowledge that the members of the coalition C might have does not affect if SCX ϕ is true or not. For this reason, we refer to the members of the coalition C as actors rather than agents.

Recall that Bluewater, just like each of the other robots, has a strategy to save the crew (search the first square in the second row), but it is not true that anyone who knows r would know how Bluewater can do this. Thus,

In other words, Bluewater's strategy to rescue the crew is not informed by the dataset {r}. The same dataset also does not inform the strategy for Bluewater and Lucky:

Let us further assume that the two of the squares contain old shipwrecks. These are the second square in the first row and the third square in the second row, Figure 1.

Let Boolean variable s is true in the squares that contain shipwrecks and is false in the other squares. Observe that everyone who knows the row and the ship wracks data (s) of the square where the sub has been sunk, would know that the sub is located in one of the first two squares in the second row. Thus, any such person would know how Bluewater and Lucky can achieve the goal:

The validity of the last statement depends on the location of the sub. It would not be true if the sub is located in any of the squares of the third row. In other words, the satisfiability of statement SCX ϕ depends on which of the possible worlds is the current world. In the setting of our example, there are nine possible worlds, corresponding to different locations of the sub. By default, all statements that we consider in this section assume that the current world is the one where the sub is located in the first cell of the second row. Observe that the column (c) and the wreck data do not inform a strategy for Bluewater and Lucky:

because all three squares in the first column have no wrecks.

Let us also assume that the ocean floor in some squares is covered with sand and in the others with rocks. The squares with rock floor are shaded in gray in Figure 1. Since, the sub is laying on the sandy floor and only two of squares with sandy floor have no shipwrecks, everyone who knows the floor type and the ship wreck data, knows the strategy that Bluewater and Lucky can use to save the crew:

The validity of the last statement also depends on the current world. It would not be true if the sub was laying on rocky floor. One might also observe that row, floor type, and wreck data inform a strategy for Bluewater alone to save the crew:

The numbers in Figure 1 show the depth (d), in meters, of the ocean in each square. Observe that the depth of the ocean in white (sandy) squares is equal to either 115 or 110. Thus, anyone who knows the type of the floor on which the sub is laying knows that d is equal to either 115 or 110. We write this as

Kf ("The sub is laying at either depth 115 or depth 110").

In general, we write KXϕ if the knowledge of ϕ about the current world can be gained from the values of variables in dataset X. In other words, anyone who knows the values of the variables in dataset X for the current world knows that statement ϕ is true in the current world. We read KXϕ as "dataset X informs the knowledge of statement ϕ".

Note that variable f does not inform strategy for Bluewater and Lucky to save the crew:

because there are four different squares with sandy floor. However, everyone who knows the value of f knows that the depth at which the sub is laying is either 115 or 110. Thus, everyone who knows the value of f knows that the knowledge of variable d reduces the number of locations where the sub is to just two. Hence, everyone who knows the value of f knows that variable d informs a strategy for Bluewater and Lucky to save the crew:

In this article, in addition to data-informed modalities SXϕ and KXϕ, we also consider dependency expression X ▷ Y . It means that, in the current world, the knowledge of the values of variables in dataset X informs the knowledge of the values of variables in dataset Y . We read X ▷ Y as "dataset X informs dataset Y ". For example, note that all squares in the first column have no wrecks. Thus, the knowledge of the column in which the sub is located informs the knowledge of the wreck data: c▷s. At the same time, ¬(r ▷s) because no cells in the second row have the same wreck data.

2 Games

Throughout this article, we assume a fixed nonempty set of propositional variables P , a fixed set of data variables V , and a fixed set of actors A. Recall that we use term "actors" rather than "agents" to emphasise that the knowledge in our setting is decoupled from the actions.

By a dataset we mean an arbitrary subset of V . In this section, we introduce models of our logical system, called games. Informally, a game includes a set of possible states and each of data variables is assigned a value in each of the states. An actor who is informed about a dataset cannot distinguish two states when all variables in the dataset have the same values in both states. Note that it is only important if a given variable has the same value in two given states and it is not important what exactly the value of the variable is. Thus, for the sake of simplicity, our formal definition below does not include values of variables. It only contains an indistinguishability relation ∼x on possible states associated with each data variable x ∈ V . Intuitively, two states are indistinguishable by a data variable x if this variable has the same value in both states. In this article, by BA we denote the set of all functions from set A to set B.

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

1. W is a (possibly empty) set of states,

1. ∼x is an indistinguishability equivalence relation on set W for each data variable x ∈ V ,
2. ∆ is a nonempty set of "actions",
3. M ⊆ W ×∆A ×W is a "mechanism" of the game,
4. π(p) ⊆ W for each propositional variable p ∈ P .

By a complete action profile we mean an arbitrary element of the set ∆A. By a coalition we mean an arbitrary subset C ⊆ A of actors. By an action profile of a coalition C we mean an arbitrary element of the set ∆C .

Our introductory example has 9 initial states, representing the different locations of the sub, and two final states ("saved" and "not saved"). Note that although in this example the states are naturally divided into initial and final, the same is not true in general. In Definition 1, we assume that, the game might make multiple consecutive transitions between states.

In our example, the set V contains variables r, c, s, f, and d. If w is the current state, in which the sub is located at (2, 1), and w′ is the state in which the sub is located at (1, 2), then w ∼f w′ and w ∼d w′ because squares (2, 1) and (1, 2) have the same floor type and the same depth.

To keep the notations simple, in Definition 1, we assume that the set of actions ∆ is the same for all actors in all states. This assumption is not significant for our results because available actions can always be combined into a single set and the additional actions can be assigned some "default" meaning. At the same time, our assumption that set ∆ is nonempty is significant. Without this assumption, the Public Knowledge axiom, introduced in Section 4, is not valid.

Note that the mechanism M is a relation, not a function. Informally, (w, δ,w′ ) ∈ M if under complete action profile δ ∈ ∆A the game can transition from state w to state w′ . Defining mechanism as a relation allows us to model nondeterministic games where from a given state under a given complete action profile the game can transition to one of several possible "next" states. Note that we also allow that for some combinations of a state and a complete action profile there might be no next states. We interpret this as a termination of the game.

In our introductory example, the actions consist in searching a square. Since there are nine squares, the set ∆ has nine actions corresponding to these squares. The game transitions from the current initial state w = (2, 1) to final state "saved" if at least one of the actions is searching in the square where the sub is laying. Otherwise, the game transitions to the final state "not saved". Note that we do not allow the actors to repeat the game. Thus, no further transitions can be made from either of the two final states. We model this by assuming that the mechanismM of this game has no triples whose first element is one of the final states of the game.

As common in modal logics, we interpret propositional variables as properties of states. Informally, w ∈ π(p) if propositional variable p is true in state w ∈ W. This is different from the setting of [Baltag and van Benthem, 2021], where the authors have used atomic predicates instead of propositional variables. The predicates are true or false depending not on the state, but on the values of data variables in the state. In other words, the atomic formulae in their setting capture properties of the variables rather than of the states.

We discuss the significance of this difference in the next section.

3 Syntax and Semantics

Language Φ of our logical system is defined by the grammar

where p ∈ P is a propositional variable, X ⊆ V is a dataset, and C ⊆ A is a coalition. We read X ▷ Y as "dataset X informs dataset Y ", KXϕ as "dataset X informs the knowledge of ϕ", and SCX ϕ as "dataset X informs a strategy of coalition C to achieve ϕ". By KXϕ we mean formula ¬KX¬ϕ. We also assume that constant true ⊤, conjunction ∧, and biconditional ↔ are defined in the standard way. In this article, we omit curly brackets and parenthesis when it does not create confusion. For example, we write x instead of {x}, x1, . . . , xn instead of {x1, . . . , xn}, and ϕ → ψ instead of (ϕ → ψ).

For any states w,w′ ∈ W and any dataset X ⊆ V , let w ∼X w′ mean that w ∼x w′ for each data variable x ∈ X. In particular, w ∼∅ w′ is true for any states w,w′ ∈ W. Also, we write f =B g if f(b) = g(b) for each element b of a set B.

Definition 2. For any state w ∈ W of a game (W, {∼x }x∈V ,∆,M, π) and any formula ϕ ∈ Φ, satisfaction relation w ⊩ ϕ is defined recursively as follows

1. w ⊩ p, if w ∈ π(p),
2. w ⊩ X ▷ Y , when for each w′ ∈ W if w ∼X w′ , then w ∼Y w′ ,
3. w ⊩ ¬ϕ, if w ⊮ ϕ,
4. w ⊩ ϕ→ψ, if w ⊮ ϕ or w ⊩ ψ,
5. w ⊩ KXϕ, if w′ ⊩ ϕ for each w′ ∈ W such that w ∼X w′ ,
6. w ⊩ SCX ϕ, when there is an action profile s ∈ ∆C of coalition C such that for all states w′ , v ∈ W and each complete action profile δ ∈ ∆A if w ∼X w′ , s =C δ, and (w′ , δ, v) ∈ M, then v ⊩ ϕ.

Observe that K∅ϕ is the universal modality that says "statement ϕ is true in each state of the game". If K∅ϕ is true in each state, then everyone must know it. For this reason, we read K∅ϕ as "statement ϕ is public knowledge".

The sentence "dataset X informs dataset Y " could be interpreted in two ways: locally and globally. Under the first interpretation, the values of variables X in the current state determine the values of variables Y . Under the second interpretation, the values of X determine the values of Y in each state. For example, suppose that real values of variables x and y are such that y = x2 in each state of the game. Then, the value of x globally determines the value of y, but the value of y does not globally determine the value of x. However, the value of y determines the value of x locally in each state where y = 0. Item 2 of Definition 2, defines the semantics of expression X▷Y as local dependency. The global dependency can be captured by the expression K∅(X ▷ Y ).

The data-informed strategies also can be local and global. For example, supposed that based on the test results X a doctor knows how to adjust a medication. This is a global datainformed strategy because the doctor would know how to adjust medication no matter what the results X are. Of course, for different test results the strategy (adjustment amount) would be different. We can specify such global data-informed strategies as functions that map each X-equivalent class of states into an action. A local strategy might exists only for the values of X in the current state. For example, a doctor might have a strategy to save the life of a cancer patient for the current values of the test results X. For some other value of X she might no longer have such a strategy. A local datainformed strategy is a single action that guarantees result only in the X-equivalence class of the current state. Item 6 of Definition 2 defines modality SCX ϕ as a claim of existence of a local data-informed strategy. The modality for global strategy could be defined as K∅SCX ϕ.

4 Axioms

In addition to propositional tautologies in language Φ, our logical system contains the following axioms.

1. Truth: KXϕ→ϕ,
2. Negative Introspection: ¬KXϕ→KX¬KXϕ,
3. Distributivity: KX(ϕ→ψ) → (KXϕ→KXψ),
4. Reflexivity: X ▷ Y , where Y ⊆ X,
5. Transitivity: X ▷Y → (Y ▷Z →X ▷Z),
6. Augmentation: X ▷Y → (X ∪Z) ▷ (Y ∪Z),
7. Introspection of Dependency: X ▷Y →KX(X ▷Y ),
8. Knowledge Monotonicity: X ▷Y → (KY ϕ→KXϕ),
9. Cooperation: SCX (ϕ→ψ) → (SDX ϕ→ SC∪D X ψ), where C ∩ D = ∅,
10. Strategic Monotonicity: X ▷Y → (SCY ϕ→ SCX ϕ),
11. Strategic Introspection: SCX ϕ→KXSCX ϕ,
12. Knowledge of Unavoidability: KXS∅Y ϕ → S∅X ϕ,
13. Public Knowledge: K∅ϕ→ SCX ϕ.

The Truth, the Negative Introspection, and the Distributivity axioms are the standard principles from epistemic logic S5. The Reflexivity, the Transitivity, and the Augmentation are well-known Armstrong's axioms for functional dependency [Armstrong, 1974].

The Introspection of Dependency axiom states that if a dataset X informs a dataset Y , then this is known to anyone with access to X. The Knowledge Monotonicity axioms states that if a dataset X informs a dataset Y and dataset Y informs the knowledge of ϕ, then dataset X also informs the knowledge of ϕ. The Cooperation axiom is a variation of Marc Pauly's axiom introduced in the logic of coalition power [Pauly, 2001; Pauly, 2002]. It states that if a dataset X informs strategies (actions profiles) of disjoint coalitions C and D to achieve ϕ → ψ and ϕ, respectively, then the dataset also informs a joint strategy for these coalitions to achieve ψ. The Strategic Monotonicity axiom states that if a dataset X informs a dataset Y , then X informs each strategy informed by Y . The Strategic Introspection axiom states that if a dataset X informs a strategy, then X also informs the knowledge that it informs the strategy.

To understand the meaning of the Knowledge of Unavoidability axiom, note that statement KXSCY ϕ means that "anyone who knows X knows that anyone who knows Y knows a strategy of coalition C to achieve ϕ". Let us refer to the knowers of X and Y as Xena and Yeily. Note that while Yeily knows the strategy, Xena only knows that the strategy exists and is known to Yeily. Generally speaking, Xena does not knowwhat the strategy is. One important exception, however, is when coalition C is empty. In this case, coalition C has only a single strategy (the unique function from the set ∆C ). In such a situation, knowing that a strategy exists is equivalent to knowing what the strategy is. This is captured by the Knowledge of Unavoidability axiom. The name of the axiom comes from the fact that S∅Y ϕ can also be interpreted as "anyone who knows Y , knows that ϕ is unavoidable".

By item 3 of Definition 1, each game has at least one action. Such an action can be used by the members of any coalition to achieve any statement which is true in each state of the game. This is captured by the Public Knowledge axiom.

We write ⊢ ϕ and say that formula ϕ ∈ Φ is a theorem of our system if it is derivable from the above axioms using the Modus Ponens and the Necessitation inference rule:

In addition to unary relation ⊢ ϕ, we also consider a binary relation F ⊢ ϕ. We write F ⊢ ϕ if formula ϕ ∈ Φ is provable from the set of formulae F ⊆ Φ and the theorems of our logical system using only the Modus Ponens inference rule. We say that set F is inconsistent if there is a formula ϕ ∈ F such that F ⊢ ϕ and F ⊢ ¬ϕ.

5 Main Results

Theorem 1 (Strong Soundness). For each state w of an arbitrary game, each set of formulae F ⊆ Φ and each formula ϕ ∈ Φ, if w ⊩ f for each formula f ∈ F and F ⊢ ϕ, then w ⊩ ϕ.

Theorem 2 (Strong Completeness). For any set of formulae F ⊆ Φ and any formula ϕ ∈ Φ, if the set V of data variables is finite and F ⊬ ϕ, then there is a state w of a game such that w ⊩ f for each formula f ∈ F and w ⊮ ϕ.

Theorem3. If the set V of data variables is infinite, then any strongly sound logical system L is not strongly complete.

Theorem 4. If ϕ ∈ Φ is a data-finite formula such that ⊬ ϕ, then there is a state w of a game such that w ⊮ ϕ.

Acknowledgments

Junli Jiang acknowledges the support of the "Innovation Research 2035 Pilot Plan of Southwest University" (NO. SWUPilotPlan018).