On Propositional Dynamic Logic and Concurrency
This work addresses the long-standing challenge of applying dynamic logic to concurrency by introducing a parametric framework that separates programs from traces, enabling reasoning about interleaving in concurrent systems.
The authors generalize propositional dynamic logic (PDL) to operational PDL (OPDL), which separates programs from their traces generated by an arbitrary operational semantics, enabling reasoning about concurrency. They provide the first cut-elimination proof for a non-wellfounded sequent calculus for PDL and demonstrate OPDL's applicability to CCS and choreographic programming.
Dynamic logic is a powerful approach to reasoning about programs and their executions, obtained by extending classical logic with modalities that can express program executions as formulas. However, the use of dynamic logic in the setting of concurrency has proved problematic because of the challenge of capturing interleaving. This challenge stems from the fact that, traditionally, programs are represented by their sets of traces. These sets are then expressed as elements of a Kleene algebra, for which it is not possible to decide equality in the presence of the commutations required to model interleaving. In this work, we generalise propositional dynamic logic (PDL) to a logic framework we call operational propositional dynamic logic (OPDL), which departs from tradition by distinguishing programs from their traces. Traces are generated by an arbitrary operational semantics that we take as a parameter, making our approach applicable to different program syntaxes and semantics. To develop our framework, we provide the first proof of cut-elimination for a finitely-branching non-wellfounded sequent calculus for PDL. Thanks to this result we can effortlessly prove adequacy for PDL, and extend these results to OPDL. We conclude by discussing OPDL for two representative cases of concurrency: the Calculus of Communicating Systems (CCS), where interleaving is obtained by parallel composition, and Choreographic Programming, where interleaving is obtained by out-of-order execution.