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

• URL: http://arxiv.org/abs/2504.01807v1
• Date: Wed, 02 Apr 2025 15:12:34 GMT
• Title: Barrier Certificates for Unknown Systems with Latent States and Polynomial Dynamics using Bayesian Inference
• Authors: Robert Lefringhausen, Sami Leon Noel Aziz Hanna, Elias August, Sandra Hirche,
• Abstract summary: This paper proposes a novel approach for synthesizing barrier certificates for unknown systems.<n>A prior in state-space representation is updated using input-output data via a targeted marginal Metropolis-Hastings sampler.<n>It is shown that if the candidate satisfies the required conditions on a test set of additional samples, it is also valid for the true, unknown system with high probability.
• Score: 3.0839725524711774
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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 input-output data via a targeted marginal Metropolis-Hastings sampler. The resulting samples are used to construct a candidate barrier certificate through a sum-of-squares program. It is shown that if the candidate satisfies the required conditions on a test set of additional samples, it is also valid for the true, unknown system with high probability. The approach and its probabilistic guarantees are illustrated through a numerical simulation.

Related papers

• Data-Driven Safety Verification using Barrier Certificates and Matrix Zonotopes [1.6078581568133972]
  We propose a data-driven safety verification framework to verify system safety directly from noisy data.<n>Instead of trusting a single unreliable model, we construct a set of models that align with the observed data.<n>This model set is compactly represented using matrix zonotopes, enabling efficient computation and propagation of uncertainty.
  arXiv  Detail & Related papers  (2025-04-01T17:46:42Z)
• Safe Reach Set Computation via Neural Barrier Certificates [46.1784503246807]
  We present a novel technique for online safety verification of autonomous systems. Our approach uses barrier certificates given by parameterized neural networks that depend on a given initial set, unsafe sets, and time horizon. Such networks are trained efficiently offline using system simulations sampled from regions of the state space.
  arXiv  Detail & Related papers  (2024-04-29T15:49:37Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• User-defined Event Sampling and Uncertainty Quantification in Diffusion Models for Physical Dynamical Systems [49.75149094527068]
  We show that diffusion models can be adapted to make predictions and provide uncertainty quantification for chaotic dynamical systems. We develop a probabilistic approximation scheme for the conditional score function which converges to the true distribution as the noise level decreases. We are able to sample conditionally on nonlinear userdefined events at inference time, and matches data statistics even when sampling from the tails of the distribution.
  arXiv  Detail & Related papers  (2023-06-13T03:42:03Z)
• Learning-Based Optimal Control with Performance Guarantees for Unknown Systems with Latent States [4.4820711784498]
  This paper proposes a novel method for the computation of an optimal input trajectory for unknown nonlinear systems with latent states. The effectiveness of the proposed method is demonstrated in a numerical simulation.
  arXiv  Detail & Related papers  (2023-03-31T11:06:09Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)
• Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise [59.47042225257565]
  We present a novel planning method that does not rely on any explicit representation of the noise distributions. First, we abstract the continuous system into a discrete-state model that captures noise by probabilistic transitions between states. We capture these bounds in the transition probability intervals of a so-called interval Markov decision process (iMDP)
  arXiv  Detail & Related papers  (2021-10-25T06:18:55Z)
• SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
  We study the verification of parameterised multi-agent systems (MASs) In particular, we study whether unwanted states, characterised as a given state formula, are reachable in a given MAS.
  arXiv  Detail & Related papers  (2020-08-11T15:24:05Z)
• Efficient statistical validation with edge cases to evaluate Highly Automated Vehicles [6.198523595657983]
  The widescale deployment of Autonomous Vehicles seems to be imminent despite many safety challenges that are yet to be resolved. Existing standards focus on deterministic processes where the validation requires only a set of test cases that cover the requirements. This paper presents a new approach to compute the statistical characteristics of a system's behaviour by biasing automatically generated test cases towards the worst case scenarios.
  arXiv  Detail & Related papers  (2020-03-04T04:35:22Z)

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.