Reasoning about Normative Update

1 Introduction

Recently a number of authors have independently started developing new and very expressive frameworks for automated planning based on dynamic epistemic logic [Bolan¨owe et al., 2011; Aucher, 2012;

Pardo and Sadrzadeh, 2012]. Dynamic epistemic logic (DEL) extends ordinary modal epistemic logic [Hintikka, 1962] by the inclusion of event models to describe actions, and a product update operator that defines how epistemic models are updated as the consequence of executing actions described through event models [Baltag et al., 1998]. Using epistemic models as states, event models as actions, and the product operator as state transition function, one immediately gets a planning formalism based on DEL.

One of the main advantages of this formalism is expressiveness. Letting states of planning tasks be epistemic models implies that we have something that generalizes belief states, the classical approach to planning with nondeterminism and partial observability [Ghallab et al., 2004]. 1 Compared to

1 A belief state can be modeled as a set of propositional valuations, which again can be modeled as a connected S5 model of epistemic logic.

Thomas Bolander

DTU Compute Technical University of Denmark Copenhagen, Denmark

tobo@dtu.dk

standard planning formalisms using belief states, the DELbased approach has the advantage that actions (event models) encode both nondeterminism and partial observability [Andersen et al., 2012], and hence that observability can be action dependent, and we don't need observation functions on top of action descriptions. Active sensing actions are also expressible in the DEL-based framework. Another advantage of the DEL-based framework is that it generalizes immediately to the multi-agent case. Both epistemic logic and DEL are by default multi-agent formalisms, and the single-agent situation is simply a special case. Hence the formalism provides a planning framework for multi-agent planning integrating nondeterminism and partial observability. It can be used both for adversarial and cooperative multi-agent planning. Finally, the underlying epistemic logic also allows agents to represent their beliefs about the beliefs of other agents, hence allowing them to do Theory of Mind modeling. Theory of Mind (ToM) is a concept from cognitive psychology referring to the ability of attributing mental states (beliefs, intentions, etc.) to other agents [Premack and Woodruff, 1978]. Having a ToM is essential for successful social interaction in human agents [Baron-Cohen, 1997], hence can be expected to play an equally important role in the construction of socially intelligent artificial agents.

The flip side of the expressivity advantages of the DELbased planning framework is that the plan existence problem is undecidable in the unrestricted framework. This was proven in [Bolander and Andersen, 2011] by an encoding of Turing machines as 3-agent planning tasks (leading to a reduction of the Turing machine halting problem to the 3-agent plan existence problem). The proof made essential use of actions with postconditions, that is, ontic actions that make factual changes to the world (e.g. writing a symbol to a tape cell of a Turing machine). One could speculate that undecidability relied essentially on the inclusion of ontic actions, but in the present paper we prove this not to be the case. We prove that plan existence is undecidable even when only allowing purely epistemic (non-ontic) actions, and already for 2 agents. This is by an encoding of two-counter machines as planning tasks. We also prove that even single-agent planning is undecidable on S4 frames.

Given that we deal with multi-agent situations, it is important to specify our modeling approach, and in particular whether the modeler/planner is one of the agents. A classification of the different modeling approaches and their respective formalisms can be found in [Aucher, 2010]. For ease of presentation, we follow in this article the perfect external approach of (dynamic) epistemic logic and model the situation from an external and omniscient point of view. This said, all our results in this article transfer to the other modeling approaches if we replace epistemic models with internal models or imperfect external (i.e. multi-pointed) models, which, as we said, generalize to a multi-agent setting the belief states of classical planning [Bolander and Andersen, 2011] .

The article is structured as follows. In Section 2, we recall the core of the DEL framework. In Section 3, we relate our DEL-based approach to the classical planning approach and provide an example of an epistemic multi-agent planning task. In Section 4, we introduce two-counter machines which are used in Sections 5 and 6 to prove our undecidability results. In Section 7, we derive from our results the undecidability of the DEL model checking problem (for the language with the star operator on actions). Finally, we discuss related work and end with some concluding remarks in Section 8. An extended version of this article with more detailed proofs can be found in [Aucher and Bolander, 2013].

