论文标题
表征积极不变的集：感应和拓扑方法
Characterizing Positively Invariant Sets: Inductive and Topological Methods
论文作者
论文摘要
我们介绍了在普通微分方程系统流动下集合积极不变性的两个表征。第一个表征使用内部集合，从直观地收集了这些点，这些点在短时间内在集合中演变而成，而第二个特征则使用退出集的概念，这些概念直观地收集了流量立即离开集合的那些点。我们的证据强调将实际归纳原则用作一种通用统一的证明技术，该技术捕获了正式推理的本质，证明了我们的结果合理，并提供了已知结果的更清洁的替代证明。本文中介绍的两个特征本质上是等效的，但在多项式普通微分方程系统的流动下，在检查给定的半代数集合下是否有两个不同的决策程序（分别称为LZZ和ESE）。该过程LZZ在Liu，Zhan和Zhao的原始作品上有所改善（Emsoft 2011）。本文中介绍的程序通过以原则性的方式将问题分解为更容易检查的简单子问题，并且显示出与具有非繁琐布尔式结构的公式所描述的半代数集相比，其表现出色，并且表现出更高的性能。
We present two characterizations of positive invariance of sets under the flow of systems of ordinary differential equations. The first characterization uses inward sets which intuitively collect those points from which the flow evolves within the set for a short period of time, whereas the second characterization uses the notion of exit sets, which intuitively collect those points from which the flow immediately leaves the set. Our proofs emphasize the use of the real induction principle as a generic and unifying proof technique that captures the essence of the formal reasoning justifying our results and provides cleaner alternative proofs of known results. The two characterizations presented in this article, while essentially equivalent, lead to two rather different decision procedures (termed respectively LZZ and ESE) for checking whether a given semi-algebraic set is positively invariant under the flow of a system of polynomial ordinary differential equations. The procedure LZZ improves upon the original work by Liu, Zhan and Zhao (EMSOFT 2011). The procedure ESE, introduced in this article, works by splitting the problem, in a principled way, into simpler sub-problems that are easier to check, and is shown to exhibit substantially better performance compared to LZZ on problems featuring semi-algebraic sets described by formulas with non-trivial Boolean structure.
