Differential Equation Inductive Robustness Axiomatization
For researchers in formal verification and hybrid systems, this work provides a complete axiomatization and approximate decidability for robust safety of polynomial dynamical systems, enabling proof generation beyond finite horizons.
This paper proves the completeness of an axiomatization for robust safety of polynomial dynamical systems over bounded time, and establishes approximate decidability: for any perturbation parameter δ, a computable algorithm either produces a proof of robust safety or correctly decides the system is not robustly safe under δ-perturbation. The approach leverages subanalytic geometry to handle arbitrary bounded semialgebraic initial/post conditions without requiring positive separation at boundaries.
This article establishes the completeness of an axiomatization for the robust safety of dynamical systems with polynomial differential equations on bounded time horizons. Safety properties of robust systems are uniformly reduced to a sound axiomatization of polynomial invariants, resulting in reliable logical proofs of correctness. Approximate decidability results are also established: there is a computable algorithm such that, given any perturbation parameter $δ$, it either produces a symbolic proof of robust safety (hence correctly decides the dynamical system to be robustly safe), or correctly decides that the system is not robustly safe under a perturbation of level $δ$. In contrast to earlier works, this article crucially leverages results from subanalytic geometry to retain a level of exactness, thereby establishing positive results of provability/decidability allowing for arbitrary bounded (semialgebraic) initial/post conditions even without positive separation at their (topological) boundaries. This enables the generation of proofs of inductive safety beyond finite time horizons for general hybrid dynamical systems.