2 Dynamic Epistemic Logic

In this section, we present the basic notions from DEL required for the rest of the article (see [Baltag et al., 1998; van Ditmarsch et al., 2007; van Benthem, 2011] for more details). Following the DEL methodology, we split our exposition into three subsections. In Section 2.1, we recall the syntax and semantics of the epistemic language. In Section 2.2, we define event models, and in Section 2.3, we define the product update. Finally, in Section 2.4, we define specific classes of epistemic and event models that will be studied in the sequel.

2.1 Epistemic Models

Throughout this article, P is a countable set of atomic propositions (propositional symbols) of cardinality at least two, and A is a non-empty finite set of agents. We will use symbols p, q, r, . . . for atomic propositions and numbers 0, 1, . . . for agents. The epistemic language L(P,A) is generated by the following BNF:

where p ∈ P and i ∈ A. As usual, the intended interpretation of a formula ✷iφ is "agent i believes φ" or "agent i knows φ". The formulas ✸iφ, φ ∨ ψ and φ → ψ are abbreviations of ¬✷i¬φ, ¬(¬φ ∧ ¬ψ), and ¬φ ∨ ψ respectively. We define ⊤ as an abbreviation for p ∨ ¬p and ⊥ as an abbreviation for p ∧ ¬p for some arbitrarily chosen p ∈ P. The semantics of L(P,A) is defined as usual through Kripke models, here called epistemic models.

Definition 1 (Epistemic models and states). An epistemic model of L(P,A) is a triple M = (W,R, V ), where W, the domain, is a finite set of worlds; R : A → 2W×W assigns an accessibility relation R(i) to each agent i ∈ A; V : P → 2W assigns a set of worlds to each atomic proposition; this is the valuation of that variable. The relation R(i)

is usually abbreviated Ri, and we write v ∈ Ri(w) or wRiv when (w, v) ∈ R(i). For w ∈ W, the pair (M,w) is called an epistemic state of L(P,A).

Definition 2 (Truth conditions). Let an epistemic model M = (W,R, V ) be given. Let i ∈ A, w ∈ W and φ, ψ ∈ L(P, A). Then

Example 1. Consider the following epistemic state of L({p}, {0, 1}).

Each world is marked by its name followed by a list of the propositional symbols being true at the world (which is possibly empty if none holds true). Edges are labelled with the name of the relevant accessibility relations (agents). We have e.g. (M,w1) |= ¬✷ip ∧ ¬✷i¬p for i = 0, 1: neither agent knows the truth-value of p. For epistemic states (M,w) we use the symbol to mark the designated world w.

2.2 Event Models

Dynamic Epistemic Logic (DEL) introduces the concept of event model (or action model) for modeling the changes to epistemic states brought about by the execution of actions [Baltag et al., 1998; Baltag and Moss, 2004]. Intuitively, in Definition 3 below, eQie′ means that while the possible event represented by e is occurring, agent i considers it possible that the event represented by e′ is in fact occurring.

Definition 3 (Event models and epistemic actions). An event model of L(P,A) is a triple E = (E,Q, pre), where E, the domain, is a finite non-empty set of events; Q : A → 2E×E assigns an accessibility relation Q(i) to each agent i ∈ A; pre : E → L(P,A) assigns to each event a precondition. The relation Q(i) is generally abbreviated Qi, and we write v ∈ Qi(w) or wQiv when (w, v) ∈ Q(i). For e ∈ E, (E, e) is called an epistemic action of L(P, A).

The event e in (E, e) is intended to denote the actual event that takes place when the action is executed. Note that we assume that events do not cause factual changes in the world. Hence, we only consider so-called epistemic events and not ontic events with postconditions, as in [van Ditmarsch et al., 2005; van Benthem et al., 2006]. Our assumptions for dealing with epistemic planning will therefore also differ from the assumptions used in [Bolander and Andersen, 2011].

2.3 Product Update

Definition 4 (Applicability). An epistemic action (E, e) is applicable in an epistemic state (M, w) if (M, w) |= pre(e).

