Characterizing Positively Invariant Sets: Inductive and Topological Methods

TL;DR

This paper introduces two new characterizations of positive invariance for sets under differential equation flows, providing decision procedures that improve verification efficiency for polynomial systems.

Contribution

It presents two novel characterizations of positive invariance using inward and exit sets, along with decision procedures that outperform previous methods.

Findings

ESE procedure shows better performance than LZZ on complex semi-algebraic sets.

Both characterizations lead to decision procedures for polynomial ODE systems.

The proofs utilize the real induction principle for cleaner, unified reasoning.

Abstract

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.