# decidability_results_in_firstorder_epistemic_planning__ae232d93.pdf

Decidability Results in First-Order Epistemic Planning

Andr es Occhipinti Liberman1 and Rasmus Kræmmer Rendsvig2

1DTU Compute, Technical University of Denmark 2Center for Information and Bubble Studies, University of Copenhagen aocc@dtu.dk, rasmus@hum.ku.dk

Propositional Dynamic Epistemic Logic (DEL) provides an expressive framework for epistemic planning, but lacks desirable features that are standard in ﬁrst-order planning languages (such as problem-independent action representations via action schemas). A recent epistemic planning formalism based on First-Order Dynamic Epistemic Logic (FODEL) combines the strengths of DEL (higher-order epistemics) with those of ﬁrst-order languages (lifted representation), yielding beneﬁts in terms of expressiveness and representational succinctness. This paper studies the plan existence problem for FODEL planning, showing that while the problem is generally undecidable, the cases of single-agent planning and multi-agent planning with non-modal preconditions are decidable.

1 Introduction

The development of autonomous agents is a key goal of artiﬁcial intelligence. A salient feature of autonomous agents is their ability to exhibit goal-directed behaviour, i.e., to commit to goals and generate plans to achieve them. In a multi-agent setting, agents often need to create their own plans taking into account, not only their own capabilities and knowledge, but also their knowledge about other agents. Epistemic planning [Baral et al., 2017] focuses on domains where such form of reasoning is key. For example, in an epistemic planning problem, agent a may have the following goal: a knows the truthvalue of ϕ, while b does not know that a knows this . To achieve this goal, agent a will typically need to reason about what it can do to learn ϕ, but also about what b may do or learn about ϕ from a s actions. In automated planning, standard formalisms such as the Planning Domain Deﬁnition Language (PDDL) model domains using ﬁrst-order logic. A notable advantage of ﬁrstorder over propositional languages is that variables can be used to deﬁne domain dynamics compactly. E.g., in the PDDL description of Blocks World, the action schema stack(x, y) uses variables x and y to represent the preconditions and effects of all actions of the form: put block x on top of block y . By lifting the representation to the level of

variables, schemas yield action representations whose size is independent of the number of objects in a domain. Formalisms such as PDDL can describe how actions change the physical state of the environment, but rarely model the mental states of agents or knowledge dynamics. Automated planning has therefore recently seen an inﬂux of work on epistemic planning based on Dynamic Epistemic Logic (DEL). DEL offers a highly expressive basis for planning, allowing e.g. nondeterminism, partial observability and arbitrary levels of higher-order reasoning. For an overview, see e.g. [Bolander, 2017]. However, the DEL language is propositional, and this has drawbacks. For instance, DEL cannot provide problem-independent action deﬁnitions via schemas. Recently, Achen, Occhipinti Liberman and Rendsvig [2020] introduced an epistemic planning formalism based on First-Order Dynamic Epistemic Logic (FODEL). FODEL integrates the higher-order expressivity of DEL with the ﬁrstorder abstraction level of languages such as PDDL. It is based on term-modal logic: ﬁrst-order modal logics where the operators double as predicates by taking ﬁrst-order terms as subscripts, with e.g. x Kx P(x) a well-formed formula. This allows agents and epistemic formulas in action schemas. While this yields advantages in terms of expressiveness and representational succinctness, the decidability and complexity aspects of FODEL have not been explored. This paper studies the decidability of the plan existence problem for FODEL planning. For DEL, the problem is undecidable in general [Bolander and Andersen, 2011], entailing that the unrestricted FODEL problem is undecidable as well, since FODEL planning extends DEL planning. However, decidable and reasonably expressive fragments of DEL planning have been found, such as single-agent planning and multi-agent planning with nonmodal preconditions. The main results of this paper show that the corresponding FODEL fragments are also decidable. Before reaching the main results, Section 2 presents the FODEL framework: its syntax, semantics, action schemas and updates, and planning notions, while Section 3 introduces ﬁrst-order bisimulations for term-modal models. The notion and accompanying results are essential to the study of FODEL planning: As for DEL planning [Bolander and Andersen, 2011; Yu et al., 2013], the decidability proofs of Section 4 rely crucially on constraining the state space, to ensure that only ﬁnitely many states must be visited to check for a

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

plan. In the decidable DEL cases, this is achieved by showing that the inﬁnite state space to be searched is ﬁnitely representable up to bisimulation. Hence, the notion of bisimulation is pivotal to such proofs. Introducing FODEL bisimulations and developing the accompanying model-theoretic results allows us to apply similar arguments to FODEL planning and ultimately establish decidability for single-agent planning as well as multi-agent planning with non-modal preconditions.

2 First-Order Dynamic Epistemic Logic

