Resource separation in dynamic logic of propositional assignments

TL;DR

This paper extends the dynamic logic of propositional assignments with a parallel composition operator inspired by separation logics, providing an axiomatisation and analyzing the complexity of related decision problems.

Contribution

It introduces a new operator for parallel composition into the logic, along with a reduction axiomatization, and proves decidability and PSPACE complexity bounds.

Findings

Axiomatisation via reduction axioms established

Decidability of the extended logic proven

Model checking and satisfiability remain in PSPACE

Abstract

We extend dynamic logic of propositional assignments by adding an operator of parallel composition that is inspired by separation logics. We provide an axiomatisation via reduction axioms, thereby establishing decidability. We also prove that the complexity of both the model checking and the satisfiability problem stay in PSPACE.