Automatic Verification of Dynamical System Properties

by R. Baker Kearfott

Department of Mathematics, University of

Southwestern Louisiana

             rbk@usl.edu

Introduction

• Existence / uniqueness questions for dynamical systems are framed as existence / uniqueness of fixed points or solutions of nonlinear systems.

• With directed roundings, floating-point algorithms can rigorously prove or disprove such existence and uniqueness questions.

• Interval arithmetic can sometimes simultaneously verify such properties for an entire parametrized class of problems.

Dynamical Systems Verification November, 1997 IMA–1

Overview

This talk will

1. Review the basic underlying mathematical principles.

2. Review the connection between mathematical proofs and floating point computations.

3. Outline particular dynamical systems problems and the status of computational verification approaches.

4. Discuss practicality and future developments.

The General Mathematical Framework

Use the notation

X = {(x_{1}, x_{2}, …, x_{n})^{T} ∈ ℝ^{n}
|\underline{x}_{i} ≤ x_{i} ≤ \overline{x}_{i}, 1 ≤ i ≤ n\},

A fundamental problem is then

Given F : X → ℝ^{n} and X ∈ 𝕀ℝ^{n}, rigorously verify:

• there exists a unique X^{∗} ∈ X such that F (X^{∗}) = 0,

(1)

Computer arithmetic can be used to verify the assertion in Problem (1), with the aid of interval extensions and computational fixed point theorems.

Underlying Mathematics

• Classical fixed point theory implies existence.

– Contraction Mapping Theorem

– Brouwer Fixed Point Theorem

– Miranda’s Theorem

• Regularity (non-singularity) implies uniqueness.

• Fundamental property of interval arithmetic allows computational existence and uniqueness.

Underlying Mathematics

Miranda’s Theorem

Theorem 1 Suppose X ∈ 𝕀ℝ^{n}, and let the faces of X be denoted by

X\underline{i} = (x_{1}, …, x_{i−1}, \underline{x}_{i}, x_{i+1}, …, x_{n})^{T}
X\overline{i} = (x_{1}, …, x_{i−1}, \overline{x}_{i}, x_{i+1}, …, x_{n})^{T} .

Let F = (f_{1}, …, f_{n})^{T} be a continuous function defined on X. If

f_{i}^{u}(X\underline{i})f_{i}^{u}(X\overline{i}) ≤ 0  (2)

for each i between 1 and n, then there is an X ∈ X such that F (X) = 0.

Connections with Computation

Fundamental Property of Interval Arithmetic

Definition 1 If f : ℝ → ℝ is a function computable as an expression, algorithm or computer program involving the four elementary arithmetic operations, then a natural interval extension of f, whose value over an interval x is denoted by f(x), is obtained by replacing each occurrence of x by the interval x and by executing all operations as interval operations.

It is not hard to show

Theorem 2 If f is any natural interval extension of f, and x ∈ 𝕀ℝ is contained within the domain of f, then f(x) contains the range f^{u}(x) of f over x.

Dynamical Systems Verification November, 1997 IMA–6

Regularity

Lemma 3 Suppose F : X → ℝ^{n} and A is a Lipschitz matrix, such as F′(X). If A is regular, then any root of F in X is unique.

Proof: Suppose X^{∗} ∈ X and X ∈ X have F (X^{∗}) = 0 and F (X) = 0. If A is a Lipschitz matrix, then there is an A ∈ A such that

F (X^{∗}) − F (X) = 0
= A(X^{∗}) − A(X)
= A(X^{∗} − X).

If X^{∗} ≠ X, then A would have a null vector, contradicting the regularity of A.

Existence / Uniqueness with Interval Newton Methods

An interval Newton method is defined by an iteration of the form

X̃ = N(F; X, X̌) = X̌ + V,  (3)

where

Σ(A, −F (X̌)) ⊂ V,

where A is a Lipschitz matrix for F over X and Σ(A, −F (X̌)) is that set {X ∈ ℝ^{n}} such that there exists an A ∈ A with AX = −F (X̌).

Theorem 4 Suppose X̃ is the image of X under an interval Newton method. If X̃ ⊆ X, it follows that there exists a unique solution of F (X) = 0 within X.

Interval Newton Methods

Illustration

[figure: x_{1}; x_{2}; X̃; X; (\overline{x}_{1}, \overline{x}_{2}); (\underline{x}_{1}, \underline{x}_{2})]

In this case, an interval Newton method proves existence.

Dynamical Systems Verification November, 1997 IMA–9

On Interval Newton Methods

• Proof of the interval Newton existence / uniqueness theorem proceeds from properties of interval arithmetic and the contraction mapping theorem, Miranda’s theorem, or the Brouwer fixed point theorem (depending on context and particulars).

