论命题动态逻辑与并发

《ACM Transactions on Computational Logic》：On Propositional Dynamic Logic and Concurrency

　　动态逻辑是一种推理程序和其执行的强有力方法，它通过对经典逻辑进行扩展，引入能够以公式形式表达程序执行的模态算子而获得。然而，在并发环境中使用动态逻辑一直存在困难，因为难以准确刻画交错（interleaving）行为。这一困难源于：传统上，程序由其迹（traces）集合表示；这些集合随后被表达为 Kleene 代数中的元素，而在需要建模交错时引入的交换律下，其相等性是不可判定的。在本工作中，我们将命题动态逻辑（PDL）推广为一个我们称之为操作性命题动态逻辑（OPDL）的逻辑框架。该框架突破了传统做法，将程序与其迹区分开来。迹由一个任意的操作语义生成，我们将该语义作为参数，从而使我们的方法适用于不同的程序语法和语义。为构建我们的框架，我们首次为 PDL 的一个有限分支、非良基的序列演算给出了消去律（cut-elimination）的证明。借助这一结果，我们可以轻松地证明 PDL 的适切性（adequacy），并将这些结果推广至 OPDL。最后，我们讨论了 OPDL 在两种具有代表性的并发情形下的应用：通信系统演算（CCS），其中交错通过并行组合获得；以及编舞编程（Choreographic Programming），其中交错通过乱序执行获得。