Symbolic Computation Group

Consider an autonomous first-order differential equation

x ′ = f (x) ...(1)

where f : R^n → R^n is of class C^k for some k ≥ 2. For a box B_{0} ⊆ R^n and h > 0, define

End_{f}(B_{0}, h) = {x(h) : x ∈ IVP_{f}(B_{0}, h)},

where IVP_{f}(B_{0}, h) is the set of solutions x : [0, h] → R^n of (1) with initial value x(0) ∈ B_{0}. A finite set C of boxes is an ε-cover for End_{f}(B_{0}, h) if

End_{f}(B_{0}, h) ⊆ (\bigcup_{B∈C}{B}) ⊆ (End_{f}(B_{0}, h) ⊕ [−ε, ε]^n ).

This is a form of reachability problem for the Initial Value Problem (IVP) of ODE’s. We present a complete validated algorithm to compute such an ε-cover. Completeness means that if the input (f, B_{0}, h, ε) is valid, then our algorithm halts. It is the first complete validated algorithm. The ability of users to specify any ε > 0 is also a unique feature.

We introduce the scaffold data structure and develop new validated primitives to support the efficient computation of end covers. Preliminary experiments demonstrate the practicality of our method and its favorable performance compared with state-of-the-art validated algorithms.

Joint work with Bingwei Zhang.