Paper deep dive
An Undecidability Proof for the Plan Existence Problem
Antonis Achilleos
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 99%
Last extracted: 4/27/2026, 4:10:46 AM
Summary
The paper proves that the plan existence problem in Epistemic Planning (EP) is undecidable, even when epistemic actions are restricted to having no postconditions and preconditions with a modal depth of at most 1. The proof utilizes a reduction from the Post's Correspondence Problem (PCP). The author demonstrates that this undecidability holds for both single-agent cases (specifically for modal logic K and certain extensions like KTB/KT4 without negative introspection) and multi-agent scenarios. The reduction involves constructing epistemic states that encode sequences of blocks from a PCP instance and using epistemic actions to either add blocks or verify matches by pruning the sequence.
Entities (7)
Relation Signals (4)
Plan Existence Problem → isundecidablein → Modal Logic K
confidence 100% · We prove that the plan existence problem with preconditions of modal depth at most 1 and no postcondition, is undecidable.
Plan Existence Problem → reducesfrom → Post's Correspondence Problem
confidence 100% · Our proof is by a reduction from Post's Correspondence Problem (PCP) [11].
Epistemic Action → transforms → Epistemic State
confidence 100% · Finally, an epistemic action transforms an epistemic state, by affecting the beliefs of the agents...
Epistemic Planning → uses → Kripke Model
confidence 100% · The state of the world (including the beliefs or knowledge of the agents) is represented by an epistemic state, which is a pointed Kripke model.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:The plan existence problem asks, given a goal in the form of a formula in modal logic, an initial epistemic state (a pointed Kripke model), and a set of epistemic actions, whether there exists a sequence of actions that can be applied to reach the goal. We prove that even in the case where the preconditions of the epistemic actions have modal depth at most 1, and there are no postconditions, the plan existence problem is undecidable. The (un)decidability of this problem was previously unknown.
Tags
Links
- Source: https://arxiv.org/abs/2604.22736v1
- Canonical: https://arxiv.org/abs/2604.22736v1
Trouble viewing inline? Open PDF directly →
Full Text
72,545 characters extracted from source content.
Expand or collapse full text
An Undecidability Proof for the Plan Existence Problem Antonis Achilleos# Department of Computer Science, Reykjavik University, Iceland Abstract The plan existence problem asks, given a goal in the form of a formula in modal logic, an initial epistemic state (a pointed Kripke model) and a set of epistemic actions, whether there exists a sequence of actions that can be applied to reach the goal. We prove that even in the case where the preconditions of the epistemic actions have modal depth at most 1, and there are no postconditions, the plan existence problem is undecidable. The (un)decidability of this problem was previously unknown. 2012 ACM Subject Classification Theory of computation→Automated reasoning; Theory of computation → Modal and temporal logics Keywords and phrases Epistemic Planning, Modal Logic, Undecidability Digital Object Identifier 10.4230/LIPIcs... 1 Introduction In the field of Epistemic Planning (EP) [2,4], we seek to construct a plan, that is, a sequence of actions that achieve a given goal. EP is an approach based on dynamic epistemic logic [6] that extends classical planning [8] by incorporating the beliefs and knowledge of multiple agents, allowing for the modeling of complex interactions such as coordination, communication, and secrecy. As expected, in EP, the goal is typically epistemic, in that it involves statements regarding the belief or knowledge of one or multiple agents, and it is expressed with a formula from a multi-agent epistemic logic. The state of the world (including the beliefs or knowledge of the agents) is represented by an epistemic state, which is a pointed Kripke model. Finally, an epistemic action transforms an epistemic state, by affecting the beliefs of the agents, and possibly also the values of the propositional atoms. The agents may be uncertain about the epistemic actions, and therefore these are represented as pointed Kripke frames, where each state is called an event. Each event is further equipped with preconditions, i.e. epistemic formulas that describe when the event can be applied to a world of the epistemic state; and with postconditions that describe how the propositions of a world change value when the event is applied to that world (see [4] for a more comprehensive description of EP). Thus, a central problem in EP is the plan existence problem: given an initial epistemic state, a goal, and a set of epistemic actions, is there a plan (a sequence of epistemic actions from the given ones) that transforms the initial epistemic state into one that satisfies the goal? The plan existence problem is generally undecidable [3]. Furthermore, it remains so when epistemic actions are restricted to having no postconditions and preconditions of modal depth at most 2 [5]; and to having preconditions of modal depth at most 1 and propositional postconditions [4,10]. On the other hand, it is known that plan existence is decidable when both preconditions and postconditions are propositional [1,7,14]. The case of preconditions of modal depth 1 and no postconditions, to the best of our knowledge, remains open to this day. © Author: Please provide a copyright holder; licensed under Creative Commons License C-BY 4.0 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany arXiv:2604.22736v1 [cs.LO] 24 Apr 2026 X:2 An Undecidability Proof for the Plan Existence Problem Our contribution We prove that the plan existence problem with preconditions of modal depth at most 1 and no postcondition [4], is undecidable. Our proof is by a reduction from Post’s Correspondence Problem (PCP) [11]. We prove that the problem is undecidable in the case of at least two agents without any assumptions on the modal logic that the agents’ beliefs are based on. For the single-agent case, we need to distinguish between two cases. If the agent’s knowledge behaves according to logic S5, or even if the agent has negative introspection (they know what they do not know), then it is a somewhat straightforward observation that the plan existence problem is decidable. When the agent does not have negative introspection, we consider agents based on a modal logic that extends the basic logic K with axiomsT,B,4, but not bothBand 4, as these imply negative introspection. For these cases, we prove that the plan existence problem is undecidable. Our reduction makes substantial use of the fact that successive applications of epistemic actions can construct long paths with starting and ending states definable by a formula of modal depth 1. We need this property, as we cannot use postconditions to cycle through the states of an encoded machine, nor general preconditions to access the status of worlds further away. Thus, our constructions need to operate in a local manner, having events with preconditions that depend on the immediately accessible worlds. In Section 2, we give the necessary background on epistemic logic and epistemic planning. In Section 3, we prove the undecidability of the plan existence problem for a single agent based on modal logic K. This case is likely not particularly realistic for planning situations, or general, but it is sufficiently simple to help us demonstrate our reduction method. In Section 4, we extend our reduction to the case of multiple agents, and in Section 5 we show how to further adjust our reduction to the case of agents based on logics KTB and KT4, and therefore on any logic between K and KTB, KT4. We conclude in Section 7 and give a straightforward decidability result for a single agent with negative introspection. 2 Background Modal formulae extend propositional logic with a set of modal operatorsK i ,i∈ Ag, often interpreted as asserting an agenti’s knowledge or belief of the statement it is applied on. We use a set of propositional variablesPrpthat can be assumed to be finite or countably infinite. The set of modal formulae is given by the following grammar: φ ::=⊥| p|¬φ| φ∧ φ| K i φ, wherep∈ Prpandi∈ ag. We use the usual definitions for the dual operators of the language: ⊤ :=¬⊥; φ 1 ∨ φ 2 :=¬(¬φ 1 ∧¬φ 2 ); and ̄ Kφ :=¬K¬φ. A Kripke model is a triple (W,R,V), whereWis a set of states (or worlds), representing different possibilities about reality;R= (R i ) i∈Ag , whereR i ⊆ W 2 is an accessibility relation, where (w,w ′ )∈ R i represents that at statew, agenticonsidersw ′ a possible reality; and V:W →2 Prp labels each state with a set of propositional variables, with the intended meaning that these are the variables that are true at that state. We usually writewR i w ′ instead of (w,w ′ )∈ R i . The pair (W,R) is a Kripke frame. An epistemic state, also known as a pointed model, is a pair (M,w), whereM= (W,R,V) is a Kripke model andw ∈ W— it can also be written as a quadruple (W,R,V,w). We interpret modal formulae on epistemic states. LetM= (W,R,V) be a Kriple model and A. AchilleosXX:3 w ∈ W. Then we define |= between epistemic states and formulae in the following way. (M,w)̸|=⊥ (M,w)|= pif and only ifp∈ V (w) (M,w)|=¬φif and only if(M,w)̸|= φ (M,w)|= φ 1 ∧ φ 2 if and only if(M,w)|= φ 1 and (M,w)|= φ 2 (M,w)|= K i φif and only if(M,w ′ )|= φ for every wR i w ′ . In the case where|Ag|= 1, we writeKφinstead ofK i φ, andR=R i . For each epistemic states= (M,w) = (W,R,V,w) andu ∈ W, we use (s,u) to denote the epistemic state (M,u). An epistemic action is a pair (A,e), whereA= (E,Q, pre), (E,Q) is a Kripke frame, e ∈ E, andpre:E →L maps each element ofEto a modal formula. Elements ofE are called events and for each eventf,pre(f) is called the precondition off. We restrict ourselves to preconditions of modal depth at most 1, that is, for eachf ∈ E,pre(f) does not have any nested modal operators. We say that an epistemic action (A,e) applies to an epistemic state (M,w), where A= (E,Q, pre) andM= (W,R,V), when (M,w)|=pre(e). In that case, we define the application of (A,e) to (M,w), and we denote it as (M,w)×(A,e) = ((W ′ ,R ′ ,V ′ ),(w,e)), where W ′ =(u,f )∈ W × E | (M,u)|= pre(f ); R ′ i =((u 1 ,f 1 ), (u 2 ,f 2 ))∈ W ′2 | (u 1 ,u 2 )∈ R i and (f 1 ,f 2 )∈ Q i ; and V ′ (u,f ) =V (u) for every (u,f )∈ W ′ . We can recursively extend the definition of the application of an epistemic action to an epistemic state for sequences of actions: ifαis a sequence of epistemic actions,sis an epistemic state,s×αis well-defined, andais an epistemic action that applies tos×α, then s× αa = (s× α)× a. We now define our (constrained) version of the plan existence problem. ▶ Definition 2.1 (Plan Existence Problem). Given: an initial epistemic state s I ; a goalφ G , which describes the desired knowledge or belief conditions to be achieved; and a set of epistemic actionsAct, where each action has preconditions of modal depth at most 1, the Plan Existence Problem asks whether there exists a plan, i.e. a sequence of actions α = a 1 a 2 ·a m ∈ Act ∗ , such that s I × α is defined and s I × α|= Φ G . ▶ Remark 2.2. Typically (e.g. [2,4]), the plan existence problem is defined more generally, allowing preconditions of arbitrary modal depth and postconditions that allow an event to change the values of propositional variables. Here, we restrict our attention to the case of no postconditions and preconditions of modal depth at most 1, as this suffices to prove undecidability. We observe that if two epistemic statess 1 ,s 2 are bisimilar (s 1 ∼ s 2 ), then for every epistemic actionα,s 1 ×α∼ s 2 ×α. Therefore, plans and plan existence are preserved under bisimulation, and, for convenience we will often identify epistemic states with their bisimilar states. X:4 An Undecidability Proof for the Plan Existence Problem Frame conditions The semantics we have given for modal formulas correspond to the simplest modal logic K n onnagents. By imposing restrictions on the accessibility relations for the frames that we allow, the resulting semantics correspond to modal logics with different behaviours — that is, each of the frame properties that we examine corresponds to a specific modal axiom. The relationship between frame conditions and modal axioms is a well-studied phenomenon called correspondence theory (see, for example, [12,13]). In this paper, we consider the following typical properties of the accessibility relations: reflexivitycorresponds to the factivity axiom:K i φ→ φand is usually required when the operator K i corresponds to knowledge; transitivity corresponds to positive introspection: K i φ→ K i K i φ; symmetrycorresponds to the axiomφ → K i ̄ K i φand usually results from the Eucledian property (below) and reflexivity; the Eucledian property corresponds to negative introspection: ¬K i φ→ K i ¬K i φ. Post’s Correspondence Problem and the Reduction Plan To prove that the plan existence problem is undecidable, we reduce from Post’s Correspond- ence Problem (PCP) [11], a well-known undecidable problem. ▶Definition 2.3 (Post’s Correspondence Problem (PCP), [11]:). Givenn≥1 andB= a i b i | 1≤ i≤ n, where for every i≤ n, a i ,b i ∈0, 1 ∗ , the Post’s Correspondence Problem asks whether there exists a non-empty sequence of indices i 1 ,i 2 ,...,i k such that: a i 1 a i 2 ...a i k = b i 1 b i 2 ...b i k . Such a sequence is called a match for B. Letn ≥1 andB= a i b i |1≤ i ≤ n, where for everyi ≤ n,a i ,b i ∈ 0,1 ∗ . The following sections demonstrate howBcan be turned into an instance of the plan existence problem, such that B has a match if and only if that instance has a plan. The overall idea is that a plan constructs a sequence of epistemic states in two stages. In the first stage, the application of the epistemic actions represents adding blocks to a sequence of blocks from B, which is encoded as two branching paths of the epistemic state, one representing the top of the sequence, and the second the bottom of the sequence. In the second stage, the application of the epistemic states verifies that the resulting sequence is a match, by iteratively removing one symbol from the end of the sequence — i.e. by removing the last state from each path, if these match. If both branches can eventually be pruned to the root, the plan has succeeded in finding a match. We first give the reduction for the case of a single agent with no restrictions on the accessibility relations. This case allows us to demonstrate our method in a clear setting; we then adjust our construction for the cases of multiagent logics with any set of frame conditions; and to single-agent logics with frame conditions that may include reflexivity, symmetry, or transitivity, but not both symmetry and transitivity. 3 The Plan Existence Problem is Undecidable for Single-agentK We now show how to reduce PCP to the plan existence problem for the case when the accessibility relations have no restrictions and there is only one agent. LetEP= (s I , Act,Φ G ), which we define in the following. A. AchilleosXX:5 w root w stg1 w empty w a w b w 0,a w 1,a w ntF w lp w 0,b w 1b w end Figure 1 The initial epistemic states I . The designated statew root is marked with an arrow pointing to it. We used dashed arrows to the auxiliary statesw end , w ntF in this and in other figures, to emphasize the part of the model that encodes a sequence of blocks and uses solid arrows. We use the following set of propositional variables: Prp =0, 1, a, b, root, stg1, empty, end, ntF, lp. 3.1 The Epistemic States The initial epistemic state s I = ((W 0 ,R 0 ,V 0 ),w root ), where W 0 =w p ,w bt,x | p∈ Prp\0, 1, bt∈0, 1,x∈a, b; R 0 =(w root ,w empty ), (w root ,w stg1 ), (w root ,w x ), (w x ,w bt,x ), (w x ,w end ), (w x ,w ntF ), (w bt,x ,w ntF ), (w bt,x ,w end ), (w bt,x ,w lp ), (w 0,x ,w bt,x ), (w 1,x ,w bt )| x∈a, b, bt∈0, 1; and for everyp ∈ Prp \ 0,1andx ∈ a,b,V 0 (w p ) =p,V 0 (w 0,x ) =0,x, and V 0 (w 1,x ) =1,x. ▶Remark 3.1. The reader will likely realise while going through the constructions in the paper, that we could use simpler and smaller epistemic states. The ones we use, however, will help shorten and simplify some of our upcoming arguments, which we consider a significant gain. Intuitively, a plan is split into two stages, and the epistemic actions are split into three kinds. The first kind is applied during the first stage, and each action amounts to adding a block fromBat the end of the block sequence; the second kind consists of one action, which signals the transition from the first stage to the second stage by removing state w stg1 or its analogous in the current model; and the third kind is applied during the second stage to iteratively delete matching symbols from the end of the constructed block sequence. X:6 An Undecidability Proof for the Plan Existence Problem w root w a w b w a,1 w b,1 w a,2 w b,2 w a,|q a | w b,|q b | w ntF Figure 2 The epistemic state s q a q b . The statesw empty ,w stg1 ,w end ,w ntF can be thought of as auxiliary, as they are used to keep track of useful information about the states of an epistemic state. As we apply actions to the epistemic states, in a state, the truth of ̄ Kempty encodes that we have applied no actions (and the state is the root state); ̄ Kstg1 encodes that we are on the first stage of the plan; ̄ Kend encodes that we are at a state at the end of the encoding of the blocks; and ̄ KntF encodes that the plan has not attempted to remove the wrong symbol from the state during the second stage — i.e., the plan has not failed yet. ▶Definition 3.2. Letq a ,q b ∈0,1 ∗ . We define the epistemic states q a q b to be (any epistemic state bisimilar to) the epistemic state s q a q b = ((W q a q b ,R q a q b ,V q a q b ),w root ), where W q a q b =w p ,w x | p∈root, a, b, ntF, x∈a, b∪ w x,j | x∈a, b and 1≤ j ≤|q x |; R q a q b =(w root ,w x ), (w x ,w ntF )| x∈a, b ∪ (w x ,w x,1 ), (w x,|q x | ,w ntF )| x∈a, b, 1≤|q x | ∪ (w x,j ,w x,j+1 ), (w x,j ,w ntF ) | x∈a, b, 1≤ j <|q x |; and for everyp ∈ root,a,b, ntF,V(w p ) =p, and for everyx ∈ a,band 1≤ j ≤ |q x |, V (w x,j ) =q x [j]. The epistemic states q a q b is used to encode a sequence of blocks fromBwhose top parts formq a and bottom parts formq b ; it is illustrated in Figure 2. We also use the epistemic states q a q b 0,1defined below, to encode the same sequences of blocks, while also retaining a loop of states that allows the plan to add more blocks to the sequence. ▶Definition 3.3. Letq 1 ,q 2 ∈ 0,1 ∗ . We define the epistemic states q a q b 0,1to be s q a q b 0, 1 = ((W ′ q a q b ,R ′ q a q b ,V ′ q a q b ),w root ), where W ′ q a q b = W q a q b ∪w stg1 ,w 0,x ,w 1,x ,w end ,w lp | x∈a, b; R ′ q a q b = R q a q b ∪(w root ,w stg1 ), (w 0,x ,w 1,x ), (w 1,x ,w 0,x ), (w 0,x ,w 0,x ), (w 1,x ,w 1,x ), (w 0,x ,w ntF ), (w 1,x ,w ntF ), (w 0,x ,w end ), (w 1,x ,w end ), (w 0,x ,w lp ), (w 1,x ,w lp )| x∈a, b ∪(w x,|q x | ,w bt,x ), (w x,|q x | ,w end )| x∈a, b, q x ̸= ε, bt∈0, 1 ∪(w x ,w bt,x ), (w x ,w end )| x∈a, b, q x = ε, bt∈0, 1; and for everyw ∈ W q a q b ,V ′ q a q b (w) =V q a q b , forp ∈ stg1, end, lp,V ′ q a q b (w p ) =p, and for p∈0, 1 and x∈a, b, V ′ q a q b (w p,x ) =p,x. A. AchilleosXX:7 w root w stg1 w a w b w a,1 w b,1 w a,2 w b,2 w a,|q a | w b,|q b | w 0,a w 1,a w 0,b w 1,b w end w ntF w lp Figure 3 The epistemic state s q a q b 0, 1. Observe that s I ̸= s ε ε 0, 1, as state w empty is absent from s ε ε 0, 1. As we will see, a successful plan will generate a sequence of epistemic states of the form s q a q b 0, 1 or s q a q b . 3.2 The Epistemic Actions We now proceed to define the epistemic actions that we use. We use the following shorthand formulas: symb = 0∨ 1,tail = (a∨ b)∧ K¬symb last = ̄ Kend∧ K¬lp,failed = (a∨ b)∧ K¬ntF, and loop x = x∧ ̄ Klp, for every x∈a, b. Note that the states ins q a q b 0,1that satisfyloop x are exactlyw 0,x ,w 1,x . The states that satisfylastarew x,|q x | , ifq x ̸=ε, andw x , ifq x =ε, wherex ∈ a,b. The states in s q a q b that satisfytailare exactlyw x,|q x | , ifq x ̸=ε, andw x , ifq x =ε. No state ins q a q b or s q a q b 0,1satisfiesfailed, which will be used to mark a state that witnesses that the plan has failed (see Lemma 3.17). X:8 An Undecidability Proof for the Plan Existence Problem e s e st e a e b e a,lst e b,lst e a,1 e b,1 e a,|a i | e b,|b i | e 01,a e 01,b e end root∧ ̄ Kstg1 stg1 a∧¬last b∧¬last a∧ last b∧ last a i [1]∧ loop a b i [1]∧ loop b a i [|a i |]∧ loop a b i [|b i |]∧ loop b loop a ∨ lp loop b ∨ lp end Figure 4 The epistemic actionadd i , where the designated event,e s is marked with an arrow. Each event’s precondition appears next to the event. To avoid overloading the figure, we omit event e ntF . 3.2.1 Adding Blocks For every 1≤ i≤ n, we define add i = (AD i ,e s ), where AD i = (E i ,R i , pre), E i =e s ,e x ,e x,lst ,e st ,e end ,e ntF ,e 01,x |x∈a, b ∪ e x,j |x∈a, b, 0 < j ≤|x i |; R i =(e s ,e st ), (e s ,e x ), (e s ,e x,lst ), (e x ,e x ), (e x ,e ntF ), (e x ,e x,lst ), (e x,lst ,e ntF ), (e 01,x ,e 01,x ), (e 01,x ,e end ), (e 01,x ,e ntF )|x∈a, b ∪ (e x,lst ,e x,1 ), (e x,j ,e ntF ), (e x,|x i | ,e end )|x∈a, b, 0 < j ≤|x i | (e x,j ,e x,j+1 )|x∈a, b, 0 < j <|x i | ∪ (e x,lst ,e 01,x ), (e x,lst ,e end )|x∈a, b, |x i | = 0; and the precondition for each event in E i is given below: pre(e s ) = root∧ ̄ Kstg1pre(e st ) = stg1 pre(e x ) = x∧¬lastpre(e x,lst ) = x∧ last pre(e ntF ) = ntFpre(e x,j ) = x i [j]∧ loop x pre(e end ) =endpre(e 01,x ) =loop x ∨ lp, for each x∈a, b and j ≤|x i |. Actionadd i corresponds to adding a block at the end of a sequence of blocks. The precondition ofe s ensures that ̄ Kstg1is true at the epistemic state, and therefore we are still in the first stage. The action is illustrated in Figure 4. A. AchilleosXX:9 ▶ Lemma 3.4. Let 1≤ i≤ n. Then, s I × add i = s ε ε 0, 1× add i . Proof. Observe thats ε ε 0,1is identical tos I except that it lacks statew empty . Since there is not any event in add i whose precondition is satisfied at w empty , the lemma follows. ◀ ▶ Lemma 3.5. Let s = s q a q b 0, 1 and 1≤ i≤ n. Then, s× add i = s q a a i q b b i 0, 1. Proof. Let ((W,R,V),(w root ,e s )) =s× add i . We show thats× add i ∼ s q a a i q b b i 0,1. For simplicity, we refer to all accessibility relations as R. LetW 1 =w root ,w stg1 ,w ntF ,w end ,w x | x∈a,b∪w x,j | x∈a,b,0< j ≤|q x |; and let W 2 (x) =w bt,x ,w lp . We note that W q a q b = W 1 ∪ W 2 . LetE 1 =e s ,e st ,e ntF ,e end ,e x ,e x,lst | x ∈ a,b;E 2 (x) =e x,j |0< j ≤ |x i |; and E 3 (x) =e 01,x . E 1 ,E 2 (a),E 2 (b),E 3 (a),E 3 (b) partition E i . We observe that for every w ∈ W q a q b and e∈ E i : 1. if w |= pre(e) and e∈ E 1 , then w ∈ W 1 ; 2. if w |= pre(e) and e∈ E 2 (x), then w ∈ W 2 (x) (specifically, w = w 0,x or w = w 1,x ); 3. if w |= pre(e) and e∈ E 3 (x), then w ∈ W 2 (x). 4. ifw ∈ W 1 , then there exists a uniquee(w)∈ E, such thatw |=pre(e(w)), and furthermore, pre(w)∈ E 1 for every w ∈ W 1 ; 5. if e∈ E 2 (x), then there exists a unique w(e)|= pre(e), and furthermore, w(e)∈ W 2 (x); 6. if w ∈ W 2 (x) and e∈ E 3 (x), then w |= pre(e). LetWE 1 =(w,e(w))| w ∈ W 1 ;WE 2 (x) =(w(e),e)| e ∈ E 2 (x); andWE 3 (x) = W 2 (x)× E 3 (x). From items 1, 2, 3, we see that the states ofs× add i are exactlyWE 1 ∪ WE 2 (a)∪ WE 2 (b)∪ WE 3 (a)∪ WE 3 (b). It is not hard to observe that (s× add i | WE 1 , (w,e(w))∼(s| W 1 ,w ) for everyw ∈ W 1 (the two structures are actually isomorphic through the projection relation). But then, s| W 1 = s q a a i q b b i 0, 1| W 1 , so (s× add i | WE 1 , (w,e(w))∼ (s q a a i q b b i 0, 1| W 1 ,w). We also see that for every (w(e x,j ),e x,j )∈ WE 2 (x), (s× add i | WE 2 (x) , (w(e x,j ),e x,j ))∼ (s q a a i q b b i 0, 1| w x,|q x |+h |0<h≤|x i | ,w x,|q x |+j ). Let w × (e x,j ) = w x,|q x |+j for each e x,j ∈ E 2 (x). Finally, (s× add i | WE 3 (x) , (w,e 01,x )))∼ (s| W 2 (x) ,w) = (s q a a i q b b i 0, 1| W 2 (x) ,w) for every w ∈ W 2 (x). LetR=((w,e(w)),w)| w ∈ W 1 ∪((w(e),e),w × (e))| e ∈ E 2 (x), x ∈ a,b∪ ((w,e 01,x ),w)| w ∈ W 2 (x), x∈a, b. To verify thatRis a bisimulation relation, from the above, it suffices to verify the accessibility pairs that cross between the setsWE 1 ,WE 2 (a),WE 2 (b),WE 3 (a),WE 3 (b) on s×add i , and the accessibility pairs that cross between the setsW 1 ,W 2 (a),W 2 (b),w x,|q x |+h | 0< h ≤ |x i |ons q a a i q b b i 0,1. But these are few and easy to verify. Observe thatRis a function. Let(w, e(w))∈ W E 1 .From the above, we have that (w,e(w))Rw. If (w,e(w))R(u,v)/∈ WE 1 , thenwRu /∈ W 1 andw ∈ W 1 , sou=w bt,x for somex ∈ a,bandbt ∈ 0,1. Then,e(w) =e x,lst andv=e x,1 orv=e 01,x . In the first case, (u,v)Rw x,|q x |+1 and X:10 An Undecidability Proof for the Plan Existence Problem e nx Figure 5 The epistemic action nxt_stg corresponds to moving the plan to the second stage. w=w x,|q x | Rw x,|q x |+1 ins q a a i q b b i 0,1; in the second case, (u,v)Ru,x i =ε, andwRuin s q a a i q b b i 0, 1 (as in s q a q b 0, 1). On the other hand, ifwRu /∈ W 1 ins q a a i q b b i , thenu=w bt,x andx i =ε, for some x ∈ a,bandbt ∈ 0,1; oru=w x,|q x |+1 for somex ∈ a,b. In the first case, let (u ′ ,v ′ ) = (w bt,x ,e 01,x ); in the second case, let (u ′ ,v ′ ) = (w(e x,1 ),e x,1 ). In both cases, it is not hard to see that (w,e(w))R(u ′ ,v ′ )Ru. Let(w(e), e)∈ W E 2 (x).From the above, we have that (w,e(w))Rw × (e). If (w(e),e)R(u,v)/∈ WE 2 (x), then: 1. e=e x,|x i | ,w(e) =w 01,x , and (u,v) = (w 01,x ,e 01,x )Ru, in which case we also have w × = w x,|q x |+|x i | Ru in s q a a i q b b i 0, 1; or 2. (u,v) = (w p ,e p ), where p∈end, ntF, in which case we also have that w × (e)Ru and (u,v)Ru. On the other hand, if w × (e)Ru /∈ WE 2 (x), then either 1. u =w 01,x , in which casew × =w x,|q x |+|x i | ,e=e x,|x i | , andw(e) =w 01,x , so let v = e 01,x , and therefore, (w(e),e)R(u,v) = (w 01,x ,e 01,x )Ru; or 2. u =w p , wherep∈end, ntF, in which case let (u,v) = (w p ,e p ), so we also have that (w(e),e)R(u,v)Ru. Let(w, e 01,x )∈ W E 3 (x).From the above, we have that (w,e 01,x )Rw. If (w,e 01,x )R(u,v)/∈ WE 3 (x), then it can only be the case that (u,v) = (w p ,e p ), wherep ∈ end, ntF, and therefore, we have thatwRuand (u,v)Ru. Similarly, ifwRu /∈ W 2 (x), then it can only be the case thatu=w p , wherep∈end, ntF, in which case let (u,v) = (w p ,e p ), so we also have that (w,e 01,x )R(u,v)Ru. We can conclude thatRis a bisimulation, and therefore the proof of the lemma is complete.◀ ▶ Corollary 3.6. Letα=add i 1 add i 2 · add i k ∈ add i |1≤ i ≤ n ∗ . Then,s I × α= s a i 1 a i 2 ·a i k b i 1 b i 2 ·b i k 0, 1. 3.2.2 Moving to the Second Stage We define epistemic action nxt_stg = (e nx ,(e nx ,e nx ),e nx ), where pre(e nx ) = (K¬empty∧ ̄ Kstg1)∨ ((a∨ b)∧ K¬lp)∨ ntF Actionnxt_stgremoves the statesw stg1 ,w end ,w 0 (x),w 1 (x),w lp froms q a q b 0,1, initiating the second stage of the plan. ▶ Lemma 3.7. Let s = s q a q b 0, 1. Then, s× nxt_stg = s q a q b . Proof.Simply observe that the states left ins q a q b are exactly the ones that satisfy the precondition of e nx . ◀ A. AchilleosXX:11 Similarly, it is straightforward to see that the following lemma holds. ▶Lemma 3.8. Letsbe an epistemic state wherenxt_stgapplies. Then,s× nxt_stg |= K¬stg1. We call the epistemic states of the forms I × α, whereα∈add i |1≤ i≤ n ∗ , first-stage states. ▶Lemma 3.9. Letsbe an epistemic state,fan epistemic action, andKφan epistemic formula of modal depth 1. If s|= Kφ, then s× f |= Kφ. Proof. Lets= ((W,R,V),w) andf= (E,R ′ ,e). It suffices to prove that for everywRw ′ and eR ′ e ′ , (s× f,(w ′ ,e ′ ))|=φ. Butφis propositional and therefore, (s× f,(w ′ ,e ′ ))|=φif and only if ((W,R,V),w ′ )|=φ. The fact thatwRw ′ ands|=Kφyield that ((W,R,V),w ′ )|=φ and the proof is complete. ◀ ▶ Lemma 3.10. For every epistemic statesandi≤ n, neitheradd i nornxt_stgapply to s×nxt_stg. Furthermore, ifadd i (andnxt_stg) does not apply tos, then for every epistemic action f that applies to s, neither add i nor nxt_stg apply to s× f. Proof. Observe thatadd i does not apply to an epistemic states ′ if and only ifs ′ |=K¬stg1. Furthermore, by Lemma 3.8,s× nxt_stg|=K¬stg1, which implies the first statement. The second statement is a consequence of Lemma 3.9. ◀ ▶Corollary 3.11. Lets=s I × α, whereαis a sequence of epistemic actions that includes nxt_stg. Then, neither nxt_stg nor add i apply to s. Therefore, epistemic actionnxt_stgcan only be applied once in a plan, and it marks the end of the applications of the actions add i . 3.2.3 Verifying one Symbol at Each Step Finally, for each bt∈0, 1, we define the epistemic action rmv bt = (E bt ,R bt ,e bt ), where E bt =e bt ,e bt ntF ,e bt fail ; R bt =(e bt ,e bt ), (e bt ,e bt fail ), (e bt ,e bt ntF ); pre(e bt ) =(root∧ K¬stg1)∨ ((a∨ b)∧¬tail); pre(e bt fail ) =(tail∧¬bt)∨ failed; and pre(e bt ntF ) =ntF. For eachbt ∈ 0,1,rmv bt only activates during the second stage and if the epistemic state is of the right form, i.e.s q a bt q b bt , the resulting state iss q a q b . If the epistemic state is not of the right form, thene bt fail activates and ensures that a last state can no longer accessw ntF , thus marking the plan as a failed one. ▶Lemma 3.12. Letsbe an epistemic state wherermv bt applies. Then, neitheradd i nor nxt_stg applies to s. Proof. The lemma results from the observation that the precondition ofe bt is consistent with neither of the preconditions for e s and e nx . ◀ X:12 An Undecidability Proof for the Plan Existence Problem e bt e bt fail e bt ntF (root∧ K¬stg1)∨ ((a∨ b)∧¬tail) (tail∧¬bt)∨ failed ntF Figure 6 The epistemic actionrmv bt corresponds to removing the bitbtfrom the end of the encoding. ▶ Lemma 3.13. Let q a ,q b ̸= ε and let s = s q a bt q b bt . Then, s× rmv bt = s q a q b . Proof.We first observe that the precondition ofe bt fail is not satisfied by any state ins q a bt q b bt ; therefore,e bt fail does not activate in the product update. Furthermore, the precondition of e bt ntF is satisfied byw ntF only. Finally, every other state ins q a bt q b bt , except forw ntF ,w a,|q a |+1 , w b,|q b |+1 , satisfies the precondition ofe bt . Let ((W,R,V),(w root ,e bt s )) =s× rmv bt . We show that s× rmv bt ∼ s q a q b . Let R = (w root ,e bt ),w root , (w x ,e bt ),w x , (w x,j ,e bt ),w x,j , (w ntF ,e ntF ),w ntF | 0 < j ≤|q x |, x∈a, b It is now straightforward to verify thatRis a bisimulation — in fact,Ris an isomorphism between the two models. ◀ ▶Definition 3.14. Lets= ((W,R,V),s 0 ) be an epistemic state. We say thatsis a failed state when there is a sequence of states s 0 Rs 1 R·Rs k , where k ≥ 1, such that: 1. ((W,R,V ),s 0 )|= root∧ K¬stg1; 2. ((W,R,V ),s 1 )|= x for some x∈a, b; 3. ((W,R,V ),s i )|= symb for every 2≤ i≤ k; and 4. ((W,R,V ),s k )|= failed. A failed state is the result of applyingrmv bt to an epistemic state that is not of the form s q a bt q b bt . In that case, the actionrmv bt marks that it failed to remove that last bit from (at least) one of the state’s branches. Furthermore, as the following Lemma 3.15 demonstrates, once an epistemic state has been marked as a failed one, it will remain marked as such throughout the application of the plan. ▶ Lemma 3.15. If rmv bt applies to epistemic state s, and s = s q a q b and q a = ε or q b = ε; s = s q a bt ′ q b or s = s q a q b bt ′ , and bt ′ ̸= bt; or s is a failed state; then s× rmv bt is a failed state. Proof.We prove the lemma for the case wheres=s q a bt ′ q b , as the other cases are similar. There exist some statesw root =r 0 R w a =r 1 R · R r k =w a,|q a |+1 ins. We then have that in s: 1. r 0 |= root∧ K¬stg1; A. AchilleosXX:13 2. r 1 |= a; 3. r i |= symb for every 2≤ i≤ k; and 4. r k |= tail∧ bt ′ in s. It is also straightforward to see that for each 0< i < k,r i |=¬tail. Therefore, it is not hard to see that s× rmv bt contains the sequence of states (r 0 ,e bt ) R (r 1 ,e bt ) R · R (r k ,e bt fail ) that satisfy the conditions in Definition 3.14 for s× rmv bt to be a failed state. ◀ ▶Corollary 3.16. Letαbe a plan (a sequence of epistemic actions) that applies to epistemic state s I . Then, α is of the form add i 1 add i 2 · add i k or add i 1 add i 2 · add i k nxt_stg rmv bt 1 rmv bt 2 · rmv bt l . Proof. The corollary is a consequence of Lemmas 3.5, 3.8, 3.12, 3.13 and 3.15. ◀ 3.3 Completing the Reduction Plan To complete the definition of EP, let Act =add i , nxt_stg, rmv bt | 1≤ i≤ n and bt∈0, 1, and Φ G =K¬empty∧ K (tail∧¬failed). ▶ Lemma 3.17. Let s be a failed epistemic state. Then, s̸|= Φ G . Proof. A consequence of the definitions of a failed state (Definition 3.14) and of Φ G . ◀ ▶ Lemma 3.18. Letq a ,q b ∈0,1 ∗ and letrm=rmv bt l rmv bt l−1 · rmv bt 1 . Ifs q a q b × rm| = Φ G , then q a = q b = bt 1 bt 2 · bt l . Proof.We proceed by induction onl. Ifrm=ε, thens q a q b =s q a q b ×rm| =Φ G , and therefore, q a =q b =ε. Ifrm=rmv bt 1 rm ′ , then, by Lemmas 3.13 and 3.15, eithers q a q b × rmv bt 1 is a failed state, or it iss q ′ a q ′ b , whereq a =q ′ a bt l andq b =q ′ b bt l . The first case results in a contradiction, due to Lemmas 3.15 and 3.17. We conclude the proof by the inductive hypothesis on l− 1. ◀ We can conclude with our main theorem. ▶ Theorem 3.19. B has a match if and only if EP has a plan. Proof. To prove the first direction, leti 1 ,i 2 ,...,i k be a match forB. Letm 1 m 2 ·m ℓ = a 1 a 2 ·a k = b 1 b 2 ·b k , where for every 1≤ i≤ ℓ, m i ∈0, 1. Let add m = add i 1 add i 2 · add i k ; rmv m = rmv m ℓ · rmv m 1 ; and α = add m nxt_stg rmv m . We now demonstrate that α is a plan that applies to s I and that s I × α|= Φ G . By Corollary 3.6,s I × add m =s m 1 m 2 ·m ℓ m 1 m 2 ·m ℓ 0,1; then, Lemma 3.7 yields thats I × add m nxt_stg=s m 1 m 2 ·m ℓ m 1 m 2 ·m ℓ 0,1× nxt_stg=s m 1 m 2 ·m ℓ m 1 m 2 ·m ℓ ; and finally, Lemma 3.13 yields that s I × α = s m 1 m 2 ·m ℓ m 1 m 2 ·m ℓ × rmv m = s ε ε |= φ G . X:14 An Undecidability Proof for the Plan Existence Problem For the converse direction, letαbe a plan that applies tos I , such thats I × α|=Φ G . By Corollary 3.16, α is of the form add i 1 add i 2 · add i k or add i 1 add i 2 · add i k nxt_stg rmv bt l rmv bt l−1 · rmv bt 1 . Ifαis of the formadd i 1 add i 2 · add i k , thens I × α=s a i 1 ·a i k b i 1 ·b i k 0,1̸|=Φ G , contradicting our assumptions. Therefore, α is of the form add i 1 add i 2 · add i k nxt_stg rmv bt l rmv bt l−1 · rmv bt 1 . We prove thati 1 ,i 2 ,...,i k is a match forB. Letm 1 m 2 ·m ℓ =a 1 a 2 ·a k andm ′ 1 m ′ 2 ·m ′ ℓ ′ = b 1 b 2 ·b k . By Corollary 3.6,s I × add i 1 add i 2 · add i k =s m 1 m 2 ·m ℓ m ′ 1 m 2 ·m ℓ ′ 0,1; then, Lemma 3.7 yields that s I × add i 1 add i 2 · add i k nxt_stg = s m 1 m 2 ·m ℓ m ′ 1 m ′ 2 ·m ′ ℓ ′ 0, 1, #× nxt_stg = s m 1 m 2 ·m ℓ m ′ 1 m ′ 2 ·m ′ ℓ ′ . Finally, by Lemma 3.18, we conclude thata 1 a 2 ·a k =m 1 m 2 ·m ℓ =m ′ 1 m ′ 2 ·m ′ ℓ ′ = b 1 b 2 ·b k , and therefore i 1 ,i 2 ,...,i k is a match for B. ◀ ▶Corollary 3.20. The plan existence problem for arbitrary frames is undecidable, even for the case of a single agent. 4 The Case of Multiple Agents For the case of multiple agents, regardless of the constraints on the accessibility relations, we can similarly prove that the plan existence problem is undecidable. To adjust our reduction, in our construction we alternate between the accessibility relations of two agents, 1 and 2, to avoid any side-effects due to the constraints on the accessibility relations, and to give direction to our models when symmetric accessibility relations do not. For the sake of simplicity, we assume that 1 and 2 are the only agents and that accessibility relations are equivalence relations, but the arguments are the same for any number of agents, and for more relaxed accessibility relation conditions. We follow the same approach as in Section 3, though we note that due to the requirements that the accessibility relations are symmetric and transitive, simply closing the epistemic states and actions with respect to symmetry and transitivity would have unintended consequences, as some states — for example, statesw ntF andw end — are accessible from multiple states that should not be connected. Therefore, we will use multiple copies of these states to avoid unintended connections. We note that in the case of accessibility relations with no closure conditions, we can ensure that statesw ntF andw end have no accessible states, and therefore keeping one or multiple copies of these results in bisimilar models. However, when the accessibility relation is an equivalence relation, that is no longer the case. We modify the definition of the epistemic states and actions in the following way. We use an additional propositional variable # that acts as a separator symbol between two bits in a block, ensuring an even number of transitions between two bit states. The initial state is relatively simple — the epistemic actions will ensure to unfold the epistemic states and alternate the accessibility relations from agent 1 to agent 2 and back. A. AchilleosXX:15 w root w stg1 w empty w a w b w 0 (a) w 1 (a) w # (a) w end (a)w ntF (a) w 0 (b) w 1 (b) w # (b) w end (b)w ntF (b) Figure 7 Initial state for the two-agent case. The dashed rectangles represent the equivalence classes of the accessibility relation for agent 1, and the solid ones represents the equivalence classes for agent 2. If a state is not contained in any rectangle, it means that it forms its own equivalence class. As illustrated in Figure 7, the initial epistemic states I = ((W 0 ,(R 1 0 ,R 2 0 ),V 0 ),w root ), where W 0 =w p | p∈root, empty, stg1, a, b∪w p (x)| p∈0, 1, #, ntF, end, x∈a, b; R 1 0 =w root ,w empty ,w stg1 ,w a ,w b 2 ∪w 0 (a),w 1 (a),w # (a),w ntF (a),w end (a) 2 ∪w 0 (b),w 1 (b),w # (b),w ntF (b),w end (b) 2 ; R 2 0 =w a ,w 0 (a),w 1 (a),w # (a),w ntF (a),w end (a) 2 ∪w b ,w 0 (b),w 1 (b),w # (b),w ntF (b),w end (b) 2 ∪w root 2 ∪w empty 2 ∪w stg1 2 and for everyp∈root, empty, stg1,a,b,V 0 (w p ) =p; and for everyp∈0,1,#, end, ntF and x∈a, b, V 0 (w p (x)) =p,x. In this multi-agent case, as we apply actions to the epistemic states, in a state, the truth of root∧ ̄ K 1 emptyencodes that we have applied no actions (and the state is the root state); root∧ ̄ K 1 stg1 encodes that we are on the first stage of the plan; #∧ ̄ K 2 endencodes that we are at a state at the end of the encoding of the blocks (or at w # ); and ok_state= ((0∨1)∧ ̄ K 1 ntF)∨((a∨b)∧¬0∧¬1∧ ̄ K 2 ntF) encodes that the plan has not attempted to remove the wrong symbol from the state during the second stage. As the reader notices, we are more explicit in the multiagent case, to avoid side-effects due to the constraints on the accessibility relations. ▶Definition 4.1. Letq a ,q b ∈ 0,1 ∗ . We define the epistemic states q a q b to bes q a q b = X:16 An Undecidability Proof for the Plan Existence Problem ((W q a q b , (R 1 q a q b ,R 2 q a q b ),V q a q b ),w root ), where W q a q b =w root ,w a ,w b ,w ntF (a),w ntF (b)∪ w x,j ,w x,j,# ,w ntF (x,j),w ntF (x,j, #),| x∈a, b and 1≤ j ≤|q x |; R 1 q a q b =w root ,w x | x∈a, b 2 ∪ [ x∈a,b 1≤j≤|q x | w x,j ,w x,j,# ,w ntF (x,j) 2 R 2 q a q b = [ x∈a,b (w x ,w ntF (x)∪w x,1 | q x ̸= ε) 2 ∪ [ x∈a,b 1≤j<|q x | w x,j,# ,w x,j+1 ,w ntF (x,j, #) 2 ∪ [ x∈a,b q x ̸=ε w x,|q x |,# ,w ntF (x,|q x |, #) 2 ; and for everyx ∈ a,b,V(w root ) =root,V(w x ) =xandV(w ntF (x)) =ntF,x, and for every 1≤ j ≤ |q x |,V(w x,j ) =q x [j],x,V(w x,j,# ) =#,x, andV(w ntF (x,j)) = V (w ntF (x,j, #)) =ntF,x. We then defines q a q b −# to be the submodel ofs q a q b induced byW q a q b \w a,|q a |,# ,w b,|q b |,# , as in Section 3. The definition of the epistemic states q a q b 0,1,#can similarly be adjusted from Section 3 (see Figure 8). ▶ Definition 4.2. Let q a ,q b ∈0, 1 ∗ and let Tl q x = ( w 0 (x),w 1 (x),w # (x),w ntF (x,|q x |, #),w end (x), if q x ̸= ε; w 0 (x),w 1 (x),w # (x),w ntF (x),w end (x),if q x = ε; for x∈a, b. We define the epistemic states q a q b 0,1,#= ((W ′ q a q b ,(R ′ 1 q a q b ,R ′ 2 q a q b ),V ′ q a q b ),w root ), where W ′ q a q b =W q a q b ∪ w stg1 ∪ Tl q a ∪ Tl q b ; R ′ 1 q a q b =R 1 q a q b ∪ w root ,w stg1 ,w a ,w b 2 ∪ Tl 2 q a ∪ Tl 2 q b R ′ 2 q a q b =R 2 q a q b ∪ w stg1 2 ∪ [ x∈a,b (Tl q x ∪w x,|q x |,# | q x ̸= ε∪w x | q x = ε) 2 ; for everywinW q a q b ,V ′ q a q b (w) =V q a q b (w),V ′ q a q b (w stg1 ) =stg1, and for everyp ∈ 0, 1, #, end and x∈a, b, V ′ q a q b (w p (x)) =p,x. 4.1 The Epistemic Actions We redefine our shorthand formulas: ag1 = root∨ 0∨ 1,ag2 = (a∨ b)∧¬(0∨ 1∨ ntF∨ end), symb = 0∨ 1∨ #,last = ag2∧ ̄ K 2 end, tail(i) = agi∧ K i ¬ag(3− i), for every i∈1, 2. We now define the epistemic actions that we use. A. AchilleosXX:17 w root w stg1 w a w b w a,1 w a,1,# · w a,|q a | w a,|q a |,# w end w 0 w 1 w # w ntF w end w 0 w 1 w # w ntF w ntF w ntF w ntF w ntF Figure 8 The epistemic states q a q b 0,1,#for the case whereq a ̸=εandq b =ε. Dashed lines represent the equivalence classes for agent 1, while solid lines represent the equivalence classes for agent 2. We omit marking the singleton equivalence classes. We write w p instead of w p (· ). 4.1.1 Adding Blocks For every 1≤ i≤ n, we define add i = (E i , (R 1 ,R 2 ),e s ), where E i =e s ,e a ,e b ,e st ,e a ,e b, ,e a,lst ,e b,lst ,e ε a ,e ε b ,e asmb ,e bsmb , e x,lst ntF ,e a,1 ntF ,e b,1 ntF ,e a,2 ntF ,e b,2 ntF ∪e x,j ,e x,j,# ,e ntF (x,j)| x∈a, b, 0 < j ≤|x i | ∪e ntF (x,j, #)| x∈a, b, 0 < j <|x i |; R 1 =e s ,e st ,e a ,e b ,e ε a ,e ε b 2 ∪e asmb ,e a,lst 2 ∪e bsmb ,e b,lst 2 ∪ [ x∈a,b 0<j≤|x i | e x,j ,e x,j,# ,e ntF (x,j) 2 ∪ [ x∈a,b 0<j<|x i | e ntF (x,j, #) 2 ∪e x,lst ntF 2 ∪e a,1 ntF 2 ∪e a,2 ntF 2 ∪e b,1 ntF 2 ∪e b,2 ntF 2 ∪e a, 2 ∪e b, 2 ; R 2 =e a ,e ntF (a),e a,smb 2 ∪e b ,e ntF (b),e b,smb 2 ∪ (e ε a ,e a,lst ,e a,2 ntF ,e a,lst ntF ∪e a,1 | a i ̸= ε∪e a, | a i = ε) 2 ∪ (e ε b ,e b,lst ,e b,2 ntF ,e b,lst ntF ∪e b,1 | b i ̸= ε∪e b, | b i = ε) 2 ∪ [ x∈a,b 0<j<|x i | (e x,j+1 ,e x,j,# ,e ntF (x,j, #) 2 ∪e x,|x i |,# ,e x, 2 ) ∪e s 2 ∪e st 2 ∪ [ x∈a,b 0<j≤|x i | e ntF (x,j) 2 ; X:18 An Undecidability Proof for the Plan Existence Problem e s e a e st e asmb e b e bsmb e ε a e ε b e a,lst e b,lst e a,1 e b,1 e a,1,# e b,1,# · · e a,|a i | e b,|b i | e a,|a i |,# e b,|b i |,# e a,2 ntF e b,2 ntF e a,lst ntF e b,lst ntF e ntF e ntF e ntF e ntF e ntF e ntF e a, e b, e a,1 ntF e b,1 ntF Figure 9 The epistemic actionadd i for the case when a i , b i ̸ =ε. The designated event,e s , is marked with an arrow. and the precondition for each event in E i is given below: pre(e s ) = root∧ ̄ K 1 stg1 pre(e st ) = stg1 pre(e x ) = x∧ ag2∧¬#∧¬last pre(e x,lst ) = x∧ #∧ last∧ K 1 ¬end pre(e ε x ) = x∧ ag2∧¬#∧ last∧ K 1 ¬end pre(e x,1 ntF ) = pre(e x,2 ntF ) = x∧ ntF∧ K 1 ¬end pre(e x,lst ntF ) = x∧ ntF∧ ̄ K 1 end pre(e x,smb ) = x∧ symb∧¬last pre(e x, ) = x∧ ̄ K 1 end∧ (symb∨ ntF∨ end) pre(e ntF (x,j)) = pre(e ntF (x,j, #)) = x∧ ntF∧ ̄ K 1 end pre(e x,j ) = x∧ x i [j]∧ ̄ K 1 end pre(e x,j,# ) = x∧ #∧ ̄ K 1 end, for each x∈a, b and j ≤|x i |. The action add i is illustrated in Figure 9. ▶ Lemma 4.3. Let s = s q a q b 0, 1, # and 1≤ i≤ n. Then, s× add i = s q a a i q b b i 0, 1, #. Proof. Let ((W,(R 1 ,R 2 ),V),(w root ,e s )) =s×add i . We show thats×add i ∼ s q a a i q b b i 0,1,#. For simplicity, we refer to all accessibility relations as (R 1 ,R 2 ). The set of states ins× add i A. AchilleosXX:19 is: (w root ,e s ), (w stg1 ,e st ) ∪(w end (x),e x, ), (w 0 (x),e x, ), (w 1 (x),e x, ), (w # (x),e x, ), | x∈a, b ∪(w ntF (x),e x, )| x∈a, b, q x = x i = ε ∪(w ntF (x,|q x |, #),e x, )| x∈a, b, q x ̸= ε ∪(w x ,e ε x )| x∈a, b, q x = ε ∪(w ntF (x),e x,lst ntF )| x∈a, b, q x = ε ∪(w x ,e x ), (w ntF (x),e x,1 ntF ), (w x,j ,e x,smb ), (w ntF (x,j),e x,1 ntF ), (w x,|q x |,# ,e x,lst ), (w ntF (x,|q x |, #),e x,lst ntF )| x∈a, b, 0 < j ≤|q x | ∪(w x,j,# ,e x,smb ), (w ntF (x,j, #),e x,2 ntF )| x∈a, b, 0 < j <|q x | ∪(w x i [h] ,e x,h ), (w # (x),e x,h,# )| x∈a, b, 0 < h≤|x i | ∪(w ntF (x,|q x |, #),e ntF (x,h, #)) | x∈a, b, 0 < h <|x i |, q x ̸= ε ∪(w ntF (x),e ntF (x,h, #))| x∈a, b, 0 < h <|x i |, q x = ε. To see this, observe that for every eventeand statew ∈ W q a q b , ifw |=pre(e), then (w,e) appears above. We split our epistemic actions and epistemic states into parts. Let E 1 =e s ,e a ,e b ,e st ,e a,lst ,e b,lst ,e ε a ,e ε b ,e asmb ,e bsmb ,e x,lst ntF ,e a,1 ntF ,e b,1 ntF ,e a,2 ntF ,e b,2 ntF ∪e 1 x | x∈a, b, x i ̸= ε∪e x, | x∈a, b, x i = ε; E 2 =e x,j ,e x,j,# ,e ntF (x,j),| x∈a, b, 0 < j ≤|x i | ∪e ntF (x,j, #)| x∈a, b, 0 < j <|x i |; and E 3 =e x | x∈a, b∪e x,|x i |,# | x∈a, b, x i ̸= ε We observe that the states ofs× add i ands q a a i q b b i 0,1,#can similarly be arranged into corresponding parts. Let W 1 =w root ,w a ,w b ,w ntF (a),w ntF (b)∪ w x,j ,w x,j,# ,w ntF (x,j),| x∈a, b and 1≤ j ≤|q x |∪ w ntF (x,j, #),| x∈a, b and 1≤ j <|q x | ∪w x i [1] (x)| x∈a, b, x i ̸= ε∪ [ x i =ε Tl q x ; W 2 (x) =Tl q x ; W ′ 2 (x) =Tl q x x i ∪w x,|x i |,# | x∈a, b, x i ̸= ε; and W 3 (x) =w x,j ,w x,j,# ,w ntF (x,j),| x∈a, b and |q x | < j ≤|q x | +|x i |∪ w ntF (x,j, #),| x∈a, b and |q x | < j <|q x | +|x i |. X:20 An Undecidability Proof for the Plan Existence Problem We consider the pairs of generated submodels on the respective restrictions ofs× add i and s q a a i q b b i 0, 1, # on: 1. W 1 × E 1 and W 1 ; 2. W 2 (x)× E 2 and W 3 (x); 3. W 2 (x)× E 3 and W ′ 2 (x). These sets cover all states — and more importantly, all accessibility relation pairs — of the respective models. We will prove that the above pairs are bisimilar. Then, it is not hard to see that, since these sets cover all states and accessibility relation pairs, the complete epistemic states are also bisimilar. In the first case, observe that each state w ∈ W 1 satisfies exactly one precondition from the ones ofE 1 . Lete(w)∈ E 1 , such thats,w |=pre(e(w)). Furthermore, we see that for everyw 1 ,w 2 ∈ W 1 , ifw 1 R j w 2 , we also have thate(w 1 )R j e(w 2 ); therefore, it is immediate that (s× add i | W 1 ×E 1 , (w,e(w)))∼ (s| W 1 ,w) = (s q a a i q b b i 0, 1, #| W 1 ,w), for every w ∈ W 1 . In the second case, we observe thatW 2 (x) is a clique for both accessibility relations, and for eache ∈ E 2 , there is a uniquew(e)∈ W 2 (x) such thats,w(e)|=pre(e) (and w(−) is surjective onW 2 (x)). For eache x,j ,e x,j,# ,e ntF (x,j)∈ E 2 , letw × (e x,j ) =w x,|q x |+j ; w × (e x,j,# ) =w x,|q x |+j,# ; andw × (e ntF (x,j)) =w ntF (x,j). And for eache ntF (x,j)∈ E 2 , let w × (e ntF (x,j, #)) = w ntF (x,j, #). It is then, not hard to see that (s× add i | W 2 (x)×E 2 , (w(e),e))∼ (s q a a i q b b i 0, 1, #| W 3 (x) ,w × (e)), for every e∈ E 2 . Finally, for the third case, letE ′ 3 =E 3 \e x,|x i |,# . AsE ′ 3 includes a single event whose precondition is satisfied in all of W 2 (x), it is not hard to see that (s× add i | W 2 (x)×E ′ 3 , (w,e x, ))∼ (s| W 2 (x) ,w)∼ (s q a a i q b b i 0, 1, #| Tl q x x i ,w + ), where ifq x =ε,x i ̸=ε, andw=w ntF (x), thenw + =w ntF (x,|x i |,#); ifq x ̸=ε,x i ̸=ε, and w=w ntF (x,|q x |,#), thenw + =w ntF (x,|q x |+|x i |,#); and otherwise,w + =w. The only interesting case is whenq x =εandx i ̸=ε, but then it suffices to observe thatw ntF (x) and w ntF (x,|x i |,#) are bisimilar. Then, after reintroducing (w # (x),e x,|x i |,# ) andw x,|x i |,# , we observe that (s× add i | W 2 (x)×E 3 , (w,e x, ))∼ (s q a a i q b b i 0, 1, #| Tl q x x i W ′ 2 (x) ,w + ), and (s× add i | W 2 (x)×E 3 , (w # (x),e x,|x i |,# )∼ (s q a a i q b b i 0, 1, #| Tl q x x i W ′ 2 (x) ,w x,|x i |,# ). This completes the proof, as we can easily construct a bisimulation betweens× add i and s q a a i q b b i 0,1,#by taking the union of the three bisimilarity relations between the respective submodels. As the bisimilarity relation is a bisimulation and every accessibility relation appears in at least one submodel, all bisimulation conditions are satisfied. ◀ ▶ Corollary 4.4. Letα=add i 1 add i 2 · add i k ∈ add i |1≤ i ≤ n ∗ . Then,s 0 × α= s a i 1 a i 2 ·a i k b i 1 b i 2 ·b i k 0, 1, #. A. AchilleosXX:21 e nx (¬root∨ (K 1 ¬empty∧ ̄ K 1 stg1))∧¬stg1∧¬( ̄ K 1 0∧ ̄ K 1 1)∨ ntF Figure 10 next stage 4.1.2 Moving to the Second Stage In the multi-agent case, we define the define epistemic action nxt_stg = (e nx , ((e nx ,e nx ),(e nx ,e nx )),e nx ), where pre(e nx ) = (¬root∨ (K 1 ¬empty∧ ̄ K 1 stg1))∧ stg1∧¬( ̄ K 1 0∧ ̄ K 1 1)∨ ntF Actionnxt_stgremovesw stg1 ,w end ,w 0 (a),w 1 (a),w # (a),w 0 (b),w 1 (b),w # (b), initiating the second stage. ▶ Lemma 4.5. Let s = s q a q b 0, 1, #. Then, s× next_stage = s q a q b . Proof. Simply observe that the states that do not satisfypre(e nx ) insare exactlyw stg1 , w end , w 0 (a), w 1 (a), w # (a), w 0 (b), w 1 (b), w # (b). ◀ Similarly, it is straightforward to see that the following lemma holds. ▶Lemma 4.6. Letsbe an epistemic state wherenext_stageapplies. Then,s×next_stage|= K 1 ¬stg1. We call the epistemic states of the forms 0 ×α, whereα∈add i |1≤ i≤ n ∗ , first-stage states. ▶Lemma 4.7. Letsbe an epistemic state,fan epistemic action, andK i φan epistemic formula of modal depth 1. If s|= K i φ, then s× f |= K i φ. Proof. The reasoning is the same as in the proof of Lemma 3.9. ◀ ▶ Lemma 4.8. For every epistemic statesandi ≤ n, neitheradd i nornxt_stgapply to s× nxt_stg. Furthermore, ifadd i andnxt_stgdo not apply tos, then for every epistemic action f that applies to s, neither add i nor nxt_stg apply to s× f. Proof. Observe thatadd i does not apply to an epistemic states ′ if and only ifs ′ |=K 1 ¬stg1. Furthermore, by Lemma 4.6,s× nxt_stg|=K 1 ¬stg1, which implies the first statement. The second statement is a consequence of Lemma 4.7. ◀ ▶ Corollary 4.9. Lets=s I × α, whereαis a sequence of epistemic actions that includes nxt_stg. Then, neither nxt_stg nor add i apply to s. Therefore, epistemic actionnxt_stgcan only be applied once in a plan, and it marks the end of the applications of the actions add i . 4.1.3 Verifying one Symbol at Each Step Finally, for each bt∈0, 1, #, we define the epistemic action rmv bt = (e bt , ((e bt ,e bt ),(e bt ,e bt )),e bt ), where X:22 An Undecidability Proof for the Plan Existence Problem pre(e bt ) =(root∧ K 1 ¬stg1)∨ ntF∧ _ i=1,2 ( ̄ K i ag1∧ ̄ K i ag2) ∨ _ i=1,2 (agi∧¬(tail(i)∧ bt∧ ̄ K i ntF)). For eachbt∈0,1,#,rmv bt only activates during the second stage and if the epistemic state is of the right form, i.e.s q a bt q b bt , the resulting state iss q a q b . If the epistemic state is not of the right form, thenpre(e bt ) ensures that a last state can no longer accessw ntF , thus marking this attempt as a failed one. ▶ Lemma 4.10. Letsbe an epistemic state. It cannot be the case thatrmv bt applies tos and so does add i or nxt_stg. Proof.The lemma results from the observation that the precondition ofe bt is consistent with neither of the preconditions for e s and e nx . ◀ ▶ Lemma 4.11. Let q a ,q b ̸= ε. 1. Let s = s q a q b . Then, s× rmv # = s q a q b − #. 2. Let s = s q a bt q b bt − #. Then, s× rmv bt = s q a q b . Proof. For both statements, it suffices to observe that the states that do not satisfypre(e bt ) insare exactlyw x,|q x |,# andw ntF (x,|q x |,#) for statement 1, andw x,|q x | andw ntF (x,|q x |) for statement 2, where x∈a, b. ◀ Lets= ((W,R,V),s 0 ) be an epistemic state. We say thatsis a failed state when there is a sequence of statess 0 R 1 s 1 R 2 ·R j s k , wherej= 1 ifkis odd andj= 2 ifkis even, such thatk ≥1; ((W,R,V),s 0 )|=root∧ K 1 ¬stg1; ((W,R,V),s 1 )|=xfor somex ∈ a,b; for each 0< i < kandj ∈ 1,2, if ((W,R,V),s i )|=agj, then ((W,R,V),s i+1 )|=ag(3− j); and ((W,R,V ),s k )|= bt∧ K¬ntF for some bt∈a, b, 0, 1, #. ▶ Lemma 4.12. If rmv bt applies to epistemic state s, and s = s q a q b and bt̸= # or q a = ε or q b = ε; s = s q a bt ′ q b − # or s = s q a q b bt ′ − # and bt ′ ̸= bt; or s is a failed state; then s× rmv bt is a failed state. Proof.We prove the lemma for the case wheres=s q a bt ′ q b − #, as the other cases are similar. There exist some statesw root =r 0 R 1 w a =r 1 R 2 · R i r k =w a,|q a |+1 ins, such thatw a,|q a |+1 |=tail∧ bt ′ ins, and for each 0< i < kandj ∈ 1,2, ifr i |=agj, then r i+1 |=ag(3−j). Sincermv bt applies tos,r 0 |=pre(e bt ); furthermore, it is not hard to verify that for every 0< i≤ k,r i |=pre(e bt ); and thatw ntF (a,|q a |,#)̸|=pre(e bt ). Therefore, there exists a sequence of states (r 0 ,e bt ) R 1 (r 1 ,e bt ) R 2 · R i (r k ,e bt ) in s× rmv bt that satisfies the conditions for a failed state. ◀ ▶ Corollary 4.13. Letαbe a plan (a sequence of epistemic actions) that applies to epistemic state s I . Then, α is of the form add i 1 add i 2 · add i k or add i 1 add i 2 · add i k nxt_stg rmv bt 1 rmv bt 2 · rmv bt l . A. AchilleosXX:23 Proof. The corollary is a consequence of Lemmas 3.5, 3.13, 4.6 and 4.12 and Corollary 4.9.◀ To complete the definition of EP, let Act =add i , nxt_stg,remove bt | 1≤ i≤ n and bt∈0, 1, #, and Φ G = K 1 ¬empty∧ K 1 (¬(a∨ b)∨ (tail(2)∧ ̄ K 2 ntF)). ▶ Lemma 4.14. Let s be a failed epistemic state. Then, s̸|= Φ G . Proof. A consequence of the definition of a failed state and of Φ G . ◀ ▶ Lemma 4.15. Letq a ,q b ∈0,1 ∗ and letrm=rmv bt 1 rmv bt 2 · rmv bt l . Ifs q a q b ×rm|=Φ G , then q a = q b and rm = rmv # rmv q a [|q a |] rmv # rmv q a [|q a |−1] · rmv # rmv q a [1] . Proof. We proceed by induction onrm. Ifrm=ε, thens q a q b =s q a q b × rm |=Φ G , and therefore,q a =q b =ε. Ifrm=rmv bt 1 rm ′ , then, by Lemmas 3.13 and 4.12, either s q a q b × rmv bt 1 is a failed state, or it iss q a q b − #, whereq a ,q b ̸=εandbt 1 = #. The first case results in a contradiction, due to Lemmas 4.12 and 4.14. Ifrm ′ =ε, thens q a q b ×rm =s q a q b − #̸|=Φ G , which contradicts the lemma’s assumptions. Therefore,rm ′ =rmv bt 2 rm ′ . Using similar reasoning as above,q a =q ′ a bt 2 andq b =q ′ b bt 2 . We conclude the proof by the inductive hypothesis on rm ′ . ◀ We can conclude with our main theorem. ▶ Theorem 4.16. B has a match if and only if EP has a plan. Proof.To prove the first direction, leti 1 ,i 2 ,...,i k be a match forB. Letm 1 m 2 ·m ℓ = a 1 a 2 ·a k = b 1 b 2 ·b k , where for every 1≤ i≤ ℓ, m i ∈0, 1. Let add m = add i 1 add i 2 · add i k ; rmv m = rmv # rmv m ℓ rmv # · rmv # rmv m 1 ; and α = add m nxt_stg rmv m . We now demonstrate that α is a plan that applies to s I and that s I × α|= Φ G . By Corollary 4.4, s I × add m = s m 1 m 2 ·m ℓ m 1 m 2 ·m ℓ 0, 1, #; then, Lemma 4.5 yields that s I × add m nxt_stg = s m 1 m 2 ·m ℓ m 1 m 2 ·m ℓ 0, 1, #× nxt_stg = s m 1 m 2 ·m ℓ m 1 m 2 ·m ℓ ; and finally, Lemma 3.13 yields that s I × α = s m 1 m 2 ·m ℓ m 1 m 2 ·m ℓ × rmv m = s ε ε |= φ G . For the converse direction, letαbe a plan that applies tos I , such thats I × α|=Φ G . By Corollary 4.13, α is of the form add i 1 add i 2 · add i k or add i 1 add i 2 · add i k nxt_stg rmv bt 1 rmv bt 2 · rmv bt l . Ifαis of the formadd i 1 add i 2 · add i k , thens I × α=s a i 1 ·a i k b i 1 ·b i k ̸| =Φ G , contradicting our assumptions. Therefore, α is of the form add i 1 add i 2 · add i k nxt_stg rmv bt 1 rmv bt 2 · rmv bt l . X:24 An Undecidability Proof for the Plan Existence Problem We prove thati 1 ,i 2 ,...,i k is a match forB. Letm 1 m 2 ·m ℓ =a 1 a 2 ·a k andm ′ 1 m ′ 2 ·m ′ ℓ ′ = b 1 b 2 ·b k . By Corollary 3.6,s I ×add i 1 add i 2 · add i k =s m 1 m 2 ·m ℓ m ′ 1 m 2 ·m ℓ ′ 0,1,#; then, Lemma 3.7 yields that s I × add i 1 add i 2 · add i k nxt_stg = s m 1 m 2 ·m ℓ m ′ 1 m ′ 2 ·m ′ ℓ ′ 0, 1, #× nxt_stg = s m 1 m 2 ·m ℓ m ′ 1 m ′ 2 ·m ′ ℓ ′ . Finally, by Lemma 4.15, we conclude thata 1 a 2 ·a k =m 1 m 2 ·m ℓ =m ′ 1 m ′ 2 ·m ′ ℓ ′ = b 1 b 2 ·b k , and therefore i 1 ,i 2 ,...,i k is a match for B. ◀ 5 A Single Agent with Reflexivity or Symmetry We now proceed to adjust our reduction to the case of a single agent with an accessibility relation that is reflexive or symmetric — but not transitive. In fact, we will give a construction using accessibility relations that are both reflexive and symmetric. We use the following set of propositional variables: Prp =0, 1, # 1 , # 2 , a, b, root, stg1, empty, end, ntF, lp. Instead of one separator symbol as in the multi-agent case, we use two (# 1 and # 2 ) to help give the epistemic states an orientation, which we need for our encoding to work as intended. 5.1 The Epistemic States The initial epistemic state s I = ((W 0 ,R 0 ,V 0 ),w root ), where W 0 =w p | p∈root, empty, stg1, a, b, lp ∪w p (x)| p∈0, 1, # 1 , # 2 , ntF, end, x∈a, b; R 0 is the reflexive and symmetric closure of: R − 0 =(w root ,w empty ), (w root ,w stg1 ), (w root ,w x ), (w x ,w bt (x)), (w bt (x),w # 1 (x)), (w # 1 (x),w # 2 (x)), (w # 2 (x),w bt (x)), (w # 2 (x),w end (x)), (w x ,w end (x)), (w x ,w ntF (x)), (w bt (x),w ntF (x)), (w # 1 (x),w ntF (x)), (w # 2 (x),w ntF (x)), (w bt (x),w lp ), (w # 1 (x),w lp ), (w # 2 (x),w lp )| x∈a, b, bt∈0, 1; and for everyw p ,w p ′ (x)∈ W 0 ,V 0 (w p ) =pandV 0 (w p ′ (x)) =p ′ ,x. The epistemic state s I is illustrated in Figure 11. ▶ Definition 5.1. Letq a ,q b ∈0,1 ∗ . We define the epistemic states q a q b to be the epistemic A. AchilleosXX:25 w root w stg1 w empty w a w b w 0 w 1 w # 1 w # 2 w end w ntF w 0 w 1 w # 1 w # 2 w end w ntF w lp Figure 11 The initial epistemic states I for the case of a single agent with a reflexive and symmetric accessibility relation. We do not draw self-loops, but every state is accessible from itself. We use arcs instead of arrows, as the accessibility relation is (reflexive and) symmetric. state s q a q b = ((W q a q b ,R q a q b ,V q a q b ),w root ), where W q a q b =w p ,w x ,w ntF (x)| p∈root, a, b, x∈a, b ∪ w x,j ,w x,j,# 1 ,w x,j,# 2 | x∈a, b and 1≤ j ≤|q x |; R q a q b is the reflexive, symmetric closure of (w root ,w x ), (w x ,w ntF (x))| x∈a, b ∪ (w x ,w x,1 ), (w x,j ,w x,j,# 1 ), (w x,j,# 1 ,w x,j,# 2 ), (w x,j ,w ntF ), (w x,j,# 1 ,w ntF ), (w x,j,# 2 ,w ntF )| x∈a, b, 1≤ j ≤|q x | ∪ (w x,j,# 2 ,w x,j+1 )| x∈a, b, 1≤ j <|q x |; and for everyx ∈ a,bandw p ∈ W q a q b ,V(w p ) =p,V(w ntF (x)) =ntF,x, and for every 1≤ j ≤|q x |, V (w x,j ) =q x [j],x, V (w x,j,# 1 ) =# 1 ,x, and V (w x,j,# 2 ) =# 2 ,x. We also define two variations ofs q a q b that encodes the same block but without the last separator or pair of separators. ▶Definition 5.2. Letq a ,q b ∈ 0,1 ∗ . We define the epistemic statess q a q b −# 2 and s q a q b −# 1 to be the submodels ofs q a q b induced respectively byW q a q b \w a,|q a |,# 2 ,w b,|q b |,# 2 and by W q a q b \w a,|q a |,# 1 ,w b,|q b |,# 1 ,w a,|q a |,# 2 ,w b,|q b |,# 2 . ▶ Definition 5.3. Letq 1 ,q 2 ∈ 0,1 ∗ . We define the epistemic states q a q b 0,1,#to be X:26 An Undecidability Proof for the Plan Existence Problem w root w a w b w a,1 w b,1 w a,1,# 1 w b,1,# 1 w a,1,# 2 w b,1,# 2 w a,|q a | w b,|q b | w a,|q a |,# 1 w b,|q b |,# 1 w a,|q a |,# 2 w b,|q b |,# 2 w ntF w ntF Figure 12 The epistemic state s q a q b . The state w ntF appears twice for clarity. s q a q b 0, 1, # = ((W ′ q a q b ,R ′ q a q b ,V ′ q a q b ),w root ), where W ′ q a q b = W q a q b ∪ w stg1 ,w 0 (x),w 1 (x),w # 1 (x),w # 2 (x),w lp | x∈a, b; R ′ q a q b = R q a q b ∪ (w root ,w stg1 ), (w stg1 ,w root ), (w 0 (x),w # 1 (x)), (w 1 (x),w # 1 (x)), (w # 1 (x),w 0 (x)), (w # 1 (x),w 1 (x)), (w # 1 (x),w # 2 (x)), (w # 2 (x),w # 1 (x)), (w # 2 (x),w 0 (x)), (w # 2 (x),w 1 (x)), (w 0 (x),w # 2 (x)), (w 1 (x),w # 2 (x)), (w 0 (x),w ntF (x)), (w 1 (x),w ntF (x)), (w # 1 (x),w ntF (x)), (w # 2 (x),w ntF (x)), (w ntF (x),w 0 (x)), (w ntF (x),w 1 (x)), (w ntF (x),w # 1 (x)), (w ntF (x),w # 2 (x))| x∈a, b ∪ (w x,|q x |,# 2 ,w bt (x)), (w bt (x),w x,|q x |,# 2 )| x∈a, b, q x ̸= ε, bt∈0, 1 ∪ (w x ,w bt (x)), (w bt (x),w x )| x∈a, b, q x = ε, bt∈0, 1 ∪ (w,w)| w ∈w stg1 ,w 0 (x),w 1 (x),w # 1 (x),w # 2 (x),w lp | x∈a, b ∪ (w,w lp ), (w lp ,w)| w ∈w 0 (x),w 1 (x),w # 1 (x),w # 2 (x)| x∈a, b; and for everyw ∈ W q a q b ,V ′ q a q b (w) =V q a q b ,V ′ q a q b (w stg1 ) =stg1, and forp∈lp,0,1, # 1 , # 2 and x∈a, b, V ′ q a q b (w p (x)) =p,x. A. AchilleosXX:27 w root w stg1 w a w b w a,1 w b,1 w a,1,# 1 w b,1,# 1 w a,1,# 2 w b,1,# 2 w a,|q a | w b,|q b | w a,|q a |,# 1 w b,|q b |,# 1 w a,|q a |,# 2 w b,|q b |,# 2 w 0 w 1 w # 1 w # 2 w end w 0 w 1 w # 1 w # 2 w end w ntF w ntF w lp Figure 13 The epistemic state s q a q b 0, 1, #. 5.2 The Epistemic Actions We use the following shorthand formulas: nxt(0) = nxt(1) = # 1 ,nxt(a) = nxt(b) = nxt(# 2 ) = 0∨ 1, nxt(# 1 ) = # 2 ,symb = 0∨ 1∨ # 1 ∨ # 2 , last = ̄ Kend∧ K¬lp,loop x = x∧ ̄ Klp, and tail = (a∨ b)∧ (¬symb∧ K¬nxt(a))∨ _ d∈0,1,# 1 ,# 2 (d∧ K¬nxt(d)) , for every x∈a, b. We now adjust the epistemic actions that add blocks to the encoding of a sequence of blocks. X:28 An Undecidability Proof for the Plan Existence Problem For every 1≤ i≤ n, we define add i = (E i ,R i ,e s ), where E i =e s ,e x ,e x,lst ,e st ,e end ,e ntF ,e 01,x |x∈a, b ∪e x,j ,e x,j,# 1 ,e x,j,# 2 |x∈a, b, 0 < j ≤|x i |; R i is the reflexive, symmetric closure of R − i =(e s ,e st ), (e s ,e x ), (e s ,e x,lst ), (e x ,e x ), (e x ,e ntF ), (e x ,e x,lst ), (e x,lst ,e ntF ), (e 01,x ,e 01,x ), (e 01,x ,e end ), (e 01,x ,e ntF )|x∈a, b ∪ (e x,lst ,e x,1 ), (e x,j ,e x,j,# 1 ), (e x,j ,e ntF ), (e x,j,# 1 ,e x,j,# 2 ), (e x,j,# 1 ,e ntF ) (e x,j,# 2 ,e ntF ), (e x,|x i |,# 2 ,e 01,x ), (e x,|x i |,# 2 ,e end )|x∈a, b, 0 < j ≤|x i | ∪ (e x,j,# 2 ,e x,j+1 )|x∈a, b, 0 < j <|x i | ∪ (e x,lst ,e 01 ), (e x,lst ,e end )|x∈a, b, |x i | = 0; and the precondition for each event in E i is given below: pre(e s ) = root∧ ̄ Kstg1pre(e st ) = stg1 pre(e x ) = x∧¬lastpre(e x,lst ) = x∧ last pre(e ntF ) = ntFpre(e x,j ) = x i [j]∧ loop x pre(e x,j,# 1 ) = # 1 ∧ loop x pre(e x,j,# 2 ) = # 2 ∧ loop x pre(e end ) =endpre(e 01,x ) =loop x ∨ lp, for each x∈a, b and j ≤|x i |. The action is illustrated in Figure 14. The remaining reduction proceeds in the same way as the one in Section 3. The difference is that the accessibility relation forrmv bt must become its reflexive and symmetric closure, and thatbtshould also range over # 1 and # 2 . Then, as in Section 4, one needs to also take into account the separator symbols # 1 and # 2 . 6 A Single Agent with Transitivity The case of (single-agent) transitive frames requires a slightly different construction. If we use a similar approach as in the other cases to add blocks to the encoding of a block sequence, it is hard to then distinguish between a state in a final loop and one that is part of the block encoding. Every state accessible from the loop is also accessible from the encoding state due to transitivity, but it is also the case that every state accessible from an encoding state must have an analogous state accessible from the loop, to be able to then unfold the loop into the encoding states. Our solution is to switch the order between the loops and the encoding states. A. AchilleosXX:29 e s e st e a e b e a,lst e b,lst e a,1 e b,1 e a,1,# 1 e b,1,# 1 e a,1,# 2 e b,1,# 2 e a,|a i | e b,|b i | e a,|a i |,# 1 e b,|b i |,# 1 e a,|a i |,# 2 e b,|b i |,# 2 e 01 e 01 e end Figure 14 The epistemic actionadd i , where the designated event,e s is marked with an arrow. For a cleaner figure, we omit event e ntF . We proceed to adjust our reduction to the case of a single agent with an accessibility relation that is reflexive and transitive (a preorder). We use the following set of propositional variables: Prp =0, 1, #, a, b, root, stg1, empty, lp. 6.1 The Epistemic States The initial epistemic state s I = ((W 0 ,R 0 ,V 0 ),w root ), where W 0 =w p | p∈root, empty, stg1, a, b∪w p (x)| p∈0, 1, #, lp, x∈a, b; R 0 is the reflexive and transitive closure of: R − 0 =(w root ,w empty ), (w root ,w stg1 ), (w root ,w bt (x)), (w bt (x),w # (x)), (w # (x),w bt (x)), (w # (x),w x ), (w bt (x),w lp ), (w # (x),w lp ) | x∈a, b, bt∈0, 1; and for everyw p ,w p ′ (x)∈ W 0 ,V 0 (w p ) =pandV 0 (w p ′ (x)) =p ′ ,x. The epistemic state s I is illustrated in Figure 15. ▶Definition 6.1. Letq a ,q b ∈ 0,1 ∗ . We defines q a q b to be the epistemic states q a q b = X:30 An Undecidability Proof for the Plan Existence Problem w root w stg1 w empty w a w b w 0 w 1 w # w 0 w 1 w # w lp Figure 15 The initial epistemic states I for the case of a single agent with a reflexive and transitive accessibility relation. We do not draw all the accessibility pairs; the accessibility relation is the reflexive and transitive closure of the one in the figure. ((W q a q b ,R q a q b ,V q a q b ),w root ), where W q a q b =w p | p∈root, a, b ∪ w x,j ,w x,j,# | x∈a, b and 1≤ j ≤|q x |; R q a q b is the reflexive, transitive closure of (w root ,w x )| x∈a, b ∪ (w root ,w x,j ), (w x,j ,w x,j,# ), (w x,j,# ,w x ) | x∈a, b, 1≤ j ≤|q x | ∪ (w x,j,# ,w x,j+1 )| x∈a, b, 1≤ j <|q x |; and for everyw p ∈ W q a q b ,V(w p ) =p, and for every 1≤ j ≤ |q x |,V(w x,j ) =q x [j],xand V (w x,j,# ) =#,x. As usual, we also define a variations ofs q a q b that encodes the same block but without the last separator. ▶Definition 6.2. Letq a ,q b ∈0,1 ∗ . We define the epistemic states q a q b −# and to be the submodel of s q a q b induced by W q a q b \w a,|q a |,# ,w b,|q b |,# . ▶ Definition 6.3. Letq 1 ,q 2 ∈ 0,1 ∗ . We define the epistemic states q a q b 0,1,#to be s q a q b 0, 1, # = ((W ′ q a q b ,R ′ q a q b ,V ′ q a q b ),w root ), where W ′ q a q b = W q a q b ∪w stg1 ,w 0 (x),w 1 (x),w # (x),w lp | x∈a, b; R ′ q a q b is the reflexive, transitive closure of R q a q b ∪(w root ,w stg1 ), (w root ,w 0 (x)), (w root ,w 1 (x)), (w 0 (x),w # (x)), (w 1 (x),w # (x)), (w # (x),w 0 (x)), (w # (x),w 1 (x)), (w 0 (x),w lp ), (w 1 (x),w lp ), (w # (x),w x )| x∈a, b ∪(w # (x),w x,1 )| x∈a, b, q x ̸= ε ∪(w,w lp )| w ∈w 0 (x),w 1 (x),w # (x)| x∈a, b; A. AchilleosXX:31 w root w stg1 w 1 w 0 w # w lp w 0 w 1 w # w a,1 w b,1 w a,1,# w b,1,# w a,|q a | w b,|q b | w a,|q a |,# w b,|q b |,# w a w b Figure 16 The epistemic state s q a q b 0, 1, #. and for everyw ∈ W q a q b ,V ′ q a q b (w) =V q a q b ,V ′ q a q b (w stg1 ) =stg1,V ′ q a q b (w lp ) =lp, and for p∈0, 1, # and x∈a, b, V ′ q a q b (w p (x)) =p,x. 6.2 The Epistemic Actions We use the following shorthand formulas: nxt(0) = nxt(1) = #,nxt(#) = 0∨ 1, nxt(a) = nxt(b) = 0∨ 1,symb = 0∨ 1∨ #, tail = symb∧ _ d∈0,1,# (d∧ K¬nxt(d)), andloop x = x∧ ̄ Klp for every x∈a, b. ▶ Remark 6.4. We note that the definition oftailis the main reason we need the separator symbol #. Otherwise, it would be harder to express that a state is the last encoding state when the accessibility relation is reflexive. We now show how to adjust the epistemic actions add i for this case. For every 1≤ i≤ n, we define add i = (E i ,R i ,e s ), where E i =e s ,e x ,e st ,e 01,x |x∈a, b ∪e x,j ,e x,j,# |x∈a, b, 0 < j ≤|x i |; R i is the reflexive, transitive closure of R − i =(e s ,e st ), (e s ,e x ), (e s ,e 01,x )|x∈a, b ∪ (e s ,e x,1 ), (e x,j ,e x,j,# ), (e x,j ,e x )|x∈a, b, 0 < j ≤|x i | ∪ (e x,j,# ,e x,j+1 )|x∈a, b, 0 < j <|x i |; and the precondition for each event in E i is given below: pre(e s ) = root∧ ̄ Kstg1pre(e st ) = stg1 pre(e x ) = x∧¬loop x pre(e x,j ) = x i [j]∧ loop x pre(e x,j,# ) = #∧ loop x pre(e 01,x ) =loop x ∨ lp, X:32 An Undecidability Proof for the Plan Existence Problem e s e st e 01,a e 01,b e a,1 e b,1 e a,1,# e b,1,# e a,|a i | e b,|b i | e a,|a i |,# e b,|b i |,# e a e b Figure 17 The epistemic action add i , where the designated event, e s is marked with an arrow. for each x∈a, b and j ≤|x i |. Actionadd i corresponds to adding a block at the end of a sequence of blocks. The precondition ofe s ensures that ̄ Kstg1is true at the epistemic state and therefore we are still in the first stage. The action is illustrated in Figure 17. The remaining reduction proceeds in the same way as usual (see Sections 3 to 5). 7 Conclusions We have shown that the plan existence problem for the case of preconditions of modal depth 1 and no postconditions is undecidable (except for the case of a single agent with negative introspection). This result completes the picture of (un)decidability of plan existence with respect to the modal depth of the pre- and postconditions. The situation may seem grim, as it appears that even very restricted epistemic precondi- tions suffice to make the plan existence problem undecidable. However, a more optimistic view is that the modal depth of the preconditions and postconditions is not the right measure to use to determine the hardness of the problem. In fact, several approaches restrict the problem successfully to ensure decidability. Decidability Usually, one solves the plan existence problem for a decidable case by showing that the class of relevant epistemic states is finite of finitely representable (e.g. [1,4]). To actively restrict the plan space, one can bound the length of the plan as in the bounded plan existence problem [4] or restrict the epistemic actions to be separable [3,4] — i.e. no two preconditions are consistent with each other. This assumption ensures that the state space does not grow arbitrarily. In fact, we note that it was crucial for our reduction that the epistemic actions are not separable, to allow the plan to encode arbitrarily long sequences of PCP blocks. The following decidability result is based on known ideas that have the same effect. A decidable case: an agent with negative introspection When the accessibility relations are constrained to be an equivalence relation, every epistemic state is bisimilar to one where every state is accessible and every set of propositional formulas is satisfied in at most one state. Then, Lemma 3.9 yields that the application of an epistemic action is equivalent to removing a subset of the states, and therefore we can consider only plans that have length at most as much as the number of states in the initial epistemic state. This observation yields the following theorem. ▶Theorem 7.1. The plan existence problem for the case of a single agent with reflexive, symmetric, and transitive accessibility relations, is in NP. A. AchilleosXX:33 We can also use a very similar argument for the slightly more general case of a single agent that has a Eucledian accessibility relation [9]. Furthermore, it is not hard to see that in this case, the plan existence problem isNP-hard by a reduction from SAT. A propositional formulaφwithPthe set of its propositional variables can be turned into an initial state whose worlds are0,p| p∈ P, where 0/∈ P; p∈ L(w) if and only ifw=pfor eachp∈ Pand worldw; and 0 is the designated state. For eachp∈ Pwe can introduce an epistemic action that removes worldp. Then, the goal isφ ′ , where φ ′ results from φ by replacing each p∈ P with ̄ Kp. ▶ Corollary 7.2. The plan existence problem for the case of a single agent with accessibility relations that are restricted to be at least Eucledian, is NP-complete. References 1Guillaume Aucher, Bastien Maubert, and Sophie Pinchinat. Automata Techniques for Epistemic Protocol Synthesis. In Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi, editors, 2nd International Workshop on Strategic Reasoning, SR 2014, volume 146 of EPTCS, page 11, 2014-04-06, France, April 2014. 2Thomas Bolander. A gentle introduction to epistemic planning: The DEL approach. Theoretical Computer Science, 243:1–22. 3 Thomas Bolander and Mikkel Birkegaard Andersen. Epistemic planning for single- and multi-agent systems. Journal of Applied Non-Classical Logics, 21(1):9–34, 2011. 4Thomas Bolander, Tristan Charrier, Sophie Pinchinat, and François Schwarzentruber. Del- based epistemic planning: Decidability and complexity. Artificial Intelligence, 287, October 2020. 5Tristan Charrier, Bastien Maubert, and François Schwarzentruber. On the impact of modal depth in epistemic planning. In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI’16, page 1030–1036. AAAI Press, 2016. 6Hans van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi. Dynamic Epistemic Logic. Springer Publishing Company, Incorporated, 1st edition, 2007. 7 Gaëtan Douéneau-Tabot, Sophie Pinchinat, and François Schwarzentruber. Chain-monadic second order logic over regular automatic trees and epistemic planning synthesis. Advances in Modal Logic, 12:237–256, 2018. 8Richard E. Fikes and Nils J. Nilsson. Strips: A new approach to the application of theorem proving to problem solving. Artificial Intelligence, 2(3):189–208, 1971. 9 Joseph Y. Halpern and Leandro Chaves Rêgo. Characterizing the NP-PSPACE gap in the satisfiability problem for modal logic. Journal of Logic and Computation, 17(4):795–806, 2007. 10Sébastien Lê Cong, Sophie Pinchinat, and François Schwarzentruber. Small undecidable problems in epistemic planning. In Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI’18, page 4780–4786. AAAI Press, 2018. 11Emil L. Post. A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society, 52:264–268, 1946. 12Henrik Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logic. In Stig Kanger, editor, Proceedings of the Third Scandinavian Logic Symposium, volume 82 of Studies in Logic and the Foundations of Mathematics, pages 110–143. Elsevier, 1975. 13 Johan Van Benthem. Correspondence theory. In Handbook of Philosophical Logic: Volume I: Extensions of Classical Logic, pages 167–247. Springer, 1984. 14Quan Yu, Ximing Wen, and Yongmei Liu. Multi-agent epistemic explanatory diagnosis via reasoning about actions. In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI ’13, page 1183–1190. AAAI Press, 2013.