Throughout, we adopt the epistemic planning framework developed in detail in [Achen et al., 2020]. Additional FODEL examples may be found in [Occhipinti Liberman and Rendsvig, 2019]. For an introduction to epistemic planning with DEL, see e.g. [Bolander, 2017].

2.1 Language Term-modal logical languages are parameterized by a signature specifying the non-logical symbols and their type i.e., the constants and relation symbols, and the sort of arguments (agents or objects) they apply to. For the purposes of representing epistemic planning, we limit attention to function-free signatures with ﬁnitely many predicate and constant symbols. This restriction is not assumed in [Achen et al., 2020].

Deﬁnition 1. A signature is a tuple Σ = (V, C, R, t) where V := Vagt Vobj is a set of agent and object variables, with Vagt and Vobj both countably inﬁnite, C a ﬁnite set of constant symbols and R a ﬁnite set of predicate symbols. The terms of Σ are T := V C. Finally, t is a type assignment that satisﬁes (i) for x T, t(x) {agt, obj} with t(x) = i for all x Vi, i {agt, obj}, and (ii) for r R with arity n, t(r) {agt, obj}n. We denote by ti(r) the i-th component of t(r) and by ar(r) the arity of r.

Deﬁnition 2. Let Σ be a signature. The language L(Σ) is given by the grammar:

ϕ := r(t1, ..., tn) | ϕ | ϕ ϕ | Ktϕ | xϕ

where t1, . . . , tn T, r R, (t(t1), ..., t(tn)) t(r), t T with t(t) = agt, and x V. An atom is a formula of the form r(t1, ..., tn); it is ground if it contains no variables and free if it only contains variables. Ground Atoms(L(Σ)) and Free Atoms(L(Σ)) denote the set of ground and free atoms of L(Σ). A sentence is a formula without free variables. L0(Σ) is the Kt-free sublanguage.

Throughout, the standard Boolean connectives as well as , and are used as meta-linguistic abbreviations as usual. Ktϕ is read as agent t knows that ϕ .

2.2 Epistemic Models In epistemic logic-based planning frameworks, states are represented using variants of Kripke models [Kripke, 1962]. We use constant domain Kripke models (the same domain in each world) with non-rigid constants (names, like predicates and relations, may change extension between worlds, allowing for uncertainty about agent identity). Models where agents accessibility relations are equivalence relations are standard in epistemic planning, and here called epistemic models. A

ann bob eva key

a1 a2 a3 o1

ann bob eva key

a1 a2 a3 o1

sees a2, a3

Figure 1: An epistemic state s0 = (M, w1) for L({x , x1, x2, . . . }, {ann, bob, eva, key}, {owns, sees}, t). Types are t(c) = agt for c {ann, bob, eva}, t(key) = obj, t(owns) = (agt, obj) and t(sees) = (agt, agt). The state has worlds W M = {w1, w2}, domain DM = {a1, a2, a3, o1} and accessibility relations Ra1 = {(w1, w1), (w2, w2)}, Ra2 = Ra3 = W W (reﬂexive world-edges are not drawn). The interpretation function is depicted like so: squiggly lines link constants to entities, and predicate-labelled arrows relate entities for predicates (e.g., (a1, o1) IM(owns, w1)). In the actual world w1, ann owns the key. bob and eva do not know this (they cannot distinguish w1 and w2). Everyone knows that bob can see ann.

model with a designated world is a state; Figure 1 depicts an epistemic state, formally deﬁned below.

Deﬁnition 3. An L(Σ) model is a tuple M = (DM, W M, RM, IM) where (i) the domain DM := Dagt Dobj is the disjoint union of the non-empty sets Dagt and Dobj (the agent domain and the object domain); (ii) W M

is a non-empty set of worlds; (iii) RM : Dagt P(W W) associates to each agent d Dagt an accessibility relation on W, denoted RM d , and (iv) IM is an interpretation satisfying: IM(c, w) Dt(c) if c C and IM(r, w) Qn i=1 Dti(r) for r R with arity n. For w W M, the pair s = (M, w) is called a state. A state s is called ﬁnite if W M is ﬁnite. If RM d is an equivalence relation for all d Dagt, then M is an epistemic model, and s = (M, w) is then an epistemic state.

Truth conditions for formulas of L(Σ) are deﬁned over states, together with a variable assignment.

Deﬁnition 4. A variable assignment for a model M is a map g : V DM with g(x) Dt(x) for each x V. Denote by g[x 7 d] the assignment mapping x to d but else identical to g. The extension of term t T at w in M, under g, is Jt KIM,g w = g(t) if t V and Jt KIM,g w = IM(t, w) if t C. If M is given by context, we omit it and write Jt KI,g w .

Deﬁnition 5. Let M and g be given. Then M, w g r(t1, ..., tn) iff (Jt1KI,g w , ..., Jtn KI,g w ) IM(r, w) M, w g ϕ iff not M, w g ϕ. M, w g ϕ ψ iff M, w g ϕ and M, w g ψ. M, w g xϕ iff M, w g[x7 d] ϕ for all d Dt(x). M, w g Ktϕ iff M, v g ϕ for all v s.t. (w, v) RM Jt KI,g w .

