Expansion and estimation of the range of nonlinear functions

Source abstract

Many verification algorithms use an expansion f ( x ) ∈ f ( x ~ ) + S ⋅ ( x − x ~ ) f(x) \in f(\tilde {x}) + S \cdot (x - \tilde {x}) , f : R n → R n f : \mathbb {R}^n \rightarrow \mathbb {R}^n for x ∈ X x \in X , where the set of matrices S S is usually computed as a gradient or by means of slopes. In the following, an expansion scheme is described which frequently yields sharper inclusions for S S . This allows also to compute sharper inclusions for the range of f f over a domain. Roughly speaking, f f has to be given by means of a computer program. The process of expanding f f can then be fully automatized. The function f f need not be differentiable. For locally convex or concave functions special improvements are described. Moreover, in contrast to other methods, x ~ ∩ X \tilde {x} \cap X may be empty without implying large overestimations for S S . This may be advantageous in practical applications.