On Propositional Dynamic Logic and Concurrency

Matteo Acclavio, Fabrizio Montesi, Marco Peressotti [2024].
In CoRR abs/2403.18508.

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.

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@article{DBLP:journals/corr/abs-2403-18508,
  author       = {Matteo Acclavio and
                  Fabrizio Montesi and
                  Marco Peressotti},
  title        = {On Propositional Dynamic Logic and Concurrency},
  journal      = {CoRR},
  volume       = {abs/2403.18508},
  year         = {2024},
  url          = {https://doi.org/10.48550/arXiv.2403.18508},
  doi          = {10.48550/ARXIV.2403.18508},
  eprinttype    = {arXiv},
  eprint       = {2403.18508},
  timestamp    = {Wed, 10 Apr 2024 17:37:45 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2403-18508.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}