Data-driven Safety Verification of Stochastic Systems via Barrier Certificates

TL;DR

This paper introduces a data-driven method for safety verification of unknown stochastic systems using barrier certificates, formulating the problem as a scenario convex program to provide probabilistic safety guarantees.

Contribution

It develops a novel framework that combines barrier certificates with data-driven scenario convex programming for safety verification of unknown stochastic systems.

Findings

Successfully verified safety of a room temperature system using collected data.

Provided probabilistic safety guarantees with confidence levels.

Demonstrated the approach on a real-world temperature control system.

Abstract

In this paper, we propose a data-driven approach to formally verify the safety of (potentially) unknown discrete-time continuous-space stochastic systems. The proposed framework is based on a notion of barrier certificates together with data collected from trajectories of unknown systems. We first reformulate the barrier-based safety verification as a robust convex problem (RCP). Solving the acquired RCP is hard in general because not only the state of the system lives in a continuous set, but also and more problematic, the unknown model appears in one of the constraints of RCP. Instead, we leverage a finite number of data, and accordingly, the RCP is casted as a scenario convex problem (SCP). We then relate the optimizer of the SCP to that of the RCP, and consequently, we provide a safety guarantee over the unknown stochastic system with a priori guaranteed confidence. We apply our approach to an unknown room temperature system by collecting sampled data from trajectories of the system and verify formally that temperature of the room lies in a comfort zone for a finite time horizon with a desired confidence.