Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification

动态逻辑及其变种因其清晰和表达性强的特点，在程序/系统规范和验证等领域中已被用作形式化工具多年，并有许多其他应用。动态逻辑的程序模型以显式形式呈现。对于不同的目标程序模型，必须提出不同的动态逻辑理论来适应不同模型的语义。在本文中，我们提出了一种参数化的“动态逻辑风格”形式化工具，即$DL_p$，用于指定和推理一般的程序模型。在$DL_p$中，程序模型和逻辑公式被视为“参数”，允许根据不同的感兴趣领域采用任意形式。这种特性使$DL_p$能够支持基于程序模型的操作语义的直接推理，同时仍保留基于语法结构的组合推理。$DL_p$提供了一个灵活的验证框架，以涵盖不同的动态逻辑理论。此外，它还便于对语义不是组合的程序模型进行推理，例如神经网络、基于自动机的模型、同步编程语言等。我们主要关注$DL_p$理论的构建，包括定义其语法和语义、构建证明系统和构建循环预证明结构。我们分析并证明了$DL_p$的合理性。案例研究展示了$DL_p$如何用于推理不同类型的程序模型。

本论文提出了一个名为$DL_p$的参数化动态逻辑形式，用于规范和推理关于一般程序模型的性质。$DL_p$的特点是将程序模型和逻辑公式作为“参数”，可以适应不同的领域和语义，从而支持基于程序模型操作语义的直接推理和基于语法结构的组合推理。主要针对的问题是如何针对不同类型的程序模型提出适当的动态逻辑理论，以及如何进行推理。

$DL_p$是一个参数化动态逻辑形式，可以适应不同类型的程序模型，支持直接推理和组合推理，为不同的动态逻辑理论提供了灵活的验证框架。

论文提出了$DL_p$的语法和语义，建立了证明系统并构建了循环预证明结构。并分析证明了$DL_p$的合理性。案例研究展示了$DL_p$如何用于推理不同类型的程序模型。

近年来，许多动态逻辑形式被提出用于程序/系统规范和验证，例如时态逻辑、模态逻辑、线性时间逻辑等。相关研究包括：Pnueli, M. (1977). The temporal logic of programs. Annual Symposium on Foundations of Computer Science, 46–57. Clarke, E. M., & Emerson, E. A. (1981). Design and synthesis of synchronization skeletons using branching-time temporal logic. Logic of Programs, 52–71. Alur, R., & Henzinger, T. A. (1994). Reactive modules. Formal Methods in System Design, 5(1), 1–23.