Decidability of Iteration-free PDL with Parallel Composition

ABSTRACT. PRSPDL is a highly undecidable propositional dynamic logic with an operator for parallel composition of programs. This operator has a separation semantic such that a multiplicative conjunction similar to the one found in the logic of Boolean bunched implications is definable. The present work identifies an iteration-free decidable fragment of PRSPDL in which the multiplicative conjunction is still definable. A NEXPTIME complexity upper bound for the fragment is given.