Knowing How to Plan

Standard Epistemic Logic (EL) mainly studies reasoning patterns of knowing that $\varphi$, despite early contributions by Hintikka on formulating other know-wh expressions such as knowing who and why using first-order and higher-order modal logic. In recent years, there is a resurgence of interest on epistemic logics of know-wh powered by the new techniques for fragments of first-order modal logic based on the so-called bundle modalities packing a quantifier and a normal epistemic modality together [27, 25, 22]. Within the varieties of logics of know-wh, the logics of know-how received the most attention in AI (cf. e.g., [26, 9, 21, 17]).

Besides the inspirations from philosophy and linguistics (e.g., [24]), the idea of automated planning in AI also plays an important role in the developments of various logics of know-how. The core idea is (roughly) to interpret knowing how to achieve $\varphi$ as a de re statement of knowledge: “there is a plan such that you know that this plan will ensure $\varphi$”. Here, depending on the exact notion of plans and how much we want to “ensure” that the plan works, there can be different semantics based on ideas from conformant planning and contingent planning in AI. However, as shown by Li and Wang [17], there is a logic core which is independent from the exact notions of plans underlying all these notions of know-how. We can actually unify different planning-based approaches in a powerful framework.

In this paper, we show that the connection between planning and know-how is not merely one way in terms of planning-based know-how, it also makes perfect sense to do know-how-based planning which generalizes the notion of planning to incorporate know-how based goals to be explained in the next subsection. As observed in [17], the typical epistemic planning problem given explicit models can be viewed as model checking problems in our framework with the know-how modality $\mathsf{Kh}$ in the language. For example, $\mathsf{Kh}_{\_}1(\mathsf{K}_{\_}2\varphi\land\neg\mathsf{K}_{\_}3\mathsf{K}_{\_}2\varphi)$ captures the epistemic planning problem for agent 1 to ensure that agent 2 knows that $\varphi$ and keep it a secret from agent 3. Such epistemic planning can also be done in other epistemic approaches, for example, by using dynamic epistemic logic (cf. e.g., [4, 6, 5, 8]). However, we can do much more with the $\mathsf{Kh}$ modality in hand, as explained below.

To specify the knowledge-based plans, we need the following formal language EAL to express the knowledge conditions.

The auxiliary connectives and modalities $\to,\lor,\langle a\rangle$ are defined as abbreviations as usual.

The semantics of EAL formulas is defined on finite models with both epistemic relations and transitions labelled by atomic actions, which will also be used for the know-how logic. In contrast with the single-agent model of [17], for each agent $i$ we have a special set of actions $\mathbf{A}_{\_}i$ that are executable by $i$. Note that an action may be executable by multiple agents. Moreover, we implicitly assume each agent is aware of all the actions, even for those not executable by itself.

Inspired by [14], we only consider knowledge-based plans for each agent. We introduce the following specification language which is a multi-agent variant of a fragment of the programming language introduced in [17].

Note that the atomic action $a$ in the above definition must belong to $i$, but the condition $\mathsf{K}_{\_}i\varphi$ can contain epistemic modalities and actions of other agents, e.g., $\mathsf{K}_{\_}i\neg\mathsf{K}_{\_}j[b]p$ is a legitimate condition for a knowledge-based plan for $i$ even when $b\not\in\mathbf{A}_{\_}i$.

We will abbreviate $\mathtt{if}{\leavevmode\nobreak\ \mathsf{K}_{\_}i\varphi\leavevmode\nobreak\ }\mathtt{then}{\leavevmode\nobreak\ \pi_{\_}1\leavevmode\nobreak\ }\mathtt{else}{\leavevmode\nobreak\ \pi_{\_}2}$ as $\mathsf{K}_{\_}i\varphi?\pi_{\_}1\!:\pi_{\_}2$. We use $\pi^{n}$ to denote the program $\underbrace{\pi;\cdots;\pi}_{\_}{n}$, and $\pi^{0}$ is the empty program $\epsilon$.

Let $\mathcal{M}$ be an epistemic transition system, $s$ be a state in $\mathcal{M}$, and $\pi$ be a program in $\mathtt{KBP}(i)$. The state set $Q(\pi)(s)$, which is the set of states on which executing $\pi$ on $s$ will terminate, is defined by induction on $\pi$ as follows:

We use $Q(\pi)([s]^{i})$ to denote the set $\bigcup_{\_}{s^{\prime}\in[s]^{i}}Q(\pi)(s^{\prime})$. Given the property of perfect recall, the resulting states of a knowledge-based plan have a nice property.

Next we will define a notion of strong executability which is a generalized version of the one in [26].

To define the model checking algorithm later, we need to construct the tree of possible executions of a plan where each node is essentially an epistemic equivalence class (usually called a belief state in automated planning).

We use $r^{\mathcal{T}}$ (or simply $r$) to refer to the root node of the execution tree $\mathcal{T}$. The following two propositions show the relations between execution trees and knowledge-based plans.

Extending the work of [17], we introduce the multi-agent epistemic language of know-how and its semantics and study the model checking complexity in detail.

The readers can go back to Example 1 to verify the truth of the formula mentioned there.

