Abstract Though Propositional Dynamic Logic (PDL) as well as its relation to planning has been widely studied, there is as of yet no consensus as to how to handle parallelism in the framework. In this paper, we propose a parallel version of the Dynamic Logic of Propositional Assignments (${\textsf{DL-PA} } $), a simple fragment of PDL in which atomic programs are assignments of the truth value of a formula to a propositional variable. We introduce two new operators for ${\textsf{DL-PA} }$, namely parallel composition and inclusive non-deterministic composition. For the former, we suppose that two programs can be executed in parallel if they do not assign different values to the same variable. We give a polynomial translation of the resulting Dynamic Logic of Parallel Propositional Assignments (${\textsf{DL-PPA} }$) into ${\textsf{DL-PA} }$, thereby showing that complexity remains in PSpace. We then turn to planning and show how to capture executability of parallel STRIPS-like actions and solvability of planning tasks by parallel plans in ${\textsf{DL-PPA} }$, following three different semantics for parallelism: one closely following our criterion for parallelism in ${\textsf{DL-PPA} }$, and two from the literature based on interleaving.

International audience

We study a simple version of multi-agent epistemic planning where the number of parallel steps has to be minimized. We prove that this extension of classical planning is in PSPACE. We propose an encoding in PDDL and present some experiments providing evidence that this encoding allows us to solve practical problems. The types of problems we can encode include problems in which one agent can teach another agent how to perform a task and communication problems where some information must not be revealed to some agents.

We introduce a dynamic logic with parallel composition and two kinds of nondeterministic composition, exclusive and inclusive. We show PSPACE completeness of both the model checking and the satisfiability problem and apply our logic to sequential and parallel classical planning where actions have conditional effects.