论文标题
普通微分方程的演绎稳定性证明
Deductive Stability Proofs for Ordinary Differential Equations
论文作者
论文摘要
现实世界受控系统需要稳定性，因为它可以确保这些系统可以忍受所需的运营状态周围的小小的现实世界扰动。本文展示了如何通过差分动态逻辑（DL）正式验证的连续系统的稳定性如何。关键的见解是通过将DL的动态模态与一阶逻辑量化器合适地嵌套来指定ODE稳定性。以这种方式阐明稳定性特性的逻辑结构具有三个关键好处：i）提供了一种灵活的手段，可以正式指定感兴趣的各种稳定性特性，ii）ii）在DL的ode ode ode ode安全性和livesice验证原理和iii中，从DL的公理中获得了这些稳定性的严格证明，以及在各种稳定性之间的关系。这些好处是通过实施基于DL的混合系统定理供体的Keymaera X中的几个示例来实施的。
Stability is required for real world controlled systems as it ensures that those systems can tolerate small, real world perturbations around their desired operating states. This paper shows how stability for continuous systems modeled by ordinary differential equations (ODEs) can be formally verified in differential dynamic logic (dL). The key insight is to specify ODE stability by suitably nesting the dynamic modalities of dL with first-order logic quantifiers. Elucidating the logical structure of stability properties in this way has three key benefits: i) it provides a flexible means of formally specifying various stability properties of interest, ii) it yields rigorous proofs of those stability properties from dL's axioms with dL's ODE safety and liveness proof principles, and iii) it enables formal analysis of the relationships between various stability properties which, in turn, inform proofs of those properties. These benefits are put into practice through an implementation of stability proofs for several examples in KeYmaera X, a hybrid systems theorem prover based on dL.