We can show that ELKh is invariant under bisimualtion defined in Definition 5 which also match labelled transitions (cf. [17]).

In the remainder of this section, we will propose a model checking algorithm for ELKh. The key part of the model checking algorithm is to check the $\mathsf{Kh}_{\_}i$-formulas, and the problem of whether $\mathcal{M},s\vDash\mathsf{Kh}_{\_}i\varphi$ depends on whether there is a good plan for $\mathsf{Kh}_{\_}i\varphi$. Our strategy is to reduce the problem of whether there is a good plan for $\mathsf{Kh}_{\_}i\varphi$ to the nondeterministic planning problem in [7], which we will briefly introduce below.

Given a labeled transition system $T$ (note that there is no epistemic relation), we often write $(s,t)\in\xrightarrow{a}$ as $s\xrightarrow{a}t$. The sequence $s_{\_}0\xrightarrow{a_{\_}1}s_{\_}1\xrightarrow{a_{\_}2}\cdots s_{\_}n$ is called an execution trace of $T$ from $s_{\_}0$. A partial function $f:D\to\mathbf{A}$ is called a policy. An execution trace $s_{\_}0\xrightarrow{a_{\_}1}s_{\_}1\xrightarrow{a_{\_}2}\cdots s_{\_}n$ is induced by $f$ if $f(s_{\_}k)=a_{\_}{k+1}$ for all $0\leq k<n$. It is complete w.r.t. $f$ if $s_{\_}n$ is not in the domain of $f$.

Now we define the nondeterministic planning problem that corresponds to $\mathcal{M},s\vDash\mathsf{Kh}_{\_}i\varphi$. Since the language of ELKh is a multi-agent one where different agents have different abilities, the corresponding nondeterministic planning problem must take the agent $i$ into account. This makes the reduction more complex than that of single-agent know-how logics.

Given a model $\mathcal{M}=\langle W,\{\sim_{\_}i\mid i\in\mathbf{I}\},\{\mathbf{A}_{\_}i\mid i\in\mathbf{I}\},\{Q{(a)}\mid a\in\mathbf{A}\},V\rangle$ and an agent $i$, a planning problem for $i$ is $P(\mathcal{M},i)=\langle T(\mathcal{M},i),[w]^{i},G\rangle$ where $[w]^{i}$ is an $i$-belief-state, $G$ is a set of $i$-belief-states, and $T(\mathcal{M},i)=\langle D,\mathbf{A}_{\_}i,\{\xrightarrow{a}\mid a\in\mathbf{A}_{\_}i\}\rangle$ is a labeled transition system where $D=[W]^{i}$ and for each $a\in\mathbf{A}_{\_}i$, $[s]^{i}\xrightarrow{a}[t]^{i}\iff a$ is strongly executable on $[s]^{i}$, and there exists $t^{\prime}\in[t]^{i}:t^{\prime}\in Q(a)([s]^{i})\}$.

We will show that the problem of whether $\mathcal{M},s\vDash\mathsf{Kh}_{\_}i\varphi$ indeed can be reduced to a nondeterministic planning problem for $i$ (Lemma 4.24). Before that, we need two auxiliary propositions.

Finally, we are ready to show the upper bound of model checking ELKh.

In this section, we axiomatize our logic of know-how over finite models with perfect recall. Note that we cannot apply the generic completeness result in [17] since our setting is not only multi-agent but also with an extra condition of perfect recall. It turns out the axiomatization is the multi-agent variant of the system in [9] which has an extra axiom $\mathtt{AxKhtoKhK}$ than the proof system in [17]. Note that although the proof system is similar, the semantics of the $\mathsf{Kh}$ in [9] is based on model-dependent functions from equivalence classes to actions instead of the syntactically specified plan in our work.

The proof system $\mathbb{SLKHC}$ is presented in Table 1.

The property of perfect recall is sufficient to guarantee the validity of $\mathtt{AxKhtoKhK}$, but the axiom cannot characterize the property, as it is shown in [17]. Moreover, the composition axiom $\mathtt{AxKhKh}$ in $\mathbb{SLKHC}$ is a weaker version of the axiom $\mathsf{Kh}(\varphi\lor\mathsf{Kh}\psi)\to\mathsf{Kh}(\varphi\lor\psi)$ in [17].

Due to the axiom $\mathtt{AxKhtoKKh}$, the stronger composition axiom in [17] can be derived in $\mathbb{SLKHC}$ based on $\mathtt{AxKhKh}$.

Next, we will show that the proof system $\mathbb{SLKHC}$ is sound and complete over finite models with perfect recall. By Propositions 13 and 14, it follows that there is a correspondence between execution trees and plans. With this correspondence result, we can significantly simplify the proofs of the soundness and completeness of the proof system $\mathbb{SLKHC}$ than [9] and [17]. More specifically, the validity of Axiom $\mathtt{AxKhKh}$, which was highly non-trivial in [9], follows from the fact that two subsequent execution trees can be combined into one execution tree. (The detailed proof can be found in the following theorem of soundness.) For the completeness, the corresponding execution tree plays an important role in the proof of the truth lemma (Lemma 5.40).