Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression

Read original: arXiv:2201.00655 - Published 7/17/2024 by John Skovbekk, Luca Laurenti, Eric Frew, Morteza Lahijanian

↗️

Overview

This research paper presents a framework for verifying the behavior of discrete-time dynamical systems with uncertain, unmodeled dynamics and noisy measurements against temporal logic specifications.
The framework uses Gaussian process (GP) regression to learn the unknown system dynamics from input-output data, and then abstracts the continuous-space system as a finite-state, uncertain Markov decision process (MDP).
The uncertain MDP abstraction is then verified against the given temporal logic specification using existing model checking tools.
The computational complexity of the framework is shown to be polynomial in the size of the dataset and discrete abstraction, with a trade-off between the quality of the verification results and the computational burden.
The framework is demonstrated on several case studies involving linear, nonlinear, and switched dynamical systems.

Plain English Explanation

The paper focuses on verifying the behavior of autonomous systems that operate in safety-critical scenarios, where there may be uncertainties and unknown factors that influence the system's dynamics. To address this challenge, the researchers developed a framework that can learn the system's dynamics from input-output data and then verify the system's behavior against specific requirements, expressed as temporal logic specifications.

The key idea is to use Gaussian process regression to learn the unknown dynamics of the system from the available data. This allows the researchers to abstract the continuous-time system as a discrete-time, finite-state Markov decision process (MDP) that captures the uncertainty in the system's behavior.

The researchers then use existing model checking tools to verify the uncertain MDP abstraction against the given temporal logic specification. This approach allows them to extend the verification results from the abstraction to the underlying system, providing a way to ensure the system's safety and reliability in the presence of uncertainties and unmodeled dynamics.

The framework's computational complexity is shown to be polynomial in the size of the dataset and the discrete abstraction, which means it can be applied to larger, more complex systems. However, there is a trade-off between the quality of the verification results and the computational burden, as finer abstractions and larger datasets require more computational resources.

Technical Explanation

The paper presents a framework for verifying the behavior of discrete-time dynamical systems with unmodeled dynamics and noisy measurements against temporal logic specifications. The key components of the framework are:

Gaussian Process (GP) Regression: The framework employs GP regression to learn the unknown system dynamics from an input-output dataset. This allows the continuous-space system to be abstracted as a finite-state, uncertain Markov decision process (MDP).
Uncertain MDP Abstraction: The continuous-space system is abstracted as a finite-state, uncertain MDP by discretizing the state space and computing transition probability intervals. The uncertainty in the MDP abstraction comes from the error in GP regression and the discretization process.
Verification: The uncertain MDP abstraction is then verified against the given temporal logic specification using existing model checking tools. The researchers establish the correctness of extending the verification results from the abstraction to the underlying system.
Complexity Analysis: The computational complexity of the framework is shown to be polynomial in the size of the dataset and the discrete abstraction. This analysis illustrates a trade-off between the quality of the verification results and the computational burden.

The framework is demonstrated on several case studies involving linear, nonlinear, and switched dynamical systems, showcasing its ability to handle a variety of system dynamics.

Critical Analysis

The paper presents a comprehensive framework for verifying the behavior of autonomous systems with uncertain, unmodeled dynamics. The use of Gaussian process regression to learn the unknown system dynamics is a particularly novel and effective approach, as it allows the complex continuous-time system to be abstracted as a finite-state MDP that can be efficiently verified.

However, the paper does acknowledge some limitations and areas for further research. For example, the discretization process used to create the MDP abstraction can introduce additional sources of error, and the trade-off between the quality of the verification results and computational complexity may limit the scalability of the approach for very large or high-dimensional systems.

Additionally, the paper does not address the potential challenges of obtaining a representative dataset for learning the system dynamics, or the impact of model mismatch or other sources of uncertainty that may not be captured by the GP regression. Further research could explore ways to incorporate these considerations into the verification framework.

Despite these limitations, the paper presents a valuable contribution to the field of autonomous system verification, and the proposed framework could be a useful tool for ensuring the safety and reliability of critical systems operating in uncertain environments.

Conclusion

This research paper introduces a framework for verifying the behavior of discrete-time dynamical systems with uncertain, unmodeled dynamics and noisy measurements against temporal logic specifications. The key innovation is the use of Gaussian process regression to learn the unknown system dynamics, which allows the continuous-time system to be abstracted as a finite-state, uncertain Markov decision process that can be efficiently verified using existing model checking tools.

The framework's computational complexity is shown to be polynomial in the size of the dataset and discrete abstraction, making it scalable to larger, more complex systems. However, there is a trade-off between the quality of the verification results and the computational burden, which may limit the approach's applicability in certain scenarios.