The product update yields a new epistemic state (M, w) ⊗ (E, e) representing how the new situation which was previously represented by (M, w) is perceived by the agents after the occurrence of the event represented by (E, e).

Definition 5 (Product update). Given is an epistemic action (E, e) applicable in an epistemic state (M,w), where M = (W,R, V ) and E = (E,Q, pre). The product update of (M,w) with (E, e) is defined as the epistemic state (M, w) ⊗ (E, e) = ((W ′ , R′ , V ′ ), (w, e)), where

Example 2. Continuing Example 1, the following is an example of an applicable epistemic action of L({p}, {0, 1}) in

It corresponds to a private announcement of p to agent 0, that is, agent 0 is told that p holds (event e1), but agent 1 thinks that nothing has happened (event e2). The product update is calculated as follows:

In the updated state, agent 0 knows p (since ✷0p holds at (w1, e1)), but agent 1 didn't learn anything (doesn't know p and believes that 0 doesn't either).

2.4 Classes of Epistemic States and Actions

In this article, we consider epistemic states and actions where the accessibility relations satisfy specific properties, namely transitivity (for all w, v, u, wRiv and vRiu imply wRiu, defined by the axiom 4: ✷iφ → ✷i✷iφ), Euclidicity (for all w, v, u, wRiv and wRiu imply vRiu, defined by the axiom 5: ¬✷iφ → ✷i¬✷iφ) and reflexivity (for all w, wRiw, defined by the axiom T: ✷iφ → φ). Different conditions on the accessibility relations correspond to different assumptions on the notions of knowledge or belief [Fagin et al., 1995; Meyer and van der Hoek, 1995]. In the sequel we will refer to L-epistemic states and actions, where the conditions on these models are given in Figure 1.

3 Classical and Epistemic Planning

In this section, we briefly relate the epistemic planning approach of DEL as propounded in [Bolander and Andersen, 2011; L¨owe et al., 2011] with the classical planning approach [Ghallab et al., 2004]. For more detailed connections, we refer the reader to [Bolander and Andersen, 2011].

3.1 Classical Planning

Following [Ghallab et al., 2004], any classical planning domain can be represented as a restricted state-transition system Σ = (S, A, γ), where S is a finite or recursively enumerable set of states; A is a finite set of actions; γ : S ×A ↪→ S is a partial and computable state-transition function. A classical planning task is then represented as a triple (Σ, s0, Sg), where Σ is a restricted state-transition system; s0 is the initial state, a member of S; Sg is the set of goal states, a subset of S. A solution to a classical planning task (Σ, s0, Sg) is a finite sequence of actions (a plan) a1, a2, . . . , an such that: 1. For all i ≤ n, γ(γ(. . . γ(γ(s0, a1), a2), . . . , ai-1), ai) is defined; 2. γ(γ(. . . γ(γ(s0, a1), a2), . . . , an-1), an) ∈ Sg.

3.2 Epistemic Planning

Definition 6 (Epistemic planning tasks). An epistemic planning task is a triple (s0,A, φg) where s0 is a finite epistemic state, the initial state; A is a finite set of finite epistemic actions; φg is a formula in L(P,A), the goal formula.

Any epistemic planning task (s0,A, φg) canonically induces a classical planning task ((S, A, γ), s0, Sg) given by:

