Knowing-How under Uncertainty (Extended Abstract)

1 Introduction

In this article we study an interplay between knowledge, strategies, and uncertainty in multiagent systems. Consider an example of a traffic situation depicted in Figure 1, where a self-driving truck t is approaching an intersection at the same time as a regular car c. Although there is a stop sign instructing the car to yield to the truck, the car's driver does not notice the sign and does not slow down. This is detected by the radar on the self-driving truck t. The truck has two strategies that potentially can prevent a collision with the car: to accelerate or to break. How effective each of these strategies is depends on the speed of the car c. If the speed of the car is slow, the truck must accelerate to avoid being hit by the car in the rear half. If the speed is high, the truck must brake to avoid being hit in the front half. Suppose that the truck will avoid the collision by accelerating if the speed of car c is at most 58 miles per hour (mph) and that the truck will avoid the collision by breaking if the speed of the car is at least 56mph (see Figure 2). In the interval between 56 and 58mph, both strategies would allow the truck to avoid a collision.

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

†Contact Author

Let us further assume that the actual speed of the car is 55mph, but the truck's radar can only detect the speed of the car with a precision of ±6mph. Thus, the truck only knows that the speed of the car is somewhere in the interval between 49 and 61mph, see Figure 2. Thus, truck t does not know which of the two strategies would allow it to prevent a collision. Note that in this situation truck t has a strategy to avoid collision, but it does not know what this strategy is. If an agent t has a strategy to achieve goal ϕ, she knows that she has such a strategy, and she knows what this strategy is, then we say that she has a know-how strategy and denote this by Htϕ. In this article we study the existence of know-how strategies to achieve a goal depending on the degree of uncertainty of the information available to the agent. We represent the degree of uncertainty by the superscript of the modality. For example, we write ¬H6t ("Collision is avoided.") to say that truck t does not have a know-how strategy to avoid a collision if it determines the speed of car c with a precision of ±6mph. However, if the truck is able to determine the speed of the car with a precision of ±2mph, then truck t has a know-how strategy to prevent the collision: H2t ("Collision is avoided.").

Now suppose that an autonomous car a is driving right behind car c. From this position car a can measure the speed of car c with precision ±2mph. Thus, car a knows that the speed of car c is between 53 and 57mph. Assuming that car a is aware of truck's radar precision, it can see that no matter where within the interval between 53 and 57mph the speed of car c is, truck t does not have a know-how strategy to avoid collision. We write this as K2a¬H6t ("Collision is avoided."), where modality K2a denotes the knowledge of car a when it is able to determine the speed of car c with a precision of ±2mph.

As another example, even though the statement H2t ("Collision is avoided.") is true, car a does not know about this: ¬K2aH2t ("Collision is avoided."). Indeed, due to the precision of car a's equipment, as far as car a is concerned, the speed of the car c is between 53 and 57mph. If it is 56.5mph, then statement H2t ("Collision is avoided.") would not be true. A similar setting appears in many real world examples [Ferguson and Stentz, 2004; Brafman et al., 1997].

The interplay between knowledge modality Ka and knowhow modality Ha, both without a degree of uncertainty, has been recently studied, see Section 2. In this article we study the interplay between modalities Kca and Hca , where the degree of uncertainty c refers to the precision with which an agent a can position herself in an arbitrary metric space. Several "distance logics" for reasoning about modality "statement ϕ is true at distance at most c" were introduced in [Kutz et al., 2002] without emphasizing their epistemic interpretation. We proposed the epistemic interpretation and a sound and complete system for modality Kca in multiagent setting [Naumov and Tao, 2015]. The current article extends our previous work to include modality Hca .

Although the axiomatic system obtained in this article is a straightforward combination of existing principles, proving completeness theorems for this system required us to develop a new technique of constructing a canonical model as a tree where each child node has a twin sibling.

2 Literature Review

Non-epistemic logics of coalition power were developed by Pauly [2002], who also proved the completeness of the basic logic of coalition power. Alur, Henzinger, and Kupferman introduced Alternating-Time Temporal Logic (ATL) that combines temporal and coalition modalities [2002].

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 the modality "know they can do". Wang [2018] captured the "knowing how" as a binary modality in a complete logical system with a single agent. We previously called such strategies "executable" [Naumov and Tao, 2017a].

