Decidability Results in First-Order Epistemic Planning

1 Introduction

The development of autonomous agents is a key goal of artificial 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 Definition Language (PDDL) model domains using first-order logic. A notable advantage of firstorder over propositional languages is that variables can be used to define domain dynamics compactly. E.g., in the PDDL description of BlocksWorld, 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 influx 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 definitions 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 firstorder abstraction level of languages such as PDDL. It is based on term-modal logic: first-order modal logics where the operators double as predicates by taking first-order terms as subscripts, with e.g. ∃xKxP(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 first-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 finitely many states must be visited to check for a plan. In the decidable DEL cases, this is achieved by showing that the infinite state space to be searched is finitely 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 finitely many predicate and constant symbols. This restriction is not assumed in [Achen et al., 2020].

Definition 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 infinite, C a finite set of constant symbols and R a finite set of predicate symbols. The terms of Σ are T := V ∪ C. Finally, t is a type assignment that satisfies (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.

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

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. GroundAtoms(L(Σ)) and FreeAtoms(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

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

Definition 3. An L(Σ) model is a tuple M = (DM ,W M ,RM , I M ) 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) I M is an interpretation satisfying: I M (c,w) ∈ Dt(c) if c ∈ C and I M (r,w) ⊆ ∏ni=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 finite if W M is finite. If RM d is an equivalence relation for all d ∈ Dagt, thenM is an epistemic model, and s = (M, w) is then an epistemic state.

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

Definition 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 ↦→ 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 JtKIM ,g w = g(t) if t ∈ V and JtKIM ,g w = I M (t,w) if t ∈ C. If M is given by context, we omit it and write JtKI,g w .

Definition 5. Let M and g be given. Then

M,w ⊨g r(t1, ..., tn) iff (Jt1KI,g w , ..., JtnKI,g w ) ∈ I M (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[x↦→d] ϕ for all d ∈ Dt(x).

M, w ⊨g Ktϕ iff M, v ⊨g ϕ for all v s.t. (w, v) ∈ RM JtKI,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 specific constants to define

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) defines 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.

Definition 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 finite parameter list; (ii) E is a non-empty, finite 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 → (FreeAtoms(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 undefined. dom(post(e)) denotes the set of atoms for which post(e)(r(t1, . . . , tk)) ̸= r(t1, . . . , tk) and is required finite for each e ∈ E, so postconditions are ensured finite objects.

Schema instantiation is defined as follows.

Definition 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, preA, postA) where (i) EA = E (ii) QA(e, e′ ) = Q(e, e′ )σ; (iii) preA(e) = pre(e)σ; (iv) postA(e)(r(t1, . . . , tn)σ) = post(e)(r(t1, . . . , tn))σ if post(e)(r(t1, . . . , tn)) is defined; and postA(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 defined by the operation ⊗ that computes the state s′ = s ⊗ a reached by applying action a in state s. The operation is a first-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 described by a = (A, e). Figure 3 exemplifies the product update of the state from Figure 1 and an instance of the schema in Figure 2.

Definition 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

An action a = (A, e) is applicable in a state s = (M, w) iff (M, w) ⊨g pre(e). Else s ⊗ a is undefined.

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 finite or recursively enumerable set of finite states, A is a finite 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 finite sequence of actions a1, a2, . . . , an such that (1) For all i ≤ n, γ(γ(. . . γ(γ(s0, a1), a2), . . . , ai-1), ai) is defined, and (2) γ(γ(. . . γ(γ(s0, a1), a2), . . . , an-1), an) ∈ SG.

Epistemic planning tasks can be defined as special cases of classical planning tasks.

Definition 9. Let A be a finite 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 finite epistemic state with a finite 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:

• S := {s0 ⊗a1 ⊗ · · · ⊗an | n ∈ N, ai ∈ A}
• SG := {s ∈ S | s ⊨ ϕG}
• γ(s, a) := s ⊗ a if a is applicable in s, else undefined.

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

We follow Aucher and Bolander [2013] in defining the plan existence problem:

Definition 10. Let n ∈ N. PlanEx(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 first-order, term-modal models, we retain the "back" and "forth" conditions of propositional modal logical bisimulation, but replace the "atomic harmony" condition with first-order logical isomorphism. The resulting notion implies modal equivalence and is preserved under product updates. Further, n-bisimulation is defined 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 finitely representable, up to bisimulation. 1

3.1 Isomorphisms, Bisimulations and Equivalence

We first recall the notion of an isomorphism, viewed here as a relationship between worlds in L(Σ) models.

Definition 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,

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:

Definition 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, 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.

1 The existing work on bisimulations for first-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.

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 define n-bisimulations and bisimulation contractions.

Definition 13. For models M and N, let f : DM →DN be a bijection. A non-empty relation Z n 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 Z n-1 f

Forth: If RM d wv then there exists v′ such that RN f(d)w′ v′ and vZ n-1 f v′ , for all d ∈ Dagt,

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

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

Definition 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]↔) = I M (c, w) and I ′ (r, [w]↔) = I M (r, w)

The n-bisimulation contraction M↔n is defined in the same way based on ↔n .

Finally, we fix the relevant notions of logical equivalence:

Definition 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 defined, 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 inM and N respectively, then w ≃f v implies that w and v are elementary equivalent. If M and N have finite 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-finite models if for each world w ∈ W M and each relation RM d , the set {v ∈ W M | RM d wv} is finite. We then establish a variant of the Hennessy-Milner Theorem known from propositional modal logic:

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-finite and with finite 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 I N (t,w′ ) = f(I M (t,w)). Hence, since v was arbitrary and I N (t,w′ ) = f(I M (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 finite 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.

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 definition 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 first-order, edge-conditioned updates.

Proposition 4. For any action (A, e), if (M,w)↔(M ′ ,w′ ), then 1. (M,w) ⊗ (A, e) is defined iff (M ′ ,w′ ) ⊗ (A, e) is, and 2. if defined, 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 wZfw′ . Define Z ′f ⊆ W M⊗A × W M′⊗A by (v, e1)Z ′f (v′ , h1) iff vZfv′ and e1 = h1. Then Z ′f is an f-based bisimulation: Atoms: vZfv′ 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 vZfv′ , vRM d u and M, v ⊨g[x⋆ ↦→d] Q(e1, e2). As vZfv′ , also M ′ , v′ ⊨g[x⋆ ↦→d] Q(e1, e2). As vRM d u and vZfv′ , there is u′ s.t. v′RM′ d u′ and uZfu′ . As (u, e2) ∈ W M⊗A and uZfu′ , 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 defined iff (M ′ , w′ )⊗(A, e) is, and 2. if defined, (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 first 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 finitely many such canonical states. Hence the state space for single-agent planning is finitely representable, and it can therefore be decided whether such task is solvable. We define these canonical states as follows:

Definition 16. Given a signature Σ and a domain D with Dagt = {d}, define the structure M(Σ,D) as the tuple (D,W,W ×W, I) where W is the set of first-order interpretations i of Σ over D and I(x, i) = i(x) for all x ∈ C ∪ R and all i ∈ W. TheM(Σ,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

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

Proof. Define Zf ⊆W ×W ⋆ by vZfv′ 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 vZfv′ 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 finite, by Lemma 1, v ≃f v′ . Forth: Assume that vZfv′ and Rdvu. By definition of M ⋆ , there is a u′ ∈ W ⋆ s.t. ∀x ∈ C ∪ R, I(x, u) = I ⋆ (x, u′ ). By definition of Zf , we have Rdwv and so, by transitivity, that Rdwu. Hence uZfu′ . Finally, as R⋆ d = W ⋆ ×W ⋆ , we have R⋆ d v′u′ . Back: Assume that vZfv′ and R⋆ d v′u′ . By definition of M ⋆ , there is a u ∈ W such that Rdwu and I(x, u) = I ⋆ (x, u′ ), ∀x ∈ C∪R. Hence, uZf u′ . As vZf v′ , by definition, 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 reflexivity, it follows that wZfw⋆ .

Lemma 3. There are only finitely many non-bisimilar singleagent L(Σ) epistemic states with underlying finite 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 finite, there are only finitely many first-order interpretations of Σ over D-i.e., W is finite. Hence M(Σ,D) has finitely many substates.

Theorem1. PlanEx(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-first search of the state space, replacing each visited epistemic state by its M(Σ,D) substate. By Lemma 3, this state space is finite.

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, PlanEx(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 finite (up to bisimulation). We fix some lemmas.

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

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

Yu et al. [2013] showed that the number of ↔n equivalence classes of Kripke model has a fixed finite bound that depends on n, generalizing a result from Visser [1996]. We show a similar result for first-order models.

Lemma 5. Let M be an L(Σ) model with finite 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 PlanEx(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-first 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 finite.

5 Final Remarks

FODEL combines the higher-order expressiveness of DEL with the first-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].