2.3 Actions Schemas and Actions The FODEL planning framework uses action schemas to provide compact, problem-independent domain descriptions in the spirit of PDDL (see Figure 2). FODEL action schemas use variables as action parameters, so a single schema may be used, e.g., to represent all actions of the form agent x gives agent y object z , where x, y and z are agent or object variables, later instantiated into speciﬁc constants to deﬁne

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

e1 : owns(x, y); id e2 : ; id

sees(x , x)

Figure 2: announce own(x, y), the schema for agent x announcing that it owns y. Each event is drawn with the format pre(e), post(e) , where id is the identity map (i.e., no factual change). The actual event e1 (marked with a double circle) describes the announcement that x owns y. e2 describes the situation in which nothing happens. Agents that do not see x will not learn what is being announced. The edge-condition Q(e1, e2) = Q(e2, e1) = sees(x , x) deﬁnes this (Q(e1, e1) = Q(e2, e2) = not drawn).

a (ground, epistemic) action. As in classical planning formalisms such as PDDL, a major reason for using schemas is that they allow action representations whose size is independent of the number of agents and objects in a domain. FODEL action schemas include preconditions [Baltag et al., 1998], postconditions [van Benthem et al., 2006; van Ditmarsch et al., 2005] as well as edge-conditions in the style of [Bolander, 2014]. Preconditions specify when an event is executable. Postconditions describe the physical effects of events. Edge-conditions describe how an agent observes the action in terms of the agent s circumstances. Deﬁnition 6. An action schema is a form a( x) = (E, Q, pre, post) where (i) a is the action name and x Vn is a ﬁnite parameter list; (ii) E is a non-empty, ﬁnite set of events; (iii) Q : (E E) L(Σ) is an edge-condition function, where the formula Q(e, e ) has a free variable x of type agt, and possibly other free variables all in x; (iv) pre : E L(Σ) assigns to each event a precondition formula with all free variables in x; (v) post : E (Free Atoms(L) L(Σ)) assigns to each event a partial postcondition function such that if y1, . . . , ym x, then post(e)(r(y1, . . . , ym)) has all free variables from x; else, post(e)(r(y1, . . . , ym)) is undeﬁned. dom(post(e)) denotes the set of atoms for which post(e)(r(t1, . . . , tk)) = r(t1, . . . , tk) and is required ﬁnite for each e E, so postconditions are ensured ﬁnite objects. Schema instantiation is deﬁned as follows. Deﬁnition 7. Let a(x1, . . . , xn) be an action schema and σ : {x1, . . . , xn} C be a grounding substitution mapping action parameters to constants. For ϕ L(Σ), let ϕσ be the result of replacing each free occurence of y V in ϕ by σ(y). For an action schema a( x) = (E, Q, pre, post), the action model induced by the grounding substitution σ is the tuple A = a(σ( x)) = (EA, QA, pre A, post A) where (i) EA = E (ii) QA(e, e ) = Q(e, e )σ; (iii) pre A(e) = pre(e)σ; (iv) post A(e)(r(t1, . . . , tn)σ) = post(e)(r(t1, . . . , tn))σ if post(e)(r(t1, . . . , tn)) is deﬁned; and post A(e)(r(t1, . . . , tn)σ) = r(t1, . . . , tn)σ otherwise. A pair a = (A, e) with e EA is called an epistemic action, where e is the actual event taking place on execution.

2.4 Product Update Execution is deﬁned by the operation that computes the state s = s a reached by applying action a in state s. The operation is a ﬁrst-order variant of product update from [Baltag et al., 1998]. The new state s represents the agents perception of s = (M, w) after the occurrence of the action

ann bob eva key

a1 a2 a3 o1

ann bob eva key

a1 a2 a3 o1

ann bob eva key

a1 a2 a3 o1

Figure 3: The epistemic state s0 announce own(ann, key). bob now knows that ann owns the key. However, eva still does not know this, as she did not see bob making the announcement.

described by a = (A, e). Figure 3 exempliﬁes the product update of the state from Figure 1 and an instance of the schema in Figure 2. Deﬁnition 8. Let a = ((E, Q, pre, post), e) be an action and s = ((D, W, R, I), w) a state. The product update of s and a is the state s a = ((D, W , R , I ), (w, e)) where for any g - W = {(w, e) W E | (M, w) g pre(e)} - (w, e)R d(w , e ) iff w Rdw and M, w g[x 7 d] Q(e, e )

- I (c, (w, e)) = I(c, w) for all c C and I (r, (w, e)) = (I(r, w) r+(w)) \ r (w), where r+(w) := {(Jt1KI,g w , . . . , Jtk KI,g w ) | (M, w) g post(e)(r(t1, . . . , tk))}

