Simple dynamic logic with parallel composition and applications to planning

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.