Lucid

Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems

E. Casablanca, O. Schön, P. Zuliani, S. Soudjani

Motivation

Stochastic dynamical systems

How to learn a safety certificate for a system with unknown stochastic dynamics?

Loading diagram...

Loading diagram...

Loading diagram...

Loading diagram...

Unknown: we don't know the model

Unknown + Noisy: we don't know the model & there is random noise

Stochastic dynamical systems

We are interfacing with

state space $\mathbb{X} \sube \mathbb{R}^{d_x}$ ,
control input space $\mathcal{U} \sube \mathbb{R}^{d_u}$ ,
a probability measure $P_w$ over $\mathcal{W} \sube \mathbb{R}^{d_w}$ ,
a transition function $f: \mathbb{X} \times \mathcal{U} \times \mathcal{W} \to \mathbb{X}$ .

From the current state $x_t \in \mathbb{X}$ and control input $u_t \in \mathcal{U}$ , the next state $x_{t+1} \in \mathbb{X}$ is obtained as

x_{t+1} = f(x_t, u_t, w_t), \quad w_t \sim P_w

Goal

The goal is to find a lower bound on the probability that the system $\mathcal{S}$ satisfies some specification (safety) over a time horizon $T \in \mathbb{N}$ .

Barrier 3 function

Barrier certificates (BCs)

Barrier certificates leverage set invariance to provide safety guarantees.

Barrier certificates (BCs)

Given an initial set $\mathbb{X} \subseteq \mathbb{R}^{d_x}$ and unsafe set $\mathbb{X}_u \subseteq \mathbb{X}$ ,
a barrier certificate is a function $B: \mathbb{X} \to \mathbb{R}$ and constants $\gamma > \eta \ge 0$ , $c \ge 0$ such that

\begin{aligned} & \text{(i) } & & \forall x \in \mathbb{X} & & B(x) \ge 0 \newline & \text{(ii) } & & \forall x_0 \in \mathbb{X}_0 & & B(x_0) \le \eta \newline & \text{(iii) } & & \forall x_u \in \mathbb{X}_u & & B(x_u) \ge \gamma \newline & \text{(iv) } & & \forall x \in \mathbb{X} & & \mathbb{E}[B(x_{t+1})| X = x] - B(x) \le c \end{aligned}

Barrier certificates (BCs)

For any valid barrier and time horizon $T$ , the safety probability is lower bounded by

\mathbb{P}(\text{System safe}) \ge 1 - \frac{\eta - cT}{\gamma}

Barrier 3 contour

Data-driver Barrier Certificates

Data-driven approach
Does not require knowledge of $f$
Learns by sampling 1-step transitions $N \in \mathbb{N}$ times

\begin{array}{c} &\{x_i , u_i , x_{i}^{+} \}_{i = 1}^{N} \newline\newline &x_i^{+} = f(x_i, u_i, w_i), \quad w_i \sim P_w \end{array}

Barrier constraints enforced via empirical CME

Loading diagram...

Spectral abstraction

$\mathcal{H}$ is infinite-dimensional
Gaussian kernel $\approx$ truncated Fourier series expansion
Constraint relaxation via trigonometric bounds on lattices
Can be used in an LP problem

Barrier fourier

Lucid

Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems

C++ for performance and control
Python3 interface for usability
Modular and extensible
Python package (pylucid)
Docker image (ghcr.io/tendto/lucid)
Live demo on the browser

Features

Tool	Guarantees	Data Driven	Stochastic Dyn.	Non-poly Dyn.	Stat. correct.
LUCID	✓	✓	✓	✓	✓
TRUST (2025)	✓	✓	✗	✗	✓
FOSSIL (2024)	✓	✗	✗	✓	`NA`
OMNISAFE (2024)	✗	✓	✓	✓	✗
NPINTERVAL (2023)	✓	✗	✓/✗	✓	`NA`

Main components

Lucid flow

Execution flow

Lucid flow

Architecture

Loading diagram...

Example

Define the system and sample some points.

N = 1000
# Transition function f
f = lambda x: ...

# State space
X_bounds = RectSet((-3, -2), (2.5, 1))
# Initial set
X_i = MultiSet(
    RectSet((1, -0.5), (2, 0.5)),
    RectSet((-1.8, -0.1), (-1.2, 0.1)),
    RectSet((-1.4, -0.5), (-1.2, 0.1)),
)
# Unsafe set
X_u = MultiSet(
    RectSet((0.4, 0.1), (0.6, 0.5)),
    RectSet((0.4, 0.1), (0.8, 0.3))
)

x_samples = X_bounds.sample(N)
# We simulate the next state samples by applying f
xp_samples = f(x_samples)

Loading diagram...

Example

Train the estimator to predict the feature map.

# Create a truncated Fourier feature map
feature_map = LinearTruncatedFourierFeatureMap(
    num_frequencies=7, # Include the 0th frequency
    sigma_f=1.0,
    sigma_l=[0.05, 0.15],
    X_bounds=X_bounds,
)

# Apply the feature map to the samples
xp_features = feature_map(xp_samples)

# Train the estimator
estimator = KernelRidgeRegressor(
    kernel=GaussianKernel(sigma_l=[0.320, 0.157],
                          sigma_f=1.0),
    regularization_constant=1e-8,
)
estimator.fit(x_samples, xp_features)

Loading diagram...

Example

Synthesize the barrier certificate.

# Synthesize the barrier certificate
b = FourierBarrierCertificate(T=5, gamma=1.0)
success = b.synthesize(
    X_bounds=X_bounds,
    X_init=X_init,
    X_unsafe=X_unsafe,
    estimator=estimator,
    feature_map=feature_map,
    lattice_resolution=330,
    parameters=FourierBarrierCertificateParameters(
        set_scaling=0.025,
    ),
)

# [info] Computing LP coefficients
# [info] Optimizing
# [info] Solution found
# [info] Safety probability is 68.08%

Loading diagram...

Live demo

Future work

Tackle NLP directly.
Support STL specifications, not just safety.
Support more kernels, feature maps and estimators.
Extension to control synthesis.
Improved hyperparameter tuning.

References

Lucid Repository
Lucid: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems
Kernel-Based Learning of Safety Barriers: TBA
Data-Driven Safety Verification of Stochastic Systems via Barrier Certificates
Kernel Mean Embedding of Distributions: A Review and Beyond