• S = {s0 ⊗ a1 ⊗ · · · ⊗ an | n ≥ 0, ai ∈ A}.
• Sg = {s ∈ S | s |= φg}.
• γ(s, a) = {s ⊗ a if a is applicable in s undefined otherwise.

Hence, epistemic planning tasks are special cases of classical planning tasks. A solution to an epistemic planning task (s0, A, φg) is a solution to the induced classical planning task.

Example 3. Let a1 denote the epistemic action (E1, e1) of Example 2 and let a2 denote the result of replacing 0 by 1 and 1 by 0 everywhere in a1. The epistemic action a2 is a private announcement of p to agent 1. Now consider an epistemic planning task (s0,A, φg), where s0 = (M,w1) is the epistemic state from Example 1, and A ⊇ {a1, a2}. Let the goal be that both 0 and 1 know p, but don't know that each other knows: φg = ✷0p ∧ ✷1p ∧ ¬✷0✷1p ∧ ¬✷1✷0p. It is easy to check that a solution to this epistemic planning task is the action sequence a1, a2, since we have s0 ⊗a1 ⊗a2 |= φg. Hence a solution to the task of both agents knowing p without suspecting that each other does, is to first announce p privately to 0 then privately to 1.

The following definition is adapted from [Erol et al., 1995]. Definition 7 (Plan existence problem). Let n ≥ 1 and L ∈ {K, K4, K45, S4, S5}. PlanEx(L, n) is the following decision problem: "Given an epistemic planning task T = (s0,A, φg) where s0 is an L-epistemic state, A is a set of L-epistemic actions and |A| = n, does T have a solution?"

4 Two-counter Machines

We will prove undecidability of the plan existence problem, PLANEX(L, n), for various classes of epistemic planning tasks. Each proof is by a reduction of the halting problem for two-counter machines to the plan existence problem for the relevant class of planning tasks. So, we first introduce two-counter machines [Minsky, 1967; Hampson and Kurucz, 2012].

p ∧ ¬γ0 ∧ ¬γ1 p ∧ ¬γ0 ∧ γ1

Fig. 5: DEC(p)

Definition 8 (Two-counter machines). A two-counter machine M is a finite sequence of instructions (I0, . . . , IT ), where each instruction It, for t < T , is from the set

and IT = halt. A configuration of M is a triple (k, l,m) ∈ N3 with k being the index of the current instruction, and l,m being the current contents of counters 0 and 1, respectively. The computation function fM : N → N3 of M maps time steps into configurations, and is given by fM(0) = (0, 0, 0) and if fM(n) = (k, l,m) then

We say that M halts if fM(n) = (T, l, m) for some n, l, m ∈ N.

Theorem 1. [Minsky, 1967] The halting problem for twocounter machines is undecidable.

5 Single-agent Epistemic Planning

In this section, we assume that the set A is a singleton.

5.1 The General Case

We encode the halting problem of a two-counter machine M as an epistemic planning task in three steps: 1. We define the epistemic models CHAIN(p, n) for encoding natural numbers, and the epistemic states s(k,l,m) for encoding configurations; 2. We define a finite set of epistemic actions FM for encoding the computation function fM; 3. We encode the halting problem as an epistemic planning task using these models.

1. Encoding of configurations. For each propositional symbol p ∈ P and each n ∈ N, we define an epistemic model CHAIN(p, n) as in Figure 2. For each (k, l,m) ∈ N3 , we define the epistemic state s(k,l,m) as in Figure 3. It encodes the configurations (k, l,m) of two-counter machines.

2. Encoding of the computation function. First, we need some formal preliminaries:

Definition 9 (Path formulas). For every n ∈ N, define γn := ✸n✷⊥.

Lemma 1. Let n ∈ N and let (M, w) be an epistemic state. Then (M,w) |= γn iff there is a path of length n starting in w and ending in a world with no successor (a sink).

For each propositional symbol p ∈ P and each m, n ∈ N we define three event models INC(p), DEC(p) and REPL(p, n,m) as in Figures 4-6. We have omitted edge labels, as we are in the single-agent case.

Lemma 2. For all m, n ∈ N, for all p ∈ P ,

Proof. We only prove item 1. Introducing names for the nodes and events, we can calculate as follows: CHAIN(p, n)⊗ INC(p) =

For all k ∈ N, we define φk := ✸(p1 ∧¬γk ∧γk+1). Using Lemma 1 and the definition of s(k,l,m), we immediately get that for all k, l,m, k′ ∈ N:

Let M = (I0, . . . , IT ) be a two-counter machine. For all k < T and all l, m ∈ N, we define an epistemic action aM(k, l, m) as in Figures 7-10 depending on the values of Ik, l andm. If k, l,m, k′ , l′ ,m′ ∈ N, we write (k, l,m) ≈ (k′ , l′ ,m′ ) when the following holds:

Note that when (k, l,m) ≈ (k′ , l′ ,m′ ) then aM(k, l,m) = aM(k′ , l′ ,m′ ), hence the following set is finite:

Lemma 3 below shows that FM really encodes the computation steps of the computation function.

Lemma 3. Let M = (I0, . . . , IT ) be a two-counter machine, l, m, n ∈ N and k < T . Then, the following holds:

1. aM(k, l,m) is applicable in sfM(n) iff (k, l,m) ≈ fM (n);

Proof sketch. Assume fM(n) = (k′ , l′ ,m′ ). Item 1 is by case of Ik. We only consider the cases Ik = inc(0) and Ik = jump(j). In these cases, aM(k, l,m) is an epistemic action of the form (E, e) with pre(e) = φk. Hence using equation (1) we get: aM(k, l,m) applicable in sfM(n) ⇔ s(k′ ,l′ ,m′ ) |= φk ⇔ k = k′ ⇔ (k, l,m) ≈ (k′ , l′ ,m′ ) because Ik = inc(0) or Ik = jump(j). Item 2 is by case of Ik′ . We only consider the case Ik′ = inc(0): sfM(n) ⊗ aM(fM(n)) = s(k′ ,l′ ,m′ ) ⊗ aM(k′ , l′ , m′ ) = s(k′+1,l′+1,m) = sfM(n+1), using Lemma 2 and that aM(k′ , l′ ,m′ ) is the epistemic action of Fig. 7.

3. Encoding of the halting problem. From Lemma 3, we derive the following lemma:

Lemma 4. Let M = (I0, . . . , IT ) be a two-counter machine. Define TM as the following epistemic planning task: TM = (s(0,0,0), FM, φT ). Then TM has a solution iff M halts.

So, from Lemma 4 and Theorem 1, we obtain:

Theorem 2. PLANEX(K,1) is undecidable.

5.2 Epistemic Planning for K4, K45, S4 and S5

We can prove an even stronger result than Theorem 2, namely that the plan existence problem for S4 planning tasks is undecidable (for |P | ≥ 2). Due to lack of space, we cannot provide the proof of this result and we refer the interested reader to [Aucher and Bolander, 2013] for more details. The proof is similar to the proof of undecidability of the next section.

Theorem 3. PLANEX(S4, 1) is undecidable.

As a direct corollary of Theorem 3, we have that singleagent epistemic planning for K4 and KT are also undecidable.

Despite all these negative results, there is still room for decidability in the single-agent case if we assume that knowledge or belief are negatively introspective:

Fig. 12: META-CHAIN(p, n)

Theorem 4. PLANEX(K45, 1) and PLANEX(S5, 1) are decidable.

Proof sketch. Any formula of K45 (and hence also of S5) is provably equivalent to a normal form formula of degree 1 [Meyer and van der Hoek, 1995]. Therefore any planning task on K45 will induce a state space of finite size (up to bisimulation contraction), and hence we have decidability.

6 Multi-agent Epistemic Planning

In the multi-agent setting, we prove a strong result, namely that multi-agent epistemic planning is undecidable for any logic between K and S5. The proof of this undecidability result generalises the proof for single-agent K given in Section 5.1, but we need an extra atomic proposition r (for better readability, we use four atomic propositions p1, p2, p3 and r, although we could use only two). The idea underlying the proof is to replace worlds with meta-worlds, which are in fact epistemic models.

1. Encoding of configurations. We encode configurations as two-agent S5-epistemic states. The worlds in CHAIN(p, n) of Figure 2 are replaced with the epistemic models META-WORLD(p) of Figure 11. The way meta-worlds are connected to each other to form a META-CHAIN(p, n) is shown in Figure 12. Then, for each configuration (k, l,m) ∈ N3 , we define an epistemic state s′(k,l,m) by replacing in Figure 3 CHAIN with META-CHAIN and by labeling the accessibility edges originating from the designated world with agent 1. Note that as we are in S5, all relations are equivalence relations, but the reflexive, symmetric and transitive closure is left implicit in figures.

1. Encoding of the computation function. Similarly to the case of single-agent K, we define path formulas.

Definition 10 (Path formulas). For all p ∈ P and n ∈ N, we define formulas λn(p), µn(p) and τn(p) inductively by:

We then obtain a counterpart of Lemma 1:

Fig. 15: META-REPL(p, n,m)

Lemma 5. For all p ∈ P , n ∈ N, 0 ≤ i ≤ n, 1 ≤ j ≤ 3n+3:

In other words, λi holds in the bottom world of the (i+ 1)th to last meta-world of META-CHAIN(p, n), µi in the top right world of the same meta-world and τi in the top left world of the same meta-world. Now define META-INC(p), META-DEC(p) and META-REPL(p, n, m) as in Figures 13-15.

Let M = (I0, . . . , IT ) be a two-counter machine. For all k < T and all l,m ∈ N, we define an epistemic action a′M (k, l,m) as in Figures 7-10 by: 1) replacing INC, DEC and REPL with META-INC, META-DEC and META-REPL respectively; 2) labeling the accessibility edges originating from the designated worlds with agent 1; 3) replacing φk with ✸1µk(p1); 4) replacing ✸(p2 ∧ γ1) with ✸1µ0(p2).