Several modal logical systems that capture the interplay between knowledge and know-how strategies without uncertainty have been proposed. ˚Agotnes and Alechina [2019] introduced a complete axiomatization of an interplay between single-agent knowledge and coalition know-how modalities to achieve a goal in one step. Amodal logic that combines the distributed knowledge modality with the coalition know-how modality to maintain a goal was axiomatized by us in [Naumov and Tao, 2017a]. A sound and complete logical system in a single-agent setting for know-how strategies to achieve a goal in multiple steps rather than to maintain a goal is developed by Fervari, Herzig, Li, and Wang [2017]. In [Naumov and Tao, 2017b; 2018c], we developed a trimodal logical system that describes an interplay between the (not know-how) coalition strategic modality, the coalition know-how modality, and the distributed knowledge modality. In [Naumov and Tao, 2018b], we proposed a logical system that combines the coalition know-how modality with the distributed knowledge modality in the perfect recall setting. In [Naumov and Tao, 2018a], we introduced a logical system for the second-order know-how. Wang [2015; 2018] proposed a complete axiomatization of "knowing how" as a binary modality, but his logical system does not include the knowledge modality.

Several versions of "distance logic" were axiomatized by Kutz, Sturm, Suzuki, Wolter, and Zakharyaschev [2002]. Their logical systems have modalities A≤cϕ and A>cϕ that stand for "statement ϕ is true at each point no further than c" and "statement ϕ is true everywhere at a distance more than c". Sheremet, Wolter, and Zakharyaschev [2010], introduced two new logical systems. One of them, qualitative metric logic, contains modalities ∃≤cϕ (formula ϕ is true at some point no further than c) and ∃<cϕ (formula ϕ is true at some point closer than c) as well as quantifiers over distances. The other system, called comparative similarity logic, is a syntactical fragment of qualitative metric logic that includes modal operators for comparing distances. They gave sound and complete axiomatisations of the second logic in several different settings.

Distance logic discussed above does not include strategic modalities. In this article we combine knowledge under uncertainty modality Kca and strategic know-how modality Hca , and prove the strong completeness of the obtained system with respect to one class of semantics and the weak completeness with respect to another.

3 Syntax and Semantics

This section introduces the formal syntax and semantics of our logical system. Throughout the article we assume a fixed nonempty set of propositional variables and a fixed (possibly infinite) set of agents A.

Definition 1 Let Φ be the minimal set of formulae such that

1. p ∈ Φ for each propositional variable p,
2. ¬ϕ, ϕ→ψ ∈ Φ for all formulae ϕ, ψ ∈ Φ,
3. Kcaϕ, Hcaϕ ∈ Φ for each real number c ≥ 0, each agent a ∈ A, and each formula ϕ ∈ Φ.

We define Boolean constants ⊤ and ⊥ in the usual way.

In the introductory example we assumed that the uncertainty parameter c of the modalities Kcaϕ and Hcaϕ specifies the precision with which agents know the car's position. In [Naumov and Tao, 2015] we provided an example where an uncertainty parameter specifies the precision of a police speed radar and another example where an uncertainty parameter specifies the amount of noise in a communication channel. In the latter case, parameter c is the maximum Hamming distance between messages. Following [Naumov and Tao, 2015], we assume that parameter c represents the precision with which the agent can determine the position (state) of the whole system in an arbitrary metric space.

In mathematics, a metric space is the most general form of the concept of distance [Rudin, 1976]. Examples of commonly used metric spaces are Euclidean distance in Rn , Hamming distance on strings of a fixed length, the shortest path distance on graphs, and the Manhattan distance [Krause, 2012] on Zn . In addition to these, there are Levenshtein distance [Levenshtein, 1966], Damerau-Levenshtein distance [Damerau, 1964], Jaro-Winkler distance [Jaro, 1989; Winkler, 1990], and many others [Deza and Deza, 2006].