r (w) := {(Jt1KI,g w , . . . , Jtk KI,g w ) | (M, w) g post(e)(r(t1, . . . , tk))}

An action a = (A, e) is applicable in a state s = (M, w) iff (M, w) g pre(e). Else s a is undeﬁned.

2.5 Planning Notions As presented in [Ghallab et al., 2004], any classical planning domain can be described as a state-transition system T = (S, A, γ) where S is a ﬁnite or recursively enumerable set of ﬁnite states, A is a ﬁnite set of actions and γ : S A S is a partial, computable state-transition function. A classical planning task is given by a triple (T, s0, SG), where T is a state-transition system, s0 S is the initial state and SG S is the set of goal states. A solution to a classical planning task (T, s0, SG) is a plan consisting of a ﬁnite sequence of actions a1, a2, . . . , an such that (1) For all i n, γ(γ(. . . γ(γ(s0, a1), a2), . . . , ai 1), ai) is deﬁned, and (2) γ(γ(. . . γ(γ(s0, a1), a2), . . . , an 1), an) SG. Epistemic planning tasks can be deﬁned as special cases of classical planning tasks. Deﬁnition 9. Let A be a ﬁnite set of L(Σ) action schemas. An epistemic planning task based on A is a triple P = (s0, A, ϕG) where the initial state s0 is a ﬁnite epistemic state with a ﬁnite domain, A is the set of all ground instances of the schemas in A, and the goal formula ϕG is a sentence of L(Σ). Any epistemic planning task (s0, A, ϕG) induces a classical planning task ((S, A, γ), s0, SG) given by:

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

- S := {s0 a1 an | n N, ai A}

- SG := {s S | s ϕG}

- γ(s, a) := s a if a is applicable in s, else undeﬁned.

A solution to an epistemic planning task is a solution to the induced classical planning task.

We follow Aucher and Bolander [2013] in deﬁning the plan existence problem:

Deﬁnition 10. Let n N. Plan Ex(n) is the problem: Given an epistemic planning task P = (s0, A, ϕG) where s0 is an n-agent L(Σ)-epistemic state, does P have a solution? .

3 First-Order Bisimulations

To obtain a bisimulation notion for ﬁrst-order, term-modal models, we retain the back and forth conditions of propositional modal logical bisimulation, but replace the atomic harmony condition with ﬁrst-order logical isomorphism. The resulting notion implies modal equivalence and is preserved under product updates. Further, n-bisimulation is deﬁned and shown to imply modal equivalence for formulas of restricted modal depth, and states are shown to be bisimilar to their bisimulation contractions. These results all extend to FODEL standard properties of bisimulations in propositional DEL and are key in proving the later decidability proofs, as they allow us to show that the state spaces for some planning fragments are ﬁnitely representable, up to bisimulation.1

3.1 Isomorphisms, Bisimulations and Equivalence We ﬁrst recall the notion of an isomorphism, viewed here as a relationship between worlds in L(Σ) models.

Deﬁnition 11. Let M and N be L(Σ) models. An isomorphism between w W M and v W N is a bijection f : DM DN such that, for all c C and r R,

1. f(IM(c, w)) = IN(c, v)

2. (d1, ..., di) IM(r, w) iff (f(d1), ..., f(di)) IN(r, v)

If w and v are isomorphic based on f, we write w f v.

We then use isomorphisms to ensure that worlds linked by a bisimulation agree on all L0(Σ) formulas, while also relating agents and hence accessibility relations appropriately in the forth and back conditions:

Deﬁnition 12. For models M and N, let f : DM DN be a bijection. A non-empty relation Zf W M W N is an f-based bisimulation between M and N if

Atoms: If (w, w ) Zf, then w f w ,

Forth: If (w, w ) Zf and RM d wv, then there exists v such that RN f(d)w v and (v, v ) Zf, for all d Dagt,

1The existing work on bisimulations for ﬁrst-order modal logic models [van Benthem, 2010a; van Benthem, 2010b; Zoghifard and Pourmahdian, 2018] concern varying domain models, with their added complexity. See [Achen et al., 2020] for a planning related discussion. The resulting potential isomorphism-based world-object bisimulations are both more general and more complex than what is needed for present purposes, while not tuned to term-modal logics.

Back: If (w, w ) Zf and RN f(d)w v , then there exists v such that RM d wv and (v, v ) Zf, for all d Dagt.

If (w, w ) Zf for any f-based bisimulation Zf between M and N, call (M, w) and (N, w ) bisimilar, written (M, w) (N, w ).

Since any two bisimilar worlds w and w are required to be isomorphic, the relation (M, w) (N, w ) can only hold between models with domains of equal cardinality. Next, we deﬁne n-bisimulations and bisimulation contractions.

