Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Barrier Certificates for Unknown Systems with Latent States and Polynomial Dynamics using Bayesian Inference

Robert Lefringhausen, Sami Leon Noel Aziz Hanna, Elias August, Sandra Hirche

TL;DR

This paper proposes a novel approach for synthesizing barrier certificates for unknown systems with latent states and polynomial dynamics using a Bayesian framework, where a prior in state-space representation is updated using output data via a targeted marginal Metropolis-Hastings sampler.

Abstract

Certifying safety in dynamical systems is crucial, but barrier certificates - widely used to verify that system trajectories remain within a safe region - typically require explicit system models. When dynamics are unknown, data-driven methods can be used instead, yet obtaining a valid certificate requires rigorous uncertainty quantification. For this purpose, existing methods usually rely on full-state measurements, limiting their applicability. This paper proposes a novel approach for synthesizing barrier certificates for unknown systems with latent states and polynomial dynamics. A Bayesian framework is employed, where a prior in state-space representation is updated using output data via a targeted marginal Metropolis-Hastings sampler. The resulting samples are used to construct a barrier certificate through a sum-of-squares program. Probabilistic guarantees for its validity with respect to the true, unknown system are obtained by testing on an additional set of posterior samples. The approach and its probabilistic guarantees are illustrated through a numerical simulation.

Barrier Certificates for Unknown Systems with Latent States and Polynomial Dynamics using Bayesian Inference

TL;DR

This paper proposes a novel approach for synthesizing barrier certificates for unknown systems with latent states and polynomial dynamics using a Bayesian framework, where a prior in state-space representation is updated using output data via a targeted marginal Metropolis-Hastings sampler.

Abstract

Certifying safety in dynamical systems is crucial, but barrier certificates - widely used to verify that system trajectories remain within a safe region - typically require explicit system models. When dynamics are unknown, data-driven methods can be used instead, yet obtaining a valid certificate requires rigorous uncertainty quantification. For this purpose, existing methods usually rely on full-state measurements, limiting their applicability. This paper proposes a novel approach for synthesizing barrier certificates for unknown systems with latent states and polynomial dynamics. A Bayesian framework is employed, where a prior in state-space representation is updated using output data via a targeted marginal Metropolis-Hastings sampler. The resulting samples are used to construct a barrier certificate through a sum-of-squares program. Probabilistic guarantees for its validity with respect to the true, unknown system are obtained by testing on an additional set of posterior samples. The approach and its probabilistic guarantees are illustrated through a numerical simulation.

Paper Structure

This paper contains 9 sections, 2 theorems, 21 equations, 3 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Problem Formulation
  3. Marginal Metropolis--Hastings Sampling
  4. Synthesis and Validation of Barrier Certificates
  5. Barrier Conditions for Invariant Sets
  6. Sum-of-Squares Implementation
  7. Validation and Guarantees
  8. Simulation
  9. Conclusion

Key Result

Lemma 1

If there exists a polynomial function $h(\cdot)$ satisfying the inequality eq:barrier_condition for all $\bm{x} \in \mathcal{X}_{\text{max}}$, and polynomial functions $h_{\text{min}}(\cdot)$ and $h_{\text{max}}(\cdot)$ satisfying eq:set_polynomials, such that then, there exists the set that is forward invariant and satisfies $\mathcal{X}_\text{min}\subset \mathcal{C} \subseteq \mathcal{X}_{\tex

Figures (3)

  • Figure 1: Illustration of the constraint $\mathcal{X}_{\text{min}} \subset \mathcal{C} \subseteq \mathcal{X}_{\text{max}}$. The outer set $\mathcal{X}_{\text{max}}$ defines the allowable region for the forward-invariant set $\mathcal{C}$, while the inner set $\mathcal{X}_{\text{min}}$ specifies states that must be included in $\mathcal{C}$.
  • Figure 2: Normalized autocorrelation function (ACF) of successive samples generated by the MMH sampler without thinning. The red, yellow, and green lines correspond to the ACFs of the sampled values for $\theta_1$, $\theta_2$, and $\theta_3$, respectively.
  • Figure 3: Visualization of the obtained forward-invariant set. The red curve marks the boundary of the set $\mathcal{C}$. Red arrows illustrate the system state one step into the future from selected points on this boundary, indicating inward motion. The circular regions $\mathcal{X}_\text{min}$ and $\mathcal{X}_\text{max}$ are shown in green and grey, respectively. The yellow curve depicts the system’s limit cycle, which lies entirely within $\mathcal{C}$.

Theorems & Definitions (9)

  • Definition 1
  • Remark 1
  • Remark 2
  • Lemma 1
  • proof
  • Remark 3
  • Remark 4
  • Theorem 1
  • proof