3. Encoding of the halting problem. If CHAIN, INC, DEC, aM and s(k,l,m) are replaced in Lemmata 2 and 3 with META-CHAIN, META-INC, META-DEC, a′M and s′(k,l,m) respectively, then these Lemmata still hold. Therefore, Lemma 4 and Theorem 2 also generalize to this two-agent S5 setting, and we finally obtain that:

Theorem 5. PLANEX(S5, n) is undecidable for any n ≥ 2.

7 DELModel Checking

The DEL language L∗DEL is defined by the following BNF:

where p ∈ P, i ∈ A and (E, e) is any epistemic action [van Ditmarsch et al., 2007]. In DEL, one assumes that |A| > 1. The truth conditions for the programs π are defined as follows:

The formula [E, e]φ reads as "after the execution of the epistemic action (E, e), it holds that φ". The model checking problem is the following: "Given an epistemic state (M,w), a formula φ ∈ L∗DEL, is it the case that M, w |= φ?". As an immediate corollary of our results, we have the following theorem. It complements the result of [Miller and Moss, 2005] stating that the satisfiability problem of DEL is undecidable.

Theorem 6. The model checking problem of the language L∗DEL is undecidable.

Proof. PLANEX(S5, n) is reducible to the model checking problem of the language L∗DEL: an epistemic planning task T = (s0, A, φg) has a solution iff s0 |= ¬[A∗ ]¬φg holds.