Deﬁnition 13. For models M and N, let f : DM DN be a bijection. A non-empty relation Zn f W M W N is an f-based n-bisimulation between states (M, w) and (N, w ) if w f w , and either n = 0 or, for some f-based (n 1)- bisimulation Zn 1 f

Forth: If RM d wv then there exists v such that RN f(d)w v and v Zn 1 f v , for all d Dagt,

Back: If RN f(d)w v then there exists v such that RM d wv and v Zn 1 f v , for all d Dagt.

If (w, w ) Zn f for any f-based n-bisimulation Zn f between (M, w) and (N, w ), call them n-bisimilar, written (M, w) n(N, w ).

Deﬁnition 14. The bisimulation contraction of a L(Σ) model M is M = (DM, W , R , I ) where

- W = {[w] | w W M} where [w] = {v W M | (M, w) (M, v)};

- ([w] , [v] ) R d iff there are w [w] and v [v] such that RM d w v ;

- For all w W, c C and r R, I (c, [w] ) = IM(c, w) and I (r, [w] ) = IM(r, w)

The n-bisimulation contraction M n is deﬁned in the same way based on n.

Finally, we ﬁx the relevant notions of logical equivalence:

Deﬁnition 15. Let M and N be models. Two worlds w W M and v W N are elementary equivalent, if for any sentence ϕ L0(Σ) M, w g ϕ iff N, v g ϕ. If the same holds for any sentence ϕ L(Σ), then they are modally equivalent.

3.2 Results on First-Order Bisimulations With the notions deﬁned, we turn to showing the results needed for the later decidability proofs. First, we recall a well-known result (see, e.g. [Rothmaler, 2018]).

Lemma 1. If w and v worlds in M and N respectively, then w f v implies that w and v are elementary equivalent. If M and N have ﬁnite domains, then the converse also holds.

From this, we show that bisimulation implies modal equivalence, without restriction. For the converse, call a model M image-ﬁnite models if for each world w W M and each relation RM d , the set {v W M | RM d wv} is ﬁnite. We then establish a variant of the Hennessy-Milner Theorem known from propositional modal logic:

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

Proposition 1. 1. If there is an f-based bisimulation between (M, w) and (N, w ) then for all ϕ L(Σ): M, w g ϕ iff N, w f g ϕ. 2. If M and N are image-ﬁnite and with ﬁnite domains, the converse also holds.

Proof. 1. By induction on the complexity of ϕ. The base case where ϕ is an atomic formula follows from Lemma 1. Boolean cases are straightforward. We show the modal case with ϕ = Ktψ. If t V, assume that M, w g Ktψ and RM g(t)wv. As w w , there is a v such that RN f(g(t))w v and v v . By the induction hypothesis, we get N, v f g ϕ. As v was picked arbitrarily, M , w f g Ktψ. If instead t C, assume that M, w g Ktψ and RM I(t,w)wv. As w w , there is a v such that RN f(IM(t,w))w v and v v . By the induction hypothesis, we get N, v f g ϕ. Given w w we get w f w and thus IN(t, w ) = f(IM(t, w)). Hence, since v was arbitrary and IN(t, w ) = f(IM(t, w)), we get N, w f g Ktϕ. The other direction is similar. 2. The modal equivalence relation may be shown to be a bisimulation. The proof is analogous to the propositional case (see [Blackburn et al., 2001, Thm 2.24]), save for Atoms. But this holds as modal equivalence of worlds joint with the ﬁnite domain assumption by Lemma 1 implies isomorphism.

The modal depth of a formula ϕ, denoted md(ϕ), is the depth of nesting of modal operators in ϕ. As in the propositional case, n-bisimilar states agree on all formulas of L(Σ) whose modal depth is at most n.

Proposition 2. If there is an f-based n-bisimulation between (M, w) and (N, w ), then for all ϕ L(Σ) with md(ϕ) n: M, w g ϕ iff N, w f g ϕ.

Proof. By induction on n. For n = 0, note that w f v. Thus by Lemma 1, w and w are elementary equivalent, establishing the correspondence for sentences of modal depth 0. When free variables are assigned using g and f g, this extends to all 0-depth formulas. The inductive step is standard (see, e.g. [Blackburn et al., 2001]), except for checking that the interpretations of modal indices match appropriately between models, which they do, given f.

As in the propositional case, any state is bisimilar to its bisimulation contraction, a result used in the second decidability proof below.

Proposition 3. For any (M, w), (M, w) (M , [w] ) and for any j such that j n 0, (M, w) n(M j, [w] j).

Proof. The proof for each case is analogous to its propositional counterpart, see e.g. [Blackburn and van Benthem, 2007] for the case, and [Yu et al., 2013] for the n case. Both are by induction on n, both with induction steps that carry over to FODEL. The base cases follow by deﬁnition of and j.

