Dynamic logic of parallel propositional assignments and its applications to planning

1 Introduction

Many authors have investigated how planning problems and their solutions can be represented in Propositional Dynamic Logic PDL, including work on conformant and contingent planning and planning with epistemic actions [Spalazzi and Traverso, 2000; Andersen et al., 2012; Li et al., 2017; Bolander et al., 2018; Cong et al., 2018]. However and to the best of our knowledge, it has not been investigated yet how planning with concurrent actions can be captured in dynamic logic. Probably the reason for that is that there is no consensus on the semantics of parallel actions in the PDL community: there are proposals interpreting parallel composition as interleaving [Mayer and Stockmeyer, 1996; Benevides and Schechter, 2014], as intersection [Balbiani and Vakarelov, 2003], and as relations between states and sets of states [Peleg, 1987; Goldblatt, 1992]. There are also extensions with modalities from resource separation logics [Balbiani and Boudou, 2018; Benevides et al., 2011; Veloso et al., 2014].

We here take a di�erent route and build on a simple version of dynamic logic where atomic programs are assignments of formulas to propositional variables. Dynamic Logic of Propositional Assignments DL-PA has numerous applications in knowledge representation [Herzig, 2014] in particular classical planning [Herzig et al., 2014], and is considerably simpler than PDL. In particular, complexity is much lower: satisfiability checking is in PSPACE. We add an operator of parallel composition to DL-PA, as well as an operator of inclusive nondeterministic composition (as opposed to PDL's exclusive nondeterministic composition).

In order to solve planning tasks by parallel plans several notions of interference have been proposed [Knoblock, 1994; Dimopoulos et al., 1997]. We choose the framework of independent parallel actions introduced in the planner GRAPHPLAN [Blum and Furst, 1997] where two actions interfere if one deletes a precondition or an e�ect of the other. This rather restrictive definition is used in most approaches to parallel classical planning. Non-interfering actions can be arranged in any sequential order with exactly the same outcome.

The paper is organised as follows. We extend DL-PA to DL-PPA in Section 2 and show in Section 3 that complexity stays in PSPACE. In Section 4 we show how sequential and parallel planning as well as their bounded versions can be polynomially translated to DL-PPA. Section 5 concludes.

2 DL-PA and DL-PPA

Our Dynamic Logic of Parallel Propositional Assignments DL-PPA extends Dynamic Logic of Propositional Assignments DL-PA by two program operators: an operator of parallel composition u and a new operator of nondeterministic composition t. The distinction between t and the standard operator of nondeterministic composition [ is similar to that between inclusive and exclusive disjunction: the interpretation of �1 [ �2 is "do either �1 or �2", while that of �1 t �2 is "do either �1, or �2, or both". We call the former exclusive nondeterministic choice and the latter inclusive nondeterministic choice. The interpretation of parallel composition �1 u �2 is that both programs are executed on local copies of the variables, and then the resulting state is obtained by merging these local states: �1 u �2 fails if two assigned variables get assigned di�erent truth values by �1 and �2; otherwise new truth values override old ones.

2.1 Language

The language of DL-PPA is built from a countably infinite set of propositional variables P. Programs � and formulas ' are defined by the grammar

where p ranges over P. The formula h�i' reads "there is a possible execution of � such that ' is true afterwards". The program p ' assigns the truth value of ' to p; for example, p :p swaps the truth value of p. '? tests that ' is true (failing when ' is false). �1; �2 executes �1 and �2 in sequence. �1 [ �2 nondeterministically chooses between executing either �1 or �2; �1 t �2 nondeterministically chooses between executing either �1, or �2, or both. �1 u�2 is the parallel composition of �1 and �2. The set of all formulas is FmlDL-PPA.

The language of DL-PA is the fragment of DL-PPA without t and u.

The set of propositional variables occurring in a formula ' is noted P '; similarly, the set of variables occurring in a program � is noted P �. For example, Pp q_r = fp; q; rg.

The length of formulas and programs is the number of symbols required to write them down, excluding parentheses and considering that the length of propositional variables is 1. We note them ' � ' � and ' � � � .

We use standard abbreviations such as > and ' ! , plus n-times iterations of programs, recursively defined by � �0 = >? and � �n+1 = >? [ (�; � �n ). For P = fp1; : : : ; png, ;pi2Ppi 'i is a shorthand for p1 '1; � � � ; pn 'n. We identify it with >? if P = ;. We have to be careful here because sequential composition ';' is not commutative; e.g., the interpretation of p q; q p will di�er from that of q p; p q. We will make sure each time that the order does not matter.

2.2 Semantics of DL-PPA

Semantics is in terms of valuations, alias states, which are subsets of P. So the set of all valuations is 2 P . We use V; V 0 ;W;U; : : : for valuations.

Formulas and programs are interpreted by mutual recursion. In DL-PA, the interpretation of a formula ' was a set of valuations jj'jjDL-PA � 2 P and the interpretation of a program � is a binary relation on valuations jj�jjDL-PA � 2 P � 2 P . We recall the main clauses:

In contrast, in DL-PPA the interpretation of � is a ternary relation on the set of valuations jj�jj � 2 P � 2 P � 2 P . When (V; U; W) 2 jj�jj then there is an execution of � from state V to state U assigning the variables in W. The definition is again by mutual recursion and the main clauses are given in Figure ??; the others are standard.

Let us comment on the clauses that are new w.r.t. DL-PA.

The semantics of the assignment p ' is: p is made true if ' is true and is made false if ' is false, and in both cases the set of assigned variables is the singleton fpg.

The semantics of parallel composition �1 u �2 is that each subprogram �i is executed locally; then it is checked whether the modifications (in terms of assigned variables) are compatible: this is the case when all variables that are assigned by both subprograms (namely the variables in W1 \W2) get assigned the same truth value. If this is not the case then �1 u�2 fails; otherwise the resulting valuation U is computed by putting together

• � the unchanged part of V, i.e., V n (W1 [W2);
• � the updates of �1, i.e., U1 \W1;
• � the updates of �2, i.e., U2 \W2.

Moreover, the set of variables W assigned by �1 u �2 is the union of those assigned by its subprograms.

The semantics of inclusive nondeterministic composition �1 t�2 is, as announced, the exclusive nondeterministic composition of the three programs �1, �2 and �1 u �2.

Here are some examples of interpretations of programs:

Proposition 1. Let � be a DL-PPA program and let (V;U;W) 2 jj�jj. Then:

• � W � P �;
• � V n U � W and U n V � W;
• � If P � � P then V � P implies U � P.

The first item can be restricted a bit further: W is a subset of the variables occurring on the left-hand side of assignments of �.

The next result says that the variables not occurring in a formula or a program do not matter in their interpretation.

Proposition 2. Let ' be a DL-PPA formula and � a DL-PPA program. Let P be a set of variables none of which occurs in ' or �, i.e., P is such that P \ P ' = P \ P � = ;. Then

• � V[P 2 jj'jj i� VnP 2 jj'jj;
• � (V[P;U[P;W) 2 jj�jj i� (VnP;UnP;W) 2 jj�jj.

A formula ' is satisfiable if and only if jj'jj , ;. Thanks to Propositions 1 and 2, when checking validity or satisfiability of a formula ' it su�ces to check triples (V;U;W) whose elements are all subsets of P '.

When the variables of �1 and �2 are disjoint then they can be sequentialised:

Proposition 3. Let �1 and �2 be two programs such that P �1 \ P �2 = ;. Then jj�1 u �2jj = jj�1; �2jj = jj�2; �1jj.

Just as in DL-PA [Balbiani et al., 2014], the Kleene star can be eliminated in DL-PPA: intuitively, when there exists a run of � � going from V to U then it is possible to go from V to U in no more than 2 jP �j iterations of �. (Indeed, if there is a longer run, it necessarily goes through the same valuation twice and can be shortened.)

Proposition 4. For all DL-PPA programs �, jj� � jj = jj� �2 jP �j jj.

2.3 Counters

In DL-PA one can implement k-bit counters (see e.g. [Balbiani et al., 2013, Section II.C]), and this transfers to DL-PPA. The encoding of a binary number of length k requires a vector of dlog ke propositional variables. We represent the state of the counter by a formula ct, which stands for the conjunction of these dlog ke variables or negations thereof. Furthermore we use the following abbreviations:

jjpjj = fV : p 2 Vg jjh�i'jj = fV : there are U;W such that (V;U;W) 2 jj�jj and U 2 jj'jjg jjp 'jj = f(V; V[fpg; fpg) : V 2 jj'jjg [ f(V; Vnfpg; fpg) : V < jj'jjg jj'?jj = f(V; V; ;) : V 2 jj'jjg jj�1; �2jj = f(V;U;W) : there are U1;W1;W2 such that (V;U1;W1) 2 jj�1jj; (U1;U;W2) 2 jj�2jj and W = W1 [W2g jj�1 [ �2jj = jj�1jj [ jj�2jj jj�1 t �2jj = jj�1jj [ jj�2jj [ jj�1 u �2jj jj�1 u �2jj = ( (V;U;W) : there are U1;W1;U2;W2 such that (V;U1;W1) 2 jj�1jj; (V;U2;W2) 2 jj�2jj; W1 \ W2 \ U1 = W1 \ W2 \ U2; U = (VnW) [ (U1\W1) [ (U2\W2); and W = W1 [ W2 ) jj� � jj = [ jj�jj k

Figure 1: Interpretation of DL-PPA programs

• � ct 0 is a program that resets ct: all variables of the counter are set to false;
• � For every integer i, ct=i is a formula that is true if and only if the value encoded by ct is i;
• � ct++ increments the value of ct.

We suppose that variables used in a counter do not occur elsewhere, so that they do not interfere with other programs.

Counters allow us to formulate in a more compact way our abbreviation � �k whose expansion has length exponential in k: using a dlog ke-bit counter we can identify � �k with

whose length is linear in ' � � � + log k. Indeed, although these two programs do not have the same interpretation, they behave the same as far as the variables of � are concerned.

Proposition 5. For valuations V;U;W � P �, we have (V;U;W) 2 jj� �k jj if and only if

(V; U[U 0 ;W[W 0 ) 2 jjct 0; (:ct=k ?; �; ct++) � jj

for some subsets U 0 and W 0 of the set of counter variables.

3 Reduction fromDL-PPA to DL-PA

We are now going to give a polynomial reduction of formulas and programs of DL-PPA to DL-PA. Our translation eliminates u and t thanks to the introduction of (several kinds of) fresh copies of propositional variables.

3.1 Copying Variables

First, the copy �p of p stores that p has been assigned; it will allow us to simulate the third component W of the interpretation of programs that keeps trace of assigned variables.

Second, when translating parallel composition �1 u �2 we sequentialise �1 and �2, and in order to safely do so we let each of them work on local copies of its variables p, respectively noted (p) 1 and (p) 2 . Similarly, we also use this technique when translating inclusive nondeterministic composition �1 t �2. (Observe that we cannot simply take over the interpretation of �1 t�2 as �1 [�2 [ (�1u�2) because this can generate exponential growth.)

It is convenient to extend copying from variables to sets of variables and to programs. We associate to each set of variables P � P the copies (P) 1 = f(p) 1 : p 2 Pg and (P) 2 = f(p) 2 : p 2 Pg; and we map programs � to (�) 1 by replacing all variables p of � by (p) 1 ; similarly, we map � to (�) 2 . For example, (p q ^ r) 2 = (p) 2 (q) 2 ^ (r) 2 .

Proposition 6. Let V;U;W � P � and let i be either 1 or 2. Then:

• � (V;U;W) 2 jj�jj i� ((V) i ; (U) i ; (W) i ) 2 jj(�) i jj;
• � V 2 jj'jj i� (V) i 2 jj(') i jj.

3.2 The Translation

We are going to show that u and t can be polynomially eliminated from DL-PPA formulas. The resulting formula is in the language of DL-PA, which will allow us to transfer complexity results. The recursive definition of the translation of formulas and programs is given in Figure ??. It is homomorphic for all the program operators and logical operators of PDL, so we only comment the non-trivial cases: assignments, parallel composition and inclusive nondeterministic composition.

The translation of p ' stores that p has been assigned by means of a fresh variable �p.

The translation of �1 u �2 relies on the introduction of fresh copies (p) 1 and (p) 2 of propositional variables p: as announced in Section 3.1, the program (�1) 1 is obtained by substituting each p in �1 by its copy (�1) 1 ; and similarly, (�2) 2 is obtained by substituting each p in �2 by (�2) 2 . The idea is to execute �1 and �2 on local copies of propositional variables and then check whether the two results can be merged: did the variables that were assigned by both subprograms modify their copies in the same way, i.e., is it the case that (�(p) 1 ^ �(p) 2 ) ! ((p) 1 $ (p) 2 ) for every p 2 P �1 \ P �2 ? If so then the values of the relevant copies are copied back to each p, where we the value of p is kept unchanged when none of the copies has been assigned. Moreover, the �p are updated in order to keep track of the modification of the variables p. Finally, the auxiliary variables (p) 1 , (p) 2 , �(p) 1 , �(p) 2 are set to false.

In the translation of inclusive nondeterministic composition �1 t �2, the check of compatibility followed by copying back is replaced by an exclusive nondeterministic composition of either copying back the values computed by �1, or those computed by �2, or checking compatibility and copying back the values computed by �1 u �2.

Example 1. Consider the program p > u p ?. Its translation f (p >u p ?) is:

Just as the original program, the translated program has an empty interpretation because after setting �(p) 2 and �(p) 1 to true and (p) 1 to true and (p) 2 to false, the test (�(p) 1 ^�(p) 2 ) ! ((p) 1 $ (p) 2 )? is going to fail.

3.3 Correctness of the Translation

For a set W � P, let �W = f�p : p 2 Wg.

Proposition 7. For every formula ', jj'jj = jj f (') jjDL-PA.

Proof. Let P 0 be a finite set of variables such that P ' � P 0 and and such that for every p 2 P ', none of the copies (p) 1 , (p) 2 , �p is in P 0 . We prove by simultaneous induction:

1. V 2 jj jj i� V[�P 2 jj f ( ) jjDL-PA, for every V � P 0 and every P � P;
2. (V;U;W) 2 jj�jj i� (V[�P;U[�W[�P) 2 jj f (�) jjDL-PA, for every V � P 0 and every U; W; P � P.

For the case of a formula of the form h�i' we use Propositions 1 and 2. For the cases program operators we use Proposition 1. For parallel composition and for inclusive nondeterministic composition we moreover use Proposition 6.

Then the result follows by Proposition 2.

�

Proposition 8. The length ' � f (') � of the translation of a DL-PPA formula ' is polynomial in the length ' � ' � of '.

3.4 Complexity Results

Lower bounds for DL-PPA reasoning tasks follow from those for its fragment DL-PA. In order to establish upper bounds we appeal to the translation.

Theorem 1. The DL-PPA model checking problem of deciding, given V and ', whether V 2 jj'jj is PSPACE-complete.

Proof. The lower bound is due to PSPACE hardness of DL-PA model checking [Herzig et al., 2011]. The upper bound is obtained by Proposition 7 and Proposition 8 thanks to PSPACEmembership of DL-PA [Balbiani et al., 2014]. �

Theorem 2. The DL-PPA satisfiability checking problem is PSPACE-complete.

Proof. The lower bound is due to PSPACE hardness of DL-PA satisfiability checking [Herzig et al., 2011]. The upper bound follows from PSPACE membership of DL-PPA model checking because satisfiability checking can be polynomially reduced to model checking: a DL-PPA formula ' is satisfiable if and only if ; 2 jjh;p2P ' (p >[ p ?)i'jj. �

4 DL-PPA Applied to Automated Planning

In this section, we formally define actions and sequential and parallel planning tasks within our framework DL-PPA. Then we show that DL-PPA model checking can be used to test the solvability of such tasks.

4.1 Sequential Planning with Conditional E�ects

A planning task is a triple (Act; V0; Goal) where:

• � Act is a set of conditional actions;
• � V0 � P is a valuation (the initial state);
• � Goal 2 FmlDL-PPA is the goal.

A conditional action is a pair a = (pre(a); e� (a)) where:

• � pre(a) 2 FmlDL-PPA is the precondition of a;
• � e�(a) 2 FmlDL-PPA � 2 P � 2 P is a set of triples ce of the form (cnd(ce); ce� + (ce); ce� � (ce)), the conditional e�ects of a, where cnd(ce) is a DL-PPA formula (the condition) and ce� + (ce) and ce� � (ce) are sets of variables that are respectively added and deleted by a if condition ce is true.

We say that a state V is reachable by a sequential plan from a state V0 via a set of conditional actions Act if there is a sequential plan, that is, a sequence of actions ha1; : : : ; ami from Act, and a sequence of states hV0; : : : ; Vmi with m � 0 such that V = Vm and �ak (Vk�1) = Vk for every k such that 1 � k � m. A planning task is solvable by a sequential plan if there is at least one state V 2 jjGoaljj such that V is reachable by a sequential plan from V0 via Act; otherwise it is unsolvable by a sequential plan.

A conditional action a determines a partial function �a from 2 P to 2 P as follows. First, �a(V) is defined (and therefore action a is executable in state V) if and only if

• � V 2 jjpre(a)jj and
• � ce� + (ce1) \ ce� � (ce2) = ; for all ce1; ce2 2 e�(a) such that V 2 jjcnd(ce1) ^ cnd(ce2)jj.

Second, when �a is defined in V then:

We associate to action a the DL-PPA program exeAct(a):

The program exeAct(a) behaves like a:

Lemma 1. For every action a 2 Act:

1. �a is defined in V i� there are U; W such that (V; U; W) 2 jjexeAct(a)jj ;
2. If �a is defined in V then �a(V) = U i� (V;U;W) 2 jjexeAct(a)jj for some W.

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

Figure 2: Translation from DL-PPA to DL-PA

Proof. Let us take an arbitrary state V.

When �a(V) is not defined then there are two cases. First, if V < jjpre(a)jj then the program fails because jjpre(a)?jj = ;. Second, if there are ce1; ce2 2 e�(a) and p 2 P such that V 2 jjcnd(ce1)^cnd(ce2)jj and ce� + (ce1)\ce� � (ce2) contains p then the program fails because jjp ?u p >jj = ;.

When �a(V) is defined then V 2 jjpre(a)jj, so (V; V; ;) 2 jjpre(a)?jj. Moreover, for each ce 2 e�(a) such that V 2 jjcnd(ce)jj, the programs � p2ce� + (ce) p > and � q2ce� � (ce) q ? are executed in parallel and all the assignments are consistent (no p ? and p > is executed in parallel). Therefore the parallel composition of all these programs leads, by definition, to the state �a(V) = U with (V;U;W) 2 jjexeAct(a)jj, where U is the set of variables assigned to > and W the set of all assigned variables in the program exeAct(a). �

4.2 Parallel Planning with Conditional E�ects

In order to define solvability of a planning task by a parallel plan, we must determine the conditions of parallel executability of a set of conditional actions A = fa1; : : : ; amg in a state V. We consider that two actions are independent and can be executed in parallel if and only if these actions have no contradictory e�ects and no cross interactions.

Two actions a and a 0 that are executable in V have contradictory e�ects in state V if and only if there are conditional e�ects ce 2 e� (a) and ce 0 2 e� (a 0 ) such that:

• � V 2 jjcnd(ce)jj and V 2 jjcnd(ce 0 )jj, and
• � ce� + (ce) \ ce� � (ce 0 ) , ;.

Action a has cross interaction with another action a 0 , a in state V if and only if there is a conditional e�ect ce 0 2 e� (a 0 ) such that:

• � V 2 jjcnd(ce 0 )jj, and
• � V < jjh( � p2ce� + (ce 0 ) p >) u ( � p2ce� � (ce 0 ) p ?)ipre(a)jj.

We say that a and a 0 have cross interactions in state V if and only if a has cross interaction with a 0 in the state V or a 0 has cross interaction with a in the state V.

In words, in any parallel plan, no e�ect of an action can be destroyed by an e�ect of another action executed in parallel, and no precondition of an action can be destroyed by an effect of another action executed in parallel. For example, in parallel classical planning, this makes that it is not possible to pick and drop a same object in parallel (contradictory e�ect) and that it is not possible for two agents to pick up the same object in parallel (cross interaction).

A set of conditional actions A = fa1; : : : ; amg determines a partial function �A from 2 P to 2 P : �A(V) is defined (a1; : : : ; am are executable in parallel in state V) if and only if:

1. for all ai 2 A, �ai is defined in V, and
2. for all ai; aj 2 A such that i , j:
3. � ai and aj have no contradictory e�ects, and
4. � ai and aj have no cross interactions.

When �A is defined in V then:

To every set of conditional actions we can associate a DL-PPA program that behaves exactly like the parallel execution of its elements. Given A = fa1; : : : ; amg, let exeAct(A) be the DL-PPA program

Lemma 2. For every finite set of actions A = fa1; : : : ; amg,

1. �A is defined in V i� there areU;W such that (V;U;W) 2 jjexeAct(A)jj ;
2. If �A is defined in V then �A(V) = U if and only if (V;U;W) 2 jjexeAct(A)jj for some W.

Proof. Let us take an arbitrary state V. By Lemma 1, for all i 2 f1; : : : ;mg we know that exeAct(ai) behaves like ai, and then is executable if �ai (V) is defined. If two actions a; a 0 2 A have contradictory e�ects in state V, there are ce 2 e� (a) and ce 0 2 e�(a 0 ) and p 2 P such that V 2 jjcnd(ce) ^ cnd(ce 0 )jj and ce� + (ce) \ ce� � (ce 0 ) contains p, then the program fails because of the execution of the parallel composition of p ? and p > in the program exeAct(a) u exeAct(a 0 ). If action a has cross interaction with action a 0 in state V, there is a conditional e�ect ce 0 2 e�(a 0 ) such that V 2 jjcnd(ce 0 )jj and V < jjh( � p2ce� + (ce 0 ) p >) u ( � p2ce� � (ce 0 ) p ?)ipre(a)jj, and then the execution of hexeAct(a 0 )ipre(a)? fails. Finally, the parallel composition of all these programs check contradictory e�ects and cross interactions and leads to the state �A(V) by definition because of the parallel execution of all exeAct(ai ). �

We say that a state V is reachable by a parallel plan from a state V0 via a set of conditional actions Act if there is a parallel plan, that is, a sequence hA1; : : : ; Ami of sets of actions Ai � Act and a sequence of states hV0; : : : ; Vmi with m � 0 such that V = Vm and �Ak (Vk�1) = Vk for every k such that 1 � k � m. A planning task (Act; V0;Goal) is solvable by a parallel plan if there is at least one state V 2 jjGoaljj such that V is reachable by a parallel plan from V0 via Act; otherwise it is unsolvable by a parallel plan.

4.3 Solvability of Bounded Horizon Planning Tasks

Now that we have defined a parallel encoding of actions and the solvability of a planning task, we can capture the solvability of a planning task in DL-PPA with bounded horizon k, which is known to be PSPACE-complete [Bylander, 1994].

Theorem 3. A planning task (Act; V0; Goal) is solvable by a sequential plan with no more than k actions if and only if:

^

x

Proof. Our formula reads "there exists an execution of �S a2Act exeAct(a) ��k after which Goal is true". We know by Lemma 1 that exeAct(a) behaves correctly and produces the same e�ects as action a. The program �S a2Act exeAct(a) ��k non-deterministically chooses an action a from Act and executes the corresponding program exeAct(a), then repeats this a number of times less or equal than k. This produces a sequence of at most k actions, i.e., a sequential plan bounded by k. Therefore the formula is satisfied in the initial state if and only if there exists a sequential plan of length bounded by k after which the goal is satisfied, i.e., if and only if the planning task is solvable with a sequence of at most k actions. �

Theorem 4. A planning task (Act; V0; Goal) is solvable by a parallel plan with no more than k steps if and only if:

where exea < PexeAct(a) for all a 2 Act, and

Proof. The program � a2Act exea ? initialises a special fresh variable exea < PexeAct(a) to ?, for each action a 2 Act. Then the inclusive nondeterministic composition F a2Act exea > chooses some non empty subset of actions A � Act and executes the program � a2A exea >. At this point, exea = > i� a 2 A, and the program �exe is executed. It is easily seen that, for a given choosen set of actions A, �exe behaves like the program exeAct(A). We know by Lemma 2 that this latter program behaves correctly and produces the same e�ect as the parallel execution of all actions in A. The sequence � a2Act exea ?; F a2Act exea >; �exe is then repeated a number of times less or equal than k. This produces a sequence of at most k parallel executions of action sets, i.e., a parallel plan bounded by k. Therefore the formula is satisfied in the initial state if and only if there exists a parallel plan of length bounded by k after which the goal is satisfied, i.e., if and only if the planning task is solvable with a sequence of at most k parallel steps. �

Both in Theorem 3 and in Theorem 4, the size of the model checking problems is polynomial in the size of the planning task plus log k. This relies on our compact representation of bounded programs � �k , cf. Proposition 5.

5 Conclusion

We have shown how to capture parallel classical planning in an extension of DL-PA by parallel and inclusive nondeterministic composition whose model checking and satisfiability checking problems are still in PSPACE. This allows in particular to decide, within the complexity boundaries, the existence of a plan given a finite horizon.

For the unbounded case we get similar characterisations if we replace �k in Theorems 3 and 4 by unbounded iteration � .

A straightforward continuation of our work is parallel epistemic planning: We can take over the epistemic extension of DL-PA in terms of observational variables that was applied to sequential epistemic planning in [Cooper et al., 2016].