微分方程解的存在性和活性的公理化方法
An Axiomatic Approach to Existence and Liveness for Differential Equations
摘要：
本文提出了一种用微分动态逻辑演绎证明常微分方程存在性和活性的公理化方法。该方法证明了一个给定的常微分方程的解决方案存在足够长的时间，以达到一个给定的目标区域，而不离开一个给定的进化域。许多微妙之处使离散活性验证技术（如循环变量）推广到连续设置变得复杂。例如，ODE解可能在有限时间内爆炸，或者它们朝着目标的进展可能收敛到零。这些微妙的处理在dL连续精炼ODE活性属性使用ODE不变性属性，具有完整的公理化。这种方法是广泛适用的：从文献中的几个活性参数进行了调查，并推导出特殊情况下的公理化细化的dL。这些推导也纠正了调查文献中的几个可靠性错误，这进一步突出了ODE活性推理的微妙性和公理化方法的实用性。这种方法的一个重要特例是推导出常微分方程的（全局）存在性，这是每个常微分方程活性参数的基本部分。因此，所有存在性的推广和它们的证明都会直接导致相应的常微分方程活性论证的推广。总的来说，由此产生的共同细化步骤库，使新的ODE存在的合理发展和理由，从dL公理的活性证明规则。这些见解付诸实践，通过实施ODE活性证明的KeYmaera X定理证明混合系统。
英文摘要：
This article presents an axiomatic approach for deductive verification of existence and liveness for ordinary differential equations (ODEs) with differential dynamic logic (dL). The approach yields proofs that the solution of a given ODE exists long enough to reach a given target region without leaving a given evolution domain. Numerous subtleties complicate the generalization of discrete liveness verification techniques, such as loop variants, to the continuous setting. For example, ODE solutions may blow up in finite time or their progress towards the goal may converge to zero. These subtleties are handled in dL by successively refining ODE liveness properties using ODE invariance properties which have a complete axiomatization. This approach is widely applicable: several liveness arguments from the literature are surveyed and derived as special instances of axiomatic refinement in dL. These derivations also correct several soundness errors in the surveyed literature, which further highlights the subtlety of ODE liveness reasoning and the utility of an axiomatic approach. An important special case of this approach deduces (global) existence properties of ODEs, which are a fundamental part of every ODE liveness argument. Thus, all generalizations of existence properties and their proofs immediately lead to corresponding generalizations of ODE liveness arguments. Overall, the resulting library of common refinement steps enables both the sound development and justification of new ODE existence and of liveness proof rules from dL axioms. These insights are put into practice through an implementation of ODE liveness proofs in the KeYmaera X theorem prover for hybrid systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
