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.