On Propositional Dynamic Logic and Concurrency
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要