It is usually assumed that a distance is a non-negative real number. However, sometimes it is convenient to assume that a distance could be infinite [Burago et al., 2001], which is the approach we take in this article. In other words, we assume that the value of a distance is an extended non-negative real number, i.e., a non-negative real number or the positive infinity ∞. As usual in calculus, we assume that ∞ is greater than any real number and that the sum of ∞ and any extended non-negative real number is equal to ∞. Note, however, that per Definition 1, the formulae of our logical system can only use real numbers, not extended real numbers.

Definition 2 A metric space is a pair (W, δ) such that W is a set and δ is a distance function that maps every pair of elements of W to an extended non-negative real number, where the following properties hold for all u, v, w ∈ W:

1. Identity of Indiscernibles: δ(u, v) = 0 iff u = v,
2. Symmetry: δ(u, v) = δ(v, u),
3. Triangle Inequality: δ(u, v) ≤ δ(u,w) + δ(w, v).

Definition 3 A metric space (W, δ) is finite if all values of distance function δ are real numbers.

The next definition specifies the class of models for our logical system. By XY we denote the set of all functions from set Y to set X.

Definition 4 An epistemic transition system is a tuple

(W, {δa}a∈A, D, M, π), where

1. W is a set of "epistemic states",
2. (W, δa) is a metric space for each agent a ∈ A,
3. D is a nonempty set called "domain of actions",
4. M ⊆ W × DA × W is a "transition mechanism",
5. π maps propositional variables to subsets of W.

Informally, a model of our logical system consists of a set of states with agent-specific metrics. It resembles an S5 Kripke model except that, instead of having an indistinguishability relation specific to each agent, the model has a metric specific to an agent. If distance δa(u, v) is equal to infinity, then agent a can always distinguish epistemic states u and v. The assumption that agents have agent-specific metrics is natural in the setting when the agents can measure different sets of parameters of the system.

In each state, agents take actions. The set of all actions taken, called an action profile, is viewed as a function from the set of all agents A to a "domain of actions" D. In other words, an action profile is an element of set DA. Although this was not emphasized in our introductory example, we assume that once the actions are taken, the system transitions from one state to another. Thus, we call the model an epistemic transition system. The rules that determine the next state based on the current state and the action profile are captured by a transition mechanismM. Note that these rules are, generally speaking, non-deterministic. Furthermore we assume that in some situations there might be no "next" state(s). We interpret this as a termination of the transition system.

Definition 5 An epistemic transition system (W, {δa}a∈A, D,M, π) is with finite metrics if (W, δa) is a finite metric space for each agent a ∈ A.

In this article we prove that our logical system is strongly complete with respect to all epistemic transition systems (Theorem 1) and weakly complete with respect to all epistemic transition systems with finite metrics (Theorem 2). We also show that our logical system, as well as any other strongly sound logical system, is not strongly complete with respect to epistemic transition systems with finite metrics (Theorem 3).

The next definition is the key definition of this section. It formally specifies the meaning of modalities Kca and Hca . The part pertaining to modality Kca is identical to the corresponding definition in [Naumov and Tao, 2015].

Definition 6 For any epistemic state w ∈ W of an epistemic transition system (W, {δa}a∈A,D,M, π) and any formula ϕ ∈ Φ, let the satisfiability relation w ⊩ ϕ be defined recursively 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 ⊩ Kcaϕ if w′ ⊩ ϕ for each epistemic state w′ ∈ W such that δa(w, w′ ) ≤ c,
5. w ⊩ Hcaϕ if there is an action α ∈ D such that w′′ ⊩ ϕ for all epistemic states w′ ,w′′ ∈ W and each action profile s ∈ DA where δa(w,w′ ) ≤ c, s(a) = α, and (w′ , s, w′′ ) ∈ M, see Figure 3.

In other words, w ⊩ Kcaϕ if formula ϕ is satisfied at each point (state) in a ball of radius c around point w defined by the metric δa. Also, w ⊩ Hcaϕ if there is an action of agent a that achieves goal ϕ from any point in the ball described above. In the case when c = 0, formulae w ⊩ Kcaϕ and w ⊩ Hcaϕ have special meanings. The first of them states that ϕ is true just at point w. Thus, formula K0aϕ and formula ϕ are logically equivalent. This fact is captured through the combination of the Zero Confidence and the Truth axioms of our logical system that we introduce in the next section. Similarly, formula H0aϕ states that a strategy to achieve ϕ exists at point w.

