Tractable higher-order under-approximating AE extensions for non-linear systems

TL;DR

This paper introduces a novel framework for efficiently computing under- and over-approximations of the images of vector-valued functions, enhancing the analysis of reachable sets in uncertain non-linear systems for verification and falsification.

Contribution

It extends classical precision refinement techniques to under-approximations, enabling better analysis of non-linear dynamical systems with inputs and disturbances.

Findings

Framework effectively computes robust ranges of functions.

Improves precision of reachable set estimations.

Demonstrates efficiency on benchmark examples.

Abstract

We consider the problem of under and over-approximating the image of general vector-valued functions over bounded sets, and apply the proposed solution to the estimation of reachable sets of uncertain non-linear discrete-time dynamical systems. Such a combination of under and over-approximations is very valuable for the verification of properties of embedded and cyber-physical controlled systems. Over-approximations prove properties correct, while under-approximations can be used for falsification. Coupled, they provide a measure of the conservatism of the analysis. This work introduces a general framework relying on computations of robust ranges of vector-valued functions. This framework allows us to extend for under-approximation many precision refinements that are classically used for over-approximations, such as affine approximations, Taylor models, quadrature formulae and preconditioning methods. We end by evaluating the efficiency and precision of our approach, focusing on the application to the analysis of discrete-time dynamical systems with inputs and disturbances, on different examples from the literature.