Overall, this framework represents an important step forward in the field of autonomous system verification, providing a principled way to ensure the safety and reliability of critical systems operating in the presence of uncertainties and unmodeled dynamics. The insights and techniques presented in this paper could have far-reaching implications for the development of next-generation autonomous systems across a variety of industries and applications.

This summary was produced with help from an AI and may contain inaccuracies - check out the links to read the original source documents!

Follow @aimodelsfyi on 𝕏 →

Related Papers

↗️

Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression

John Skovbekk, Luca Laurenti, Eric Frew, Morteza Lahijanian

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.

7/17/2024

Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification

Oliver Schon, Shammakh Naseer, Ben Wooding, Sadegh Soudjani

To advance formal verification of stochastic systems against temporal logic requirements for handling unknown dynamics, researchers have been designing data-driven approaches inspired by breakthroughs in the underlying machine learning techniques. As one promising research direction, abstraction-based solutions based on Gaussian process (GP) regression have become popular for their ability to learn a representation of the latent system from data with a quantified error. Results obtained based on this model are then translated to the true system via various methods. In a recent publication, GPs using a so-called binary-tree kernel have demonstrated a polynomial speedup w.r.t. the size of the data compared to their vanilla version, outcompeting all existing sparse GP approximations. Incidentally, the resulting binary-tree Gaussian process (BTGP) is characteristic for its piecewise-constant posterior mean and covariance functions, naturally abstracting the input space into discrete partitions. In this paper, we leverage this natural abstraction of the BTGP for formal verification, eliminating the need for cumbersome abstraction and error quantification procedures. We show that the BTGP allows us to construct an interval Markov chain model of the unknown system with a speedup that is polynomial w.r.t. the size of the abstraction compared to alternative approaches. We provide a delocalized error quantification via a unified formula even when the true dynamics do not live in the function space of the BTGP. This allows us to compute upper and lower bounds on the probability of satisfying reachability specifications that are robust to both aleatoric and epistemic uncertainties.

8/1/2024

A Black-Box Physics-Informed Estimator based on Gaussian Process Regression for Robot Inverse Dynamics Identification

Giulio Giacomuzzos, Ruggero Carli, Diego Romeres, Alberto Dalla Libera

Learning the inverse dynamics of robots directly from data, adopting a black-box approach, is interesting for several real-world scenarios where limited knowledge about the system is available. In this paper, we propose a black-box model based on Gaussian Process (GP) Regression for the identification of the inverse dynamics of robotic manipulators. The proposed model relies on a novel multidimensional kernel, called textit{Lagrangian Inspired Polynomial} (kernelInitials{}) kernel. The kernelInitials{} kernel is based on two main ideas. First, instead of directly modeling the inverse dynamics components, we model as GPs the kinetic and potential energy of the system. The GP prior on the inverse dynamics components is derived from those on the energies by applying the properties of GPs under linear operators. Second, as regards the energy prior definition, we prove a polynomial structure of the kinetic and potential energy, and we derive a polynomial kernel that encodes this property. As a consequence, the proposed model allows also to estimate the kinetic and potential energy without requiring any label on these quantities. Results on simulation and on two real robotic manipulators, namely a 7 DOF Franka Emika Panda, and a 6 DOF MELFA RV4FL, show that the proposed model outperforms state-of-the-art black-box estimators based both on Gaussian Processes and Neural Networks in terms of accuracy, generality and data efficiency. The experiments on the MELFA robot also demonstrate that our approach achieves performance comparable to fine-tuned model-based estimators, despite requiring less prior information.

9/9/2024

Wiener Chaos in Kernel Regression: Towards Untangling Aleatoric and Epistemic Uncertainty

T. Faulwasser, O. Molodchyk

Gaussian Processes (GPs) are a versatile method that enables different approaches towards learning for dynamics and control. Gaussianity assumptions appear in two dimensions in GPs: The positive semi-definite kernel of the underlying reproducing kernel Hilbert space is used to construct the co-variance of a Gaussian distribution over functions, while measurement noise (i.e. data corruption) is usually modeled as i.i.d. additive Gaussians. In this note, we generalize the setting and consider kernel ridge regression with additive i.i.d. non-Gaussian measurement noise. To apply the usual kernel trick, we rely on the representation of the uncertainty via polynomial chaos expansions, which are series expansions for random variables of finite variance introduced by Norbert Wiener. We derive and discuss the analytic $mathcal{L}^2$ solution to the arising Wiener kernel regression. Considering a polynomial dynamic system as a numerical example, we show that our approach allows us to distinguish the uncertainty that stems from the noise in the data samples from the total uncertainty encoded in the GP posterior distribution.

9/14/2024