Integration Methods for ODEs, II
Markus Neher, Karlsruhe Institute of Technology, Germany
Validated integration methods for ODEs aim at computing rigorous
bounds for specific solutions of ODEs. Interval arithmetic has been
used for almost 50 years for this purpose. Recently, Taylor model methods
for ODEs have been developed by Berz and Makino by combining interval
arithmetic with computer algebra. Taylor models reduce the dependency
problem and the wrapping effect intrinsic to interval arithmetic. They
also benefit from their capability of representing nonconvex sets, which
is especially advantageous for enclosing the flows of nonlinear ODEs.
The talks in the minisymosium report on recent developments in validated
methods for ODEs, including applications to practical problems.
McMaster University, Hamilton, Ontario.
interval method for ODEs, the VNODE-LP solver, and literate programming
Interval numerical methods produce rigorous bounds that are guaranteed
to contain mathematically correct solutions. Such bounds are typically
used to ensure that critical calculations are accurate and reliable
by proving that a solution is within certain bounds. However, an
error in the implementation of such a method may invalidate its
Nedialkov is the author of VNODE-LP: a C++ package for computing
rigorous bounds in IVPs for ODEs. A distinctive feature of this
solver is that it is developed entirely using Literate Programming---
the theory, documentation, and source code of VNODE-LP are interwoven
in a single document from which the source code is extracted.
As a result, the correctness of the implementation can be certified
by human experts, by reviewing its LP document, similarly to how
a scientific work is examined for correctness in a peer-review
talk provides an overview of numerical methods behind VNODE-LP,
its capabilities, and implementation. It also presents the author's
experience using literate programming for producing verifiable
University of California, Irvine
Tinkerbell is Chaotic
is a method of backward error analysis that plays a important
role in hyperbolic dynamics. In this paper, the shadowing by containment
framework is revisited, including a new shadowing theorem. This
new theorem has several advantages with respect to
existing shadowing theorems: it does not require injectivity or
differentiability, and its hypothesis can be easily verified using
interval arithmetic. As an application of this new theorem, shadowing
by containment is shown to be applicable to infinite length orbits
and is used to provide a computer assisted proof of the presence
of chaos in the well-known non-injective Tinkerbell map.
Politecnico di Milano, Italy
Integration of Asteroid Orbits
Taylor model integrators have recently shown to be a powerful tool
for the validated integration of ordinary differential equations.
By representing the flow of a differential equation by Taylor models
a tight enclosure for the action of the differential equations on
an extended region for a time step $\Delta t$ is provided. Consequently,
the integrated initial conditions can be either point vectors expressed
by real numbers or interval boxes. Thus, either point or interval
initial conditions can be rigorously integrated, so allowing the
propagation of uncertainty boxes on initial conditions.
this work the previous feature is exploited to rigorously predict
the long-term motion of Near Earth Objects and the verified identification
of impact occurrence. In particular, these techniques are applied
starting from a simple two-body problem up to a n-body dynamics
including also relevant nongravitational perturbations. In such
a way the validated integration of the motion of significant asteroids
can be addressed considering initial uncertainties consistent
with the current measurement accuracies.
test cases that show how Taylor model based integration outperforms
classical interval schemes are presented as well as a detailed
analysis of Apophis 2029 close encounter. In the latter case,
the beneficial effects of including both an automatic box splitting
technique and a suitable description of the vector field are analyzed.