Tractable higher-order under-approximating AE extensions for non-linear systems
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.
Code (1)
Similar Papers 제목 키워드 기반
Perturbative Corrections for Approximate Inference in Gaussian Latent Variable Models
Expectation Propagation (EP) provides a framework for approximate inference. When the model under consideration is over a latent Gaussian field, with the approximation being Gaussian, we show how these approximations can…
On MAP Inference by MWSS on Perfect Graphs
Finding the most likely (MAP) configuration of a Markov random field (MRF) is NP-hard in general. A promising, recent technique is to reduce the problem to finding a maximum weight stable set (MWSS) on a derived weighted…
Exact Inference for Continuous-Time Gaussian Process Dynamics
Physical systems can often be described via a continuous-time dynamical system. In practice, the true system is often unknown and has to be learned from measurement data. Since data is typically collected in discrete tim…
Variational InferenceExact Bayesian Gaussian Cox Processes Using Random Integral
A Gaussian Cox process is a popular model for point process data, in which the intensity function is a transformation of a Gaussian process. Posterior inference of this intensity function involves an intractable integral…
Data AugmentationPoint ProcessesThe Higher-Order Prover Leo-III (Extended Version)
The automated theorem prover Leo-III for classical higher-order logic with Henkin semantics and choice is presented. Leo-III is based on extensional higher-order paramodulation and accepts every common TPTP dialect (FOF,…