End Cover for Initial Value Problem: Complete Validated Algorithms with Complexity Analysis
Bingwei Zhang, Chee Yap
TL;DR
The paper tackles the End Cover Problem for the autonomous IVP $\mathbf{x}'=\mathbf{f}(\mathbf{x})$ by developing a complete validated algorithm that computes an $\varepsilon$-end cover of $\mathrm{End}_{\boldsymbol{f}}(B_0,h)$. It introduces an enhanced EndEncl, a boundary-cover technique grounded in trajectory bundles and Brouwer's Invariance of Domain, and provides explicit complexity bounds for both EndEncl and EndCover. The authors demonstrate practical viability with experiments that show tighter enclosures and robustness compared to existing validated solvers, especially over longer time horizons. These contributions advance certifiable reachability analysis for nonlinear IVPs with quantified uncertainty and pave the way for scalable, fully halted interval-based validation methods.
Abstract
We consider the first-order autonomous ordinary differential equation \[ \mathbf{x}' = \mathbf{f}(\mathbf{x}), \] where $\mathbf{f} : \mathbb{R}^n \to \mathbb{R}^n$ is locally Lipschitz. For a box $B_0 \subseteq \mathbb{R}^n$ and $h > 0$, we denote by $\mathrm{IVP}_{\mathbf{f}}(B_0,h)$ the set of solutions $\mathbf{x} : [0,h] \to \mathbb{R}^n$ satisfying \[ \mathbf{x}'(t) = \mathbf{f}(\mathbf{x}(t)), \qquad \mathbf{x}(0) \in B_0 . \] We present a complete validated algorithm for the following \emph{End Cover Problem}: given $(\mathbf{f}, B_0, \varepsilon, h)$, compute a finite set $\mathcal{C}$ of boxes such that \[ \mathrm{End}_{\mathbf{f}}(B_0,h) \;\subseteq\; \bigcup_{B \in \mathcal{C}} B \;\subseteq\; \mathrm{End}_{\mathbf{f}}(B_0,h) \oplus [-\varepsilon,\varepsilon]^n , \] where \[ \mathrm{End}_{\mathbf{f}}(B_0,h) = \left\{ \mathbf{x}(h) : \mathbf{x} \in \mathrm{IVP}_{\mathbf{f}}(B_0,h) \right\}. \] Moreover, we provide a complexity analysis of our algorithm and introduce a novel technique for computing the end cover $\mathcal{C}$ based on covering the boundary of $\mathrm{End}_{\mathbf{f}}(B_0,h)$. Finally, we present experimental results demonstrating the practicality of our approach.
