用于验证控制不变性的比较不变量
Comparison Invariants for Verifying Control Invariance
AI总结：
本文在微分动态逻辑（dL）中引入比较不变量，推导相关公理与规则，将控制不变性简化为函数不等式，统一了控制障碍函数等安全验证技术，可用于验证控制不变性。
AI中文摘要：
控制不变性验证动态系统是否存在控制输入，使其在任何时刻都能保持给定属性。本文在微分动态逻辑（differential dynamic logic, dL）中引入一组可靠公理和证明规则，用于验证控制不变性。首先，在dL中公理化标量与向量比较原理，该原理将微分方程组与比较系统关联，以便更轻松地建立不变性属性，此公理化主要利用微分幽灵（differential ghosts），它是比较系统的证明论泛化。接下来，以比较原理为基础，引入比较不变量并推导可靠公理与证明规则。比较不变量将控制不变性问题简化为合适函数的李导数（Lie derivative）上的函数不等式，且函数的恰当选择可得到可判定的算术。此外，安全关键控制中常用的控制障碍函数（control barrier functions, CBFs）被证明是比较不变量的特例，这为CBFs建立了公理化并得到一组专用证明规则，这些规则可用于验证传统上用于合成安全控制器却未经过验证的CBFs。最后，比较不变量被证明能统一其他几种安全验证技术，包括达布不变量（Darboux invariants）和微分不变量，进一步巩固了其通用性。
英文摘要：
Control invariance validates that dynamical systems have a control input that preserves a given property at all times. This paper introduces a set of sound axioms and proof rules in differential dynamic logic (dL) that enable verification of control invariance. First, the scalar and vector comparison principles, relating a system of differential equations to a comparison system such that invariance properties can be established more easily, are axiomatized in dL. This axiomatization primarily utilizes differential ghosts, which are proof-theoretic generalizations of comparison systems. Next, with the comparison principles serving as the basis, comparison invariants are introduced, and sound axioms and proof rules are derived. Comparison invariants reduce the question of control invariance to a functional inequality on its Lie derivative for a suitable class of functions, moreover, the right choice of function can result in decidable arithmetic. Furthermore, the perennially popular control barrier functions (CBFs) used in safety-critical control are shown to be a special instance of comparison invariants. This yields an axiomatization of CBFs that leads to a dedicated set of proof rules. The rules allow for the verification of CBFs, which are traditionally used for synthesizing safe controllers without verification. Lastly, comparison invariants are shown to unify several other safety verification techniques, including Darboux invariants and differential invariants, further cementing their versatility.