Epistemic transition systems are similar to the semantics of Coalition Logic [Pauly, 2001; 2002] and concurrent game structures, the semantics of ATL [Alur et al., 2002], with three notable differences. First, in those semantics, the domain of choices depends on a state and an agent. On the other hand, we assume a uniform domain of choices for all states and all agents. This difference is insignificant because multiple domains of choices could be replaced with their union if the aggregation mechanism is modified to interpret the additional choices as alternative names for the original choices. Second, unlike the transition function in these semantics, our aggregation mechanism allows to capture nondeterministic transitions. This difference is significant because restricting semantics to only deterministic transitions would require additional axioms. For example, property H0aϕ ∨ H0a¬ϕ is universally true in single-agent deterministic transition systems, but is not universally true in single-agent nondeterministic systems. Third, we do not require that, for any current state and any action profile, there is at least one next state. Thus, in our setting, the system may terminate. Hence, for example, formula Hca⊥ might be satisfied in some states of our epistemic transition systems.

4 Axioms

In addition to propositional tautologies in language Φ, our logical system has the following five axioms:

1. Zero Confidence: ϕ→K0aϕ,
2. Truth: Kcaϕ→ϕ,
3. Negative Introspection: ¬Kcaϕ→Kda¬Kc+d a ϕ,
4. Distributivity: Kca (ϕ→ψ) → (Kcaϕ→Kcaψ),
5. Strategic Positive Introspection: Hc+d a ϕ→KcaHdaϕ.

The first four of these axioms come from [Naumov and Tao, 2015]. The Strategic Positive Introspection axiom without a degree of uncertainty first appeared in [ ˚Agotnes and Alechina, 2019] and is also present in [Wang, 2018; Fervari et al., 2017; Naumov and Tao, 2017b; 2017a; 2018b; 2018a; 2018c]. Blending the know-how and the degree of uncertainty lines of research into one logical system that captures non-trivial interplay between the two notions is the main contribution of this article.

We write ⊢ ϕ if formula ϕ ∈ Φ is provable from the above axioms using the Monotonicity, K-Necessitation, H- Necessitation, and Modus Ponens inference rules:

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

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

5 Main Results

Theorem 1 shows the strong completeness of our logical system with respect to the class of arbitrary epistemic transition systems. Theorem 2 establishes the weak completeness with respect to the class of epistemic transition systems with finite metrics. Theorem 3 shows that not only the strong completeness for the systems with finite metrics does not hold for our logical system, but there is no strongly sound logical system for which it does. The proofs of these theorems, as well as the proof of soundness of our system, can be found in the complete version of this article [Naumov and Tao, 2019].

Theorem 1 (strong completeness) If X ⊬ ϕ, then there is an epistemic state w of an epistemic transition system such that w ⊩ χ for each formula χ ∈ X and w ⊮ ϕ. ⊠

Theorem 2 (completeness for finite metrics) If w ⊩ ϕ for every epistemic state of every epistemic transition system with finite metrics, then ⊢ ϕ. ⊠

Theorem 3 (incompleteness) For any strongly sound logical system L with respect to epistemic transition systems, there is a set of formulae X ⊆ Φ and a single formula ϕ ∈ Φ such that

1. for each epistemic state w of each epistemic transition system with finite metrics, if w ⊩ χ for each formula χ ∈ X, then w ⊩ ϕ,

6 Conclusion

The contributions of this article are as follows. First, we introduced the notion of a know-how strategy under uncertainty as a strategy that can be used not only at a given state, but at any state within a given distance from the given state. Second, we proposed a sound logical system that describes the interplay between the know-how under uncertainty and the knowledge modalities. We proved the strong completeness of this system with respect to arbitrary transition systems and the weak completeness with respect to transitions systems with finite metrics. We also showed that the strong completeness with respect to the systems with finite metrics does not hold.