8 Conclusion

8.1 RelatedWork

Alternatives to the DEL-based approach to multi-agent planning with ToM abilities can be found both in the literature on temporal epistemic logics [van der Hoek and Wooldridge, 2002] and in the literature on POMDP-based planning [Gmytrasiewicz and Doshi, 2005]. However, these alternative formalisms express planning tasks in terms of an explicitly given state space, and hence do not address how to express actions in a compact and convenient formalism (and how to possibly avoid building the entire state space when solving planning tasks). In the DEL-based formalism the state space is induced by the action descriptions as in classical planning. Note that our assumptions in DEL-based planning correspond to the infinite horizon case of planning based on POMDPs, in which already ordinary, single-agent planning is undecidable [Madani et al., 1999].

8.2 Concluding Remarks

Our results are summarized in the table of Figure 16 (we recall that they hold only for |P| ≥ 2). From this table, we notice that in the single-agent setting, the property of Euclidicity (defined by Axiom 5: ¬✷iφ → ✷i¬✷iφ) draws the borderline between decidability and undecidability: if 5 is added to K4 or S4, we immediately obtain decidability.

Given these results, an important quest of course becomes to find fragments of the formalism in which interesting problems can still be formulated, but where the complexity is comparable to the complexity of other standard planning formalisms (varying from PSPACE-completeness for classical planning [Bylander, 1994] up to 2-EXP-completeness for planning under nondeterminism and partial observability [Rintanen, 2004]). We leave the quest for decidable fragments to future work. Initial results in this direction can be found in [L¨owe et al., 2011].