• Reasonable bounding sets V can be obtained by various methods, such as the preconditioned interval Gauss–Seidel method or preconditioned interval Gaussian elimination.

• Iteration of interval Newton methods leads to a locally quadratically convergent process.

Dynamical Systems Verification November, 1997 IMA–10

Applications of Interval Newton Existence/Uniqueness

• Global, exhaustive search for all solutions to a nonlinear system of equations.

• Rigorous, tight bounds on solutions to nonlinear systems, given solutions to approximate systems.

• Global optimization.

• Infallible step controls for continuation methods.

• Computation of the topological degree.

• Verification of a particular value of the topological degree.

Exhaustive Search for Solutions

Given F : X → ℝ^{n} and X ∈ 𝕀ℝ^{n}, find rigorous and tight bounds X^{∗} on all solutions X^{∗} ∈ X with F (X^{∗}) = 0, and prove that each set of bounds corresponds to a unique solution.

(4)

• The fundamental property of interval arithmetic, interval Newton methods, and a tesselation scheme for boxes X ∈ 𝕀ℝ^{n} are combined.

• The general problem is NP complete.

• Nonetheless, effective algorithms exist for moderate dimensions and for problems with special properties.

• Such algorithms are far faster than grid search, and also give mathematically rigorous results.

Dynamical Systems Verification November, 1997 IMA–12

Verification of Approximate

Solutions

\underline{The Procedure}:

1. An approximate solution X^{∗} is computed with a floating point algorithm.

2. A small box X^{∗} is constructed about X^{∗} (“ϵ-inflation”).

3. An interval Newton method is used to prove existence and uniqueness in X^{∗}

\underline{Practicality}:

• This problem is solved many times in exhaustive search.

• This problem is not NP-complete; the computational work is comparable to that of floating point linear system solvers.

Global Optimization

• The problem is similar to exhaustive search for solutions to systems of equations.

• Interval values of the objective function can be used to speed the search.

• Special techniques are used for problems with various types of constraints.

(Global optimization leads to more complicated algorithms than exhaustive search for zeros, and is more tenuously related to dynamical systems.)

Rigorous Step Controls for Continuation Methods

General Predictor–Corrector Methods

• The goal is to follow the one-dimensional solution manifolds of H(Z) = H(X, t) = 0, H : ℝ^{n+1} → ℝ^{n}.

• Popular predictor-corrector methods proceed as follows:

[figure: H(X) = 0; X_{0}; Z_{0}; X_{1}; predictor; correcting plane]

General Predictor-Corrector Methods

Failure Modes

This actually happens frequently!

[figure: t; X; H(X, t) = 0; H(X, t) = 0; X_{0}; Z_{0}; correcting plane]

Interval Step Control

Parametrized Interval Newton Methods 1. A coordinate t from the domain of

H : ℝ^{n+1} → ℝ^{n} is held fixed, and an interval Newton method is applied to the remaining coordinates.

2. With appropriate interval extensions to

the Jacobi matrix,

N(H(·, t); X, X̌) ⊂ H(X, t) implies that, for every t ∈ t, there is a unique solution of H(X, t) = 0.

3. We have also proven that there is a unique path passing through the faces (X, \underline{t}) and (X, \overline{t}) of the box (X, t) ⊂ ℝ^{n+1}.

4. Because of this uniqueness, the iterates cannot jump across branches or bifurcation points.

Dynamical Systems Verification November, 1997 IMA–17

Parametrized Interval Newton

Methods

\underline{Illustration}:

[figure: t; X; \underline{t}; \overline{t}; X̌; X; X̃; H(X, t) = 0; t]

Here, the computations prove that there is a unique path in the box, passing through the faces t = \underline{t} and t = \overline{t}. \underline{Practicality}: The interval step control suffers neither from the curse of dimensionality nor from overestimation in interval computations with large boxes.

Dynamical Systems Verification November, 1997 IMA–18

Computation of the Topological Degree

The general problem is

Given F : X ⊂ ℝ^{n} → ℝ^{n}, compute the topological degree d(F, X, 0) of F over X at 0.

• Computation of d(F, X, 0) is possible by finding all zeros of certain functions F̃ : D ⊂ ℝ^{n−1} → ℝ^{n−1} over the n (n − 1)-dimensional faces of X.

• This general degree computation is roughly n times as expensive as searching for all zeros of F in X.

• General degree computation may be useful for other reasons or when there are singular zeros of F.

Verification of a Particular Topological Degree Value

• If a particular value of the topological degree (such as 2) is suspected, or a particular singularity structure is suspected, then a modified interval Newton method can verify that the structure is as postulated.

• Such verification takes little more computational effort than application of an ordinary interval Newton method.

The above is work in progress.