Dynamical Systems (DS) are reactive motion policies representing vector fields trained with theoretical guarantees of stability and convergence. To ensure safety during deployment in unknown environments they must be locally reshaped, either through modulation or geometric control barrier function strategies. However, depending on the geometry of the obstacles and the complexity of the DS, these local strategies can lead the system to unavoidable collisions or spurious attractors. In this work, we certify safety with a value function drawn from the notion of backward reachability tube, which measures the worst-case safety along a rollout trajectory of the nominal DS. Usually, such a value function is intractable for a controlled system due to curse of dimensionality. We show that in the DS-based learning-from-demonstration setting, the absence of a control input collapses the reachability problem to a deterministic rollout, and the presence of certain stability conditions truncates the infinite horizon to a finite one, resulting in a well-defined value function. We further show that the value function we devised is the maximal forward-invariant subset of the obstaclefree region for the nominal DS flow. The application of this certificate function is validated across five DS constructions - analytical, Neural ODE, diffeomorphic latent space, LPV-DS, SE(3)and validate it on a Franka manipulator. Modulation and geometric CBFs also suffer from saddle point in cases of headon approach towards an unsafe zone. We show that CBF-on-V avoids this pitfall entirely.
Figures & tables
Fig. 1 : Head-on behavior on a star obstacle. Background shading is the safety margin h=Γ−1 (red: obstacle interior, blue: free space, opacity: distance to the boundary). Dots are far initial conditions, diamonds are on-obstacle initial conditions on the head-on arc, × marks the spurious equilibrium, and the star is the goal; black/teal trajectories reach the goal, red trajectories are trapped. (a) Reference modulation: the head-on line and one surface seed fall into a saddle . (b) CBF-on- h : a spurious attractor whose basin traps the far starts and the whole notch arc of surface seeds. (c) Stacked CBF-on- V + hard- h (ours): every start, on-obstacle or far, is steered around to the goal while keeping h≥0 .
Fig. 2 : Main results across the four DS constructions. In each panel the nominal (dashed) and filtered (solid) rollouts are overlaid on the reachability value landscape V , with the obstacle marked; only the computation of V changes between panels, the filter (Eq. ( 12 )) is identical. (a) Spiral DS with closed-form V : the nominal arc enters the obstacle, the filtered rollout rides the {V=0} boundary and converges. (b) Neural-ODE DS with a learned value network on a LASA shape (JShape): four initial conditions shown, three with V(x0)<0 and one with V(x0)≥0 , each nominal/filtered pair in the same colour. (c) LPV-DS with the certified exponential rate of αL=minkλmin(Mk)/λmax(P) as noted in section V-D . (d)-(e) Diffeomorphic latent DS: the certificate is enforced in latent space (d) and the same four rollouts are shown pulled back through ψ−1 into task space (e).
Fig. 3 : Three filters on the spiral DS from the same initial condition over the same obstacle acting on a nominally safe trajectory that grazes by the obstacle. CBF-on- V (ours) coincides with the nominal, while CBF-on- h and modulation deflect a trajectory that was already safe. Bottom: the three correction magnitudes ∥u(t)∥ for the rollout sequence.
Metric
CBF-on- V (ours)
CBF-on- h
mod.
Intervention rate
0 [2pt] (never activates)
0.041
0.278
Total effort
0.288
0.300
Peak correction
0.552
0.492
Path deviation
0.692
0.365
TABLE I : Filter behaviour on the spiral DS. They differ in intervention. CBF-on- V never activates as nominal trajectory is already safe. Metrics: intervention rate =#{∥u∥>ϵ}/N ; total effort =∫∥u∥dt ; peak =maxt∥u∥ ; path deviation =∫∥xfilt−xnom∥dt ;
Fig. 4 : Reactive avoidance of a hand-moved obstacle on the Franka for two SE(3) skills. Top: video frames at t=0–3 . Bottom: nominal (grey dashed) and filtered end-effector paths, the latter coloured by the task-space correction ∥u∥ ; the mocap-tracked obstacle is a time-graded red trail, solid at closest approach.
Bottle-to-shelf
Pouring
Plate std.-to-lying
Metric
ours
CBF- h
ours
CBF- h
ours
CBF- h
Intervention lead (s) ↑
2.12
0.11
1.11
0.12
0.86
0.12
Correction-active fraction ↓
0.067
0.095
0.239
0.322
0.205
0.139
Boundary distance (cm) ↓
13.6
34.8
34.4
42.4
20.9
33.3
Command jerk RMS (m/s 3 ) ↓
163
460
281
1104
85
92
TABLE II : SE(3) hardware: reachability filter (CBF-on- V , ours) vs. geometric distance CBF (CBF-on- h ) on the same learned policy per task; no collision in any run. Arrows give the better direction; best per task/metric in bold.
The goal of this paper is certifying safety of dynamical systems subject to uncertainty. Existing approaches use trajectory data to estimate transition probabilities, and compute safety probabilities recursively via dynamic programming (DP). This recursion may lead to compounding errors in the certified safety probability, thus collapsing to a vacuous lower bound for growing horizons T. We propose a kernel embedding framework that treats safety certification as a classification problem on trajectory data, directly estimating the T-step safety probability without recursion. We show that the framework subsumes well-established approaches from the literature (e.g., barrier certificates, robust Markov models) as special cases, and allows us to go beyond their limitations. As the main consequence, it bypasses compounding error across the horizon and enables certification for systems with non-Markovian dynamics. We demonstrate that direct estimators remain stable independent of the certification horizon and in the non-Markovian setting, whilst DP-based certificates silently go unsound -- confirmed in simulation on a neural-controlled quadrotor.
Oliver Schön, Licio Romao, Sadegh Soudjani
ETH Zürich · Zürich, Switzerland · Technical University of Denmark +3
Barrier certificates are scalar functions over the state space of dynamical systems that separate all unsafe states from all reachable states. The existence of a barrier certificate formally verifies the safety of the dynamical system. Recent approaches synthesize barrier certificates by iteratively training a neural network. In each iteration, the candidate is formally verified - if successful, the barrier certificate is found. Instead, we propose a set-based training approach that tightly integrates verification into training via a set-based loss function that soundly encodes all barrier certificate properties. A loss of zero formally proves the validity of the barrier certificate, collapsing the iterative training and verification into a single training procedure. Our experiments demonstrate that our set-based training approach scales well with the system dimension and naturally handles complex nonlinear dynamics.
Safety of stochastic dynamic systems in environments with dynamic obstacles is studied in this paper through the lens of stochastic barrier functions. We introduce both time-invariant and time-varying barrier certificates for discrete-time, continuous-space systems subject to uncertainty, which provide certified lower bounds on the probability of remaining within a safe set over a finite horizon. These certificates explicitly account for time-varying unsafe regions induced by obstacle dynamics. By leveraging Bellman's optimality perspective, the time-varying formulation directly captures temporal structure and yields less conservative bounds than state-of-the-art approaches. By restricting certificates to polynomial functions, we show that time-varying barrier synthesis can be formulated as a convex sum-of-squares program, enabling tractable optimization. Empirical evaluations on nonlinear systems with dynamic obstacles show that time-varying certificates consistently achieve tight guarantees, demonstrating improved accuracy and scalability over state-of-the-art methods.
Rayan Mazouz, Luca Laurenti, Morteza Lahijanian
Dept. of Aerospace Eng. Sciences at University of Colorado Boulder, USA · Delft University of Technology, The Netherlands