March 27, 20240 citationsOpen Access

On Propositional Dynamic Logic and Concurrency

MAMatteo AcclavioUniversity of Southern Denmark FMFabrizio MontesiUniversity of Southern Denmark MPMarco PeressottiUniversity of Southern Denmark

Key Points

Operational propositional dynamic logic (OPDL) effectively addresses the interleaving issue in concurrent systems, improving reasoning capabilities.
We prove that the cut-elimination property holds true in the sequent calculus for both PDL and OPDL, confirming their robustness.
Generalizing propositional dynamic logic allows us to handle sets of programs with various operational semantics effectively, unlike traditional methods.

Abstract

Dynamic logic in the setting of concurrency has proved problematic because of the challenge of capturing interleaving. This challenge stems from the fact that the operational semantics for programs considered in these logics is tailored on trace reasoning for sequential programs. In this work, we generalise propositional dynamic logic (PDL) to a logic framework we call operational propositional dynamic logic (OPDL) in which we are able to reason on sets of programs provided with arbitrary operational semantics. We prove cut-elimination and adequacy of a sequent calculus for PDL and we extend these results to OPDL. We conclude by discussing OPDL for Milner's CCS and Choreographic Programming.

KI fragen

Bookmark

View Full Paper