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.

翻译：真正世界控制的系统需要稳定,因为它能确保这些系统能够容忍其理想的运行状态周围的小的、真实的世界扰动。本文件展示了以普通差分方程(ODEs)建模的连续系统的稳定如何能以不同的动态逻辑(dL)进行正式核实。关键见解是通过将 dL 的动态模式与一阶逻辑限定符适当嵌套,来说明ODE 的稳定。用这种方式来说明稳定性属性的逻辑结构有三个关键好处:一)它提供了一种灵活的方式,正式说明各种利益稳定的特性;二)它从dL 的对等方方方格中得出了这些稳定性特性的严格证明,并用 dL 的值安全和活性验证原则,以及三)它使得能够对各种稳定性属性之间的关系进行正式分析,而这种分析反过来又为这些特性的证明提供证据。这些好处通过在KeYmaera X(一种基于 dL的混合系统理论)中为几个例子实施稳定性证明而付诸实践。