This paper presents a dynamic logic $d\mathcal{L}_\text{CHP}$ for compositional deductive verification of communicating hybrid programs (CHPs). CHPs go beyond the traditional mixed discrete and continuous dynamics of hybrid systems by adding CSP-style operators for communication and parallelism. A compositional proof calculus is presented that modularly verifies CHPs including their parallel compositions from proofs of their subprograms by assumption-commitment reasoning in dynamic logic. Unlike Hoare-style assumption-commitments, $d\mathcal{L}_\text{CHP}$ supports intuitive symbolic execution via explicit recorder variables for communication primitives. Since $d\mathcal{L}_\text{CHP}$ is a conservative extension of differential dynamic logic $d\mathcal{L}$, it can be used soundly along with the $d\mathcal{L}$ proof calculus and $d\mathcal{L}$'s complete axiomatization for differential equation invariants.

翻译：本文提出了一种动态逻辑 $d\mathcal{L}_\text{CHP}$，用于对通信混合程序（CHP）进行组合式演绎验证。CHP 在混合系统传统的离散与连续混合动力学基础上，通过添加 CSP 风格的通信与并行操作符进行了扩展。本文提出了一种组合式证明演算，该演算通过动态逻辑中的假设-承诺推理，从子程序的证明出发，模块化地验证 CHP（包括其并行组合）。与 Hoare 风格的假设-承诺不同，$d\mathcal{L}_\text{CHP}$ 通过为通信原语引入显式的记录器变量，支持直观的符号执行。由于 $d\mathcal{L}_\text{CHP}$ 是微分动态逻辑 $d\mathcal{L}$ 的保守扩展，它能与 $d\mathcal{L}$ 证明演算及其关于微分方程不变式的完全公理化系统一起可靠使用。