Reach-Avoid Certificates for Contact-based Stochastic Hybrid Systems
Authors: Tianyi Xia, Ryan K. Cosner
Organizations: GRASP Lab, University of Pennsylvania, PA 19104, USA · the Department of Mechanical Engineering, Tufts University, 419 Boston Avenue, Medford, MA 02155, USA
This work studies certified reach-avoid control of stochastic hybrid systems in which a stochastic differential equation governs continuous flow and a controlled stochastic kernel governs guard-triggered resets. The input appears only in the reset kernel, where it determines the post-jump distribution. Certificates for such systems have so far assumed spontaneous or controller-chosen jump times, a finite horizon, or discrete-time dynamics; we certify, over the infinite horizon, that the target is reached before the unsafe set with at least a prescribed probability. First, we introduce reach-avoid contact certificates, whose flow and jump conditions are imposed only on a sublevel corridor, and prove that any such certificate with a compatible reset policy meets the specification; a pointwise safety filter extends this guarantee from verification to control by constraining arbitrary nominal controllers. Next, we prove that executions are non-Zeno and bound the expected settling time and reset count. We frame certificate search as a linear program over any twice-differentiable dictionary followed by independent verification. We illustrate our approach via comparisons where the certified region is a subset covering 93.6% of the ground truth and where our certificate-based safety filter reaches the goal while reducing collisions from 68 to zero across 200 episodes of a dribbling ball problem.
Figures & tables
Fig. 1 : Example 1. (a) Certificate field V : the certified boundary {V=λ(1−pˉ)} against the true boundary {p=pˉ} from the PDE; the coral strip between them is the conservatism, 6.4% by area, and the rug M marks the support of the reset kernel. (b) Pointwise deficit p−(1−V/λ) against p , with median, percentile bands and per-bin minimum: nonnegative everywhere, median 2.15 pp, median 0.60 pp where p≥0.9 ; in the shaded band V≥λ and no claim is made. Example 2. (c) The degree-8 certificate with the target Xt , the unsafe set Xu (hatched), the guard Γ and the initial set X0 . (d) One shielded recovery against one path under the kernel whose damper fails at every stance. (e) Touchdown energies of 40 shielded paths against the noise-free recursion Ek+1=eEk−ΔEmax . (f) The shield law v+∗(s) inside the admissible takeoff set, bounded by the actuator cap, the pure-leg line and the (B1) floor. (g) Distribution of the contact count. (h) Distribution of the dwell time between contacts.
Fig. 2 : Example 3. (a) The certificate V on rest states; the level V=1 bounds the certified set {p≥0.95} . (b) Closed loop, 40 episodes per policy: the obstacle-blind base against the shielded loop, with the worst-case landing fan of every kick of one shielded episode. (c) V along the kick chains, against the budget V(x0)≤1 of ( C2 ) and the level λ .
Safety-critical control designs controllers that keep physical systems within hard safety constraints despite uncertainty, disturbances, and limited actuation.
Hamilton-Jacobi reachability constructs safety certificates for specified dynamics and safety constraints, tying each certificate to the deployment context for which it is synthesized. We ask whether a single certificate can instead represent a family of context-dependent safety problems and be queried across deployment conditions without re-synthesis. We learn a backward reachable tube for an eight-state vehicle model conditioned on local boundary geometry, friction coefficient, and adversarial disturbance scale. Geometry enters through an ego-frame boundary observation that defines the local containment constraint, while friction and disturbance scale enter as explicit operating-condition variables. This allows the same value function to be queried across friction coefficients from 0.4 to 2.0 and on geometries absent from synthesis. On 11 held-out evaluation geometries, the certificate maintains containment across the full tested friction range, including simultaneous geometry and grip shifts, while remaining within 1.2 percentage points in intervention rate and 0.09 m/s in speed of certificates re-synthesized with knowledge of the test geometry. We then deploy the certificate as a sampled discrete-time control barrier function filter on a full-scale vehicle near the handling limit. Lateral containment holds in every hardware session under both adversarial driving and autonomous racing, with 99th-percentile acceleration magnitude reaching 0.99 g. Across three certificates evaluated under a fixed autonomous racing controller, lap time varies by only 3.1%, demonstrating that a context-conditioned reachability certificate can transfer to deployment geometries absent from synthesis with modest performance cost.
Ali Fuat Sahin, Yunus Yazoglu, John Talbot +3
Ecole Polytechnique Fédérale de Lausanne · Stanford University · Toyota Research Institute
Hybrid dynamical systems provide a powerful modeling framework for robotic systems, particularly in contact-rich environments. However, ensuring safety and performance in such systems remains challenging due to the intricate coupling between continuous dynamics and discrete mode transitions. In this work, we extend classical Hamilton-Jacobi (HJ) reachability analysis, a formal verification method for continuous-time nonlinear systems, to hybrid dynamical systems. Our framework characterizes safe sets for hybrid systems through a generalized value function defined over both discrete and continuous states while accounting for control constraints and model uncertainty. We additionally provide a numerical algorithm to compute this value function. Building on these safe sets, we propose two different mechanisms to integrate performance objectives. First, we introduce a hybrid least-restrictive safety filter that intervenes on both the discrete and continuous components of a nominal controller only when necessary to avoid unsafe states, thereby preserving nominal behavior whenever possible. Second, we formulate and compute hybrid backward reach-avoid tubes, enabling the simultaneous enforcement of safety and goal-reaching behavior, an extension not previously addressed within hybrid HJ reachability. This enables the synthesis of continuous and discrete control policies that guarantee both safety and task completion. We validate our framework through simulation studies and real-world experiments on a quadrupedal robot, demonstrating its effectiveness in hybrid mode planning and safety-critical applications.
Javier Borquez, Shuang Peng, Somil Bansal
Universidad de Santiago de Chile · University of Southern California · Stanford University
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.
Aditya Vats, Tianyi Xia, Nadia Figueroa
The authors are with the University of Pennsylvania, Philadelphia, PA, USA.