Additionally towards proving decidability, we show that the variant of product update preserves bisimilarity. This is known for product update on propositional models, and here it is extended to ﬁrst-order, edge-conditioned updates.

Proposition 4. For any action (A, e), if (M, w) (M , w ), then 1. (M, w) (A, e) is deﬁned iff (M , w ) (A, e) is, and 2. if deﬁned, then (M, w) (A, e) (M , w ) (A, e).

Proof. 1. Follows by Proposition 1. 2. (M, w) (M , w ) implies there is a bijection f : DM DM and an fbased bisimulation Zf with w Zfw . Deﬁne Z f W M A W M A by (v, e1)Z f(v , h1) iff v Zfv and e1 = h1. Then Z f is an f-based bisimulation: Atoms: v Zfv requires that v f v . This implies that (v, e) f (v , e) for any e, as post will have identical effects on v and v . Forth: Assume that (v, e1)Z f(v , e1) and (v, e1)RM A d (u, e2). Then v Zfv , v RM d u and M, v g[x 7 d] Q(e1, e2). As v Zfv , also M , v g[x 7 d] Q(e1, e2). As v RM d u and v Zfv , there is u

s.t. v RM d u and u Zfu . As (u, e2) W M A and u Zfu , also (u , e2) W M A. Hence also (v , e1)RM A d (u , e2), so (u, e2)Z f(u , e2). The proof for Back is similar.

A corresponding result holds as well for n-bisimulations and actions with non-modal preconditions:

Proposition 5. For any two n-bisimilar L(Σ) states (M, w) and (M , w ) and any action (A, e) with pre(e ) L0(Σ) for all e EA, 1. (M, w) (A, e) is deﬁned iff (M , w ) (A, e) is, and 2. if deﬁned, (M, w) (A, e) n(M , w ) (A, e).

Proof. 1. Since (M, w) n(M , w ), w f w . As pre(e) L0(Σ), M, w g pre(e) iff M , w f g pre(e). 2. Assume that (A, e) is applicable in (M, w). We can prove (M, w) n(M , w ) by induction on n. Base case: n = 0. Since (M, w) 0(M , w ), then w f w . Thus, by the semantics of product update, (w, e) f (w , e). The inductive step is analogous to [Yu et al., 2013, Proposition 4.14].

4 Decidability Results

4.1 Single-Agent Planning We show ﬁrst that single-agent FODEL planning is decidable. The gist of the proof is that each single-agent epistemic state is shown bisimilar to a canonical state , and that there are ﬁnitely many such canonical states. Hence the state space for single-agent planning is ﬁnitely representable, and it can therefore be decided whether such task is solvable. We deﬁne these canonical states as follows:

Deﬁnition 16. Given a signature Σ and a domain D with Dagt = {d}, deﬁne the structure M(Σ,D) as the tuple (D, W, W W, I) where W is the set of ﬁrst-order interpretations i of Σ over D and I(x, i) = i(x) for all x C R and all i W. The M(Σ,D) substate of a single-agent L(Σ) epistemic state (M, w) = (D, W, R, I, w) is the epistemic state (M , w ) = (D, W , R , I , w ) where

W = {i W | u W s.t. Rdwu and x C R, I(x, u) = I(x, i)}, R d = W W , I (x, i) = I(x, i), x C R, i W , w = i s.t. I(x, i ) = I(x, w), x C R.

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

Lemma 2. Any single-agent L(Σ) epistemic state (M, w) is bisimilar to its M(Σ,D) substate (M , w ).

Proof. Deﬁne Zf W W by v Zfv iff Rdwv and x C R, I(x, v) = I (x, v ), where f is the identity map. Then Zf is a bisimulation and it links w to w : Atoms: If v Zfv then I(x, v) = I (x, v ), x C R, which, since M and M share domain D, entails v and v are elementary equivalent. As D is ﬁnite, by Lemma 1, v f v . Forth: Assume that v Zfv and Rdvu. By deﬁnition of M , there is a u W s.t. x C R, I(x, u) = I (x, u ). By deﬁnition of Zf, we have Rdwv and so, by transitivity, that Rdwu. Hence u Zfu . Finally, as R d = W W , we have R dv u . Back: Assume that v Zfv and R dv u . By deﬁnition of M , there is a u W such that Rdwu and I(x, u) = I (x, u ), x C R. Hence, u Zfu . As v Zfv , by deﬁnition, we have Rdwv. As also Rdwu, we have Rdvu, by Euclideaness. Link: Finally, as I(x, w) = I (x, w ), x C R, and Rdww by reﬂexivity, it follows that w Zfw .

Lemma 3. There are only ﬁnitely many non-bisimilar singleagent L(Σ) epistemic states with underlying ﬁnite domain D.

