Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression

• URL: http://arxiv.org/abs/2201.00655v2
• Date: Tue, 16 Jul 2024 17:33:04 GMT
• Title: Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression
• Authors: John Skovbekk, Luca Laurenti, Eric Frew, Morteza Lahijanian,
• Abstract summary: Leveraging autonomous systems in safety-critical scenarios requires verifying their behaviors in the presence of uncertainties. We develop a framework for verifying discrete-time dynamical systems with unmodelled dynamics and noisy measurements.
• Score: 11.729744197698718
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Leveraging autonomous systems in safety-critical scenarios requires verifying their behaviors in the presence of uncertainties and black-box components that influence the system dynamics. In this work, we develop a framework for verifying discrete-time dynamical systems with unmodelled dynamics and noisy measurements against temporal logic specifications from an input-output dataset. The verification framework employs Gaussian process (GP) regression to learn the unknown dynamics from the dataset and abstracts the continuous-space system as a finite-state, uncertain Markov decision process (MDP). This abstraction relies on space discretization and transition probability intervals that capture the uncertainty due to the error in GP regression by using reproducible kernel Hilbert space analysis as well as the uncertainty induced by discretization. The framework utilizes existing model checking tools for verification of the uncertain MDP abstraction against a given temporal logic specification. We establish the correctness of extending the verification results on the abstraction created from noisy measurements to the underlying system. We show that the computational complexity of the framework is polynomial in the size of the dataset and discrete abstraction. The complexity analysis illustrates a trade-off between the quality of the verification results and the computational burden to handle larger datasets and finer abstractions. Finally, we demonstrate the efficacy of our learning and verification framework on several case studies with linear, nonlinear, and switched dynamical systems.

Related papers

• VENI, VINDy, VICI: a variational reduced-order modeling framework with uncertainty quantification [4.804365706049767]
  We present a data-driven, non-intrusive framework for building reduced-order models (ROMs) In detail, the method consists of Variational SINI to identify the distribution of reduced coordinates. Once trained offline, the identified model can be queried for new parameter instances and new initial conditions to compute the corresponding full-time solutions.
  arXiv  Detail & Related papers  (2024-05-31T15:16:48Z)
• InVAErt networks: a data-driven framework for model synthesis and identifiability analysis [0.0]
  inVAErt is a framework for data-driven analysis and synthesis of physical systems. It uses a deterministic decoder to represent the forward and inverse maps, a normalizing flow to capture the probabilistic distribution of system outputs, and a variational encoder to learn a compact latent representation for the lack of bijectivity between inputs and outputs.
  arXiv  Detail & Related papers  (2023-07-24T07:58:18Z)
• Bayesian Spline Learning for Equation Discovery of Nonlinear Dynamics with Quantified Uncertainty [8.815974147041048]
  We develop a novel framework to identify parsimonious governing equations of nonlinear (spatiotemporal) dynamics from sparse, noisy data with quantified uncertainty. The proposed algorithm is evaluated on multiple nonlinear dynamical systems governed by canonical ordinary and partial differential equations.
  arXiv  Detail & Related papers  (2022-10-14T20:37:36Z)
• A Causality-Based Learning Approach for Discovering the Underlying Dynamics of Complex Systems from Partial Observations with Stochastic Parameterization [1.2882319878552302]
  This paper develops a new iterative learning algorithm for complex turbulent systems with partial observations. It alternates between identifying model structures, recovering unobserved variables, and estimating parameters. Numerical experiments show that the new algorithm succeeds in identifying the model structure and providing suitable parameterizations for many complex nonlinear systems.
  arXiv  Detail & Related papers  (2022-08-19T00:35:03Z)
• Capturing Actionable Dynamics with Structured Latent Ordinary Differential Equations [68.62843292346813]
  We propose a structured latent ODE model that captures system input variations within its latent representation. Building on a static variable specification, our model learns factors of variation for each input to the system, thus separating the effects of the system inputs in the latent space.
  arXiv  Detail & Related papers  (2022-02-25T20:00:56Z)
• A Priori Denoising Strategies for Sparse Identification of Nonlinear Dynamical Systems: A Comparative Study [68.8204255655161]
  We investigate and compare the performance of several local and global smoothing techniques to a priori denoise the state measurements. We show that, in general, global methods, which use the entire measurement data set, outperform local methods, which employ a neighboring data subset around a local point.
  arXiv  Detail & Related papers  (2022-01-29T23:31:25Z)
• Leveraging the structure of dynamical systems for data-driven modeling [111.45324708884813]
  We consider the impact of the training set and its structure on the quality of the long-term prediction. We show how an informed design of the training set, based on invariants of the system and the structure of the underlying attractor, significantly improves the resulting models.
  arXiv  Detail & Related papers  (2021-12-15T20:09:20Z)
• Structure-Preserving Learning Using Gaussian Processes and Variational Integrators [62.31425348954686]
  We propose the combination of a variational integrator for the nominal dynamics of a mechanical system and learning residual dynamics with Gaussian process regression. We extend our approach to systems with known kinematic constraints and provide formal bounds on the prediction uncertainty.
  arXiv  Detail & Related papers  (2021-12-10T11:09:29Z)
• Stochastically forced ensemble dynamic mode decomposition for forecasting and analysis of near-periodic systems [65.44033635330604]
  We introduce a novel load forecasting method in which observed dynamics are modeled as a forced linear system. We show that its use of intrinsic linear dynamics offers a number of desirable properties in terms of interpretability and parsimony. Results are presented for a test case using load data from an electrical grid.
  arXiv  Detail & Related papers  (2020-10-08T20:25:52Z)
• Active Learning for Nonlinear System Identification with Guarantees [102.43355665393067]
  We study a class of nonlinear dynamical systems whose state transitions depend linearly on a known feature embedding of state-action pairs. We propose an active learning approach that achieves this by repeating three steps: trajectory planning, trajectory tracking, and re-estimation of the system from all available data. We show that our method estimates nonlinear dynamical systems at a parametric rate, similar to the statistical rate of standard linear regression.
  arXiv  Detail & Related papers  (2020-06-18T04:54:11Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.