On Propositional Dynamic Logic and Concurrency

TL;DR

This work addresses the challenge of applying Propositional Dynamic Logic (PDL) to concurrent programs by separating program reasoning from trace reasoning, thereby overcoming the undecidability issues arising from interleaving. It introduces operational PDL (OPDL), parameterized by an operational semantics, and proves a cut-elimination result for a finitely-branching non-wellfounded sequent calculus, enabling adequacy for PDL and extending to OPDL. OPDL is instantiated for CCS and choreographic programming to demonstrate increased expressivity in handling parallel composition and out-of-order execution. The framework provides a unifying, semantics-driven method to analyze concurrency in dynamic logic and suggests avenues for future work on more complex calculi and decision problems with trace-based equivalences. Overall, OPDL offers a robust, reusable foundation for reasoning about concurrent computations within a dynamic-logic setting, with potential impact on formal verification and protocol design.

Abstract

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.

Figures (17)

• Figure 1: Grammar generating formulas
• Figure 2: Axioms and rules for Propositional Dynamic Logic.
• Figure 3: Inductive definition of the meaning of compound formulas and programs in the Kripke frames.
• Figure 4: Sequent calculus rules of the sequent system $\mathsf{LPD}^{\mathsf{cut}}=\mathsf{LPD}\cup\{\mathsf{cut}\}$.
• Figure 5: Non-trivial derivations of the axioms of $\mathsf{PDL}\xspace$ in $\mathsf{LPD}$.

Theorems & Definitions (57)

• Remark 1
• Definition 2
• Theorem 3
• Lemma 4
• proof
• Definition 5
• Definition 7
• Lemma 8
• proof
• Lemma 9