Proof. By Lemma 2, any single-agent L(Σ) epistemic state (M, w) with domain D is bisimilar to a M(Σ,D) substate. Hence, up to bisimulation, the set of single-agent L(Σ) epistemic states is representable by a set of M(Σ,D) substates. Since both Σ and D are ﬁnite, there are only ﬁnitely many ﬁrst-order interpretations of Σ over D i.e., W is ﬁnite. Hence M(Σ,D) has ﬁnitely many substates.

Theorem 1. Plan Ex(1) (single-agent planning) is decidable.

Proof. Let P = (s0, A, ϕG) be a single-agent planning task. By Proposition 1 and Lemma 2, any epistemic state and its M(Σ,D) substate are bisimilar and hence agree on ϕG. By Proposition 4, bisimilarity is preserved under product update. Thus, to check if there is a plan, we do a breadth-ﬁrst search of the state space, replacing each visited epistemic state by its M(Σ,D) substate. By Lemma 3, this state space is ﬁnite.

4.2 Multi-Agent Planning Concerning multi-agent planning, the plan existence problem is undecidable for unrestricted FODEL planning. This follows directly from the problem being undecidable for DEL planning and FODEL containing DEL as a special case: any DEL language can be simulated with a signature Σ consisting only of 0-ary predicates. Aucher and Bolander [2013] show that DEL planning is undecidable already for two agents.

Proposition 6. For k 2, Plan Ex(k) is undecidable.

Reasonably expressive DEL fragments are decidable, such as the fragment in which all actions have propositional preconditions. We show that this result generalizes to FODEL. Our result is inspired by [Yu et al., 2013], which shows decidability for DEL. As in the single-agent case, the proof exploits the fact that the state space in such case can be shown to be ﬁnite (up to bisimulation). We ﬁx some lemmas.

Lemma 4. There are ﬁnitely many non-bisimilar L(Σ) states with ﬁnite domain D and exactly n worlds.

Proof. Let |W| = n. As Σ and D are ﬁnite, the set I of interpretations deﬁnable for W, Σ and D is ﬁnite. As Dagt D is ﬁnite, also the set R of deﬁnable accessibility relations for Dagt and W is ﬁnite. Hence the set of states {(M, w) | DM = D, W M = W, RM R, IM I, w W} is ﬁnite. As the choice of W is irrelevant for bisimilarity, there are thus only ﬁnitely many non-bisimilar states with n worlds.

Yu et al. [2013] showed that the number of n equivalence classes of Kripke model has a ﬁxed ﬁnite bound that depends on n, generalizing a result from Visser [1996]. We show a similar result for ﬁrst-order models. Lemma 5. Let M be an L(Σ) model with ﬁnite domain D. Let |D| = m and |Dagt| = ℓ. Denote by Fn(M) the number of n equivalence classes of worlds of M. Let f(0) := m! and f(i + 1) := m!2f(i)+ℓfor i 0. Then Fn(M) f(n).

Proof. By induction on k. Let M = (D, W, R, I). Base case: k = 0. If w f v, then M, w 0M, v. As there are m! bijections from D into D, there are at most m! non-isomorphic worlds in M and thus at most m! 0 equivalence classes. Hence F0(M) f(0). Inductive step: Assume that the statement holds for k. We prove it for k + 1. For any w W and d Dagt, let Rd[w] := {[w ] k | Rdww }. Then, for any w1, w2 W, if w1 f w2 and Rd[w1] = Rd[w2] for all d Dagt, then (M, w1) k+1(M, w2). For any d Dagt, there are at most 2Fk(M) distinct possibilities for Rd[w]. Hence Fk+1(M) m!(2Fk(M))ℓ m!(2f(k))ℓ= m!2f(k)+ℓ= f(k + 1).

Theorem 2. If all actions have non-modal preconditions, then Plan Ex(k) is decidable, for k 1.

Proof. Let P = (s0, A, ϕG) be an epistemic planning task with md(ϕG) = n. By Proposition 3, any epistemic state and its n-bisimulation contraction are n-bisimilar and thus agree on ϕG. By Proposition 5, product update preserves n-bisimilarity. To check for a plan, we do a breath-ﬁrst search of the state space, replacing each visited state by its nbisimulation contraction. By Lemma 5, any n-bisimulation contracted model has at most Fn(M) N worlds and by Lemma 4, the number of non-bisimilar states with at most Fn(M) worlds is ﬁnite.

5 Final Remarks FODEL combines the higher-order expressiveness of DEL with the ﬁrst-order abstraction of languages such as PDDL to compactly describle epistemic planning domains. We have introduced bisimulations for FODEL models and exploited them to show decidability for single-agent planning and multi-agent planning with non-modal preconditions. Future work could study other decidable fragments, the complexity of FODEL planning, or FODEL planning algorithms.

Acknowledgements The Center for Information and Bubble Studies is funded by the Carlsberg Foundation. RKR was partially supported by the DFG-ANR joint project Collective Attitude Formation [RO 4548/8-1].

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

[Achen et al., 2020] Andreas Achen, Andr es Occhipinti Liberman, and Rasmus K. Rendsvig. Dynamic Term Modal Logics for First-Order Epistemic Planning. Artiﬁcial Intelligence, forthcoming, 2020.

[Aucher and Bolander, 2013] Guillaume Aucher and Thomas Bolander. Undecidability in Epistemic Planning. In Twenty-Third International Joint Conference on Artiﬁcial Intelligence, 2013.

[Baltag et al., 1998] Alexandru Baltag, Lawrence S. Moss, and Sławomir Solecki. The Logic of Public Announcements, Common Knowledge, and Private Suspicions (extended abstract). In TARK 98: Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge, pages 43 56. Morgan Kaufmann Publishers, 1998.

[Baral et al., 2017] Chitta Baral, Thomas Bolander, Hans van Ditmarsch, and Sheila Mc Ilrath. Epistemic Planning (Report from Dagstuhl Seminar 17231). Dagstuhl Reports, 7(6):1 47, 2017.

[van Benthem et al., 2006] Johan van Benthem, Jan van Eijck, and Barteld P. Kooi. Logics of Communication and Change. Information and Computation, 204(11):1620 1662, 2006.

[van Benthem, 2010a] Johan van Benthem. Frame Correspondences in Modal Predicate Logic. In S. Feferman and W. Sieg, editors, Proofs, Categories and Computations. Essays in Honor of Grigori Mints. College Publications, 2010.

[van Benthem, 2010b] Johan van Benthem. Modal Logic for Open Minds. CSLI, 2010.

[Blackburn and van Benthem, 2007] Patrick Blackburn and Johan van Benthem. Modal Logic: A Semantic Perspective. In Studies in Logic and Practical Reasoning, volume 3, pages 1 84. Elsevier, 2007.

[Blackburn et al., 2001] Patrick Blackburn, Maarten De Rijke, and Yde Venema. Modal Logic. Cambridge University Press, 2001.

[Bolander and Andersen, 2011] Thomas Bolander and Mikkel Birkegaard Andersen. Epistemic planning for singleand multi-agent systems. Journal of Applied Non-Classical Logics, 21(1):9 34, 2011.

[Bolander, 2014] Thomas Bolander. Seeing is Believing: Formalising False-Belief Tasks in Dynamic Epistemic Logic. In Andreas Herzig and Emiliano Lorini, editors, European Conference on Social Intelligence (ECSI 2014), volume 1283 of CEUR Workshop Proceedings, pages 87 107, 2014.

[Bolander, 2017] Thomas Bolander. A Gentle Introduction to Epistemic Planning: The DEL Approach. In Proceedings of Methods for Modalities 2017 (M4M9), volume 243 of Electronic Proceedings of Theoretical Computer Science, pages 1 22, 2017.

[van Ditmarsch et al., 2005] Hans van Ditmarsch, Wiebe van der Hoek, and Barteld P. Kooi. Dynamic Epistemic Logic with Assignment. In Proceedings of the Fourth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 05), pages 141 148. ACM, 2005. [Ghallab et al., 2004] Malik Ghallab, Dana Nau, and Paolo Traverso. Automated Planning: Theory and Practice. Morgan Kaufmann, 2004. [Kripke, 1962] Saul A. Kripke. The Undecidability of Monadic Modal Quantiﬁcation Theory. Zeitschrift f ur mathematische Logik und Grundlagen der Mathematik, 8:113 116, 1962. [Occhipinti Liberman and Rendsvig, 2019] Andr es Occhipinti Liberman and Rasmus K. Rendsvig. Dynamic Term Modal Logic for Epistemic Social Network Dynamics. In Patrick Blackburn, Emiliano Lorini, and Meiyun Guo, editors, Logic, Rationality, and Interaction (LORI 2019), volume 11813 of Lecture Notes in Computer Science, pages 168 182. Springer, 2019. [Rothmaler, 2018] Philipp Rothmaler. Introduction to Model Theory. CRC Press, 2018. [Visser, 1996] Albert Visser. Uniform Interpolation and Layered Bisimulation. In Petr H ajek, editor, G odel 96: Logical Foundations of Mathematics, Computer Science and Physics Kurt G odel s Legacy, volume 6 of Lecture Notes in Logic, pages 139 164. Cambridge University Press, 1996. [Yu et al., 2013] Quan Yu, Ximing Wen, and Yongmei Liu. Multi-Agent Epistemic Explanatory Diagnosis via Reasoning about Actions. In Twenty-Third International Joint Conference on Artiﬁcial Intelligence, pages 1183 1190, 2013. [Zoghifard and Pourmahdian, 2018] Reihane Zoghifard and Pourmahdian Pourmahdian. First-Order Modal Logic: Frame Deﬁnability and a Lindstr om Theorem. Studia Logica, 106(4):699 720, 2018.

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)