Table of Contents
Fetching ...

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.

End Cover for Initial Value Problem: Complete Validated Algorithms with Complexity Analysis

TL;DR

The paper tackles the End Cover Problem for the autonomous IVP by developing a complete validated algorithm that computes an -end cover of . 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 where is locally Lipschitz. For a box and , we denote by the set of solutions satisfying We present a complete validated algorithm for the following \emph{End Cover Problem}: given , compute a finite set 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 Moreover, we provide a complexity analysis of our algorithm and introduce a novel technique for computing the end cover based on covering the boundary of . Finally, we present experimental results demonstrating the practicality of our approach.
Paper Structure (22 sections, 10 theorems, 68 equations, 5 figures, 4 tables)

This paper contains 22 sections, 10 theorems, 68 equations, 5 figures, 4 tables.

Key Result

Theorem 1

Let ${\boldsymbol{f}}:{\mathbb R}^n\to {\mathbb R}^n$ be locally Lipschitz. For all ${\boldsymbol{p}}_0\in {\mathbb R}^n$, there exists $h,r>0$ such that there exists an ${\boldsymbol{f}}$-bundle

Figures (5)

  • Figure 1: $\varepsilon$-End Covers ($\varepsilon=0.1$) at times $h_i\in$$(0, 0.1, 0.4, 0.7,1.0)$ for $i=0 ,\ldots , 4$. The boxes in ${\mathcal{C}}$ are colored for visualization. An enlarged image for the cover at $h_4 = 1.0$ is also shown.
  • Figure 2: $\varepsilon$-Boundary Covers ($\varepsilon=0.01$) at times $h_i\in (0, 0.1, 0.4, 0.7,1.0)$ for $i=0 ,\ldots , 4$. The boxes in a cover ${\mathcal{C}}$ are colored to visualize them. An enlarged image for the cover at $h_4 = 1.0$ is also shown.
  • Figure 3: Trajectories and end enclosures for Examples Eg1 and Eg2 with $\varepsilon=0.01$.
  • Figure 4: Trajectories and end enclosures for Example Eg3 and Eg4 with $\varepsilon=0.01$.
  • Figure 5: Trajectories and end enclosures for Example Eg5 and Eg6 with $\varepsilon=0.01$.

Theorems & Definitions (10)

  • Theorem 1: Picard-Lindelöf
  • Theorem 2
  • Theorem 3: Existence of ${\boldsymbol{f}}$-bundles
  • Theorem 4
  • Proposition 5
  • Lemma 6
  • Lemma 7
  • Lemma 8
  • Lemma 9
  • Theorem 10