Reach-Avoid Certificates for Contact-based Stochastic Hybrid Systems
Abstract
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.
Related
- How suboptimal is my stochastic network controller allowed to be? Completion certificates with application to power grids hosting AI data centers
- Stability Transfer for Autonomous Systems via Higher-Order Taylor-Truncated Lyapunov Certificates
- Closed-Relational Reconstruction Systems: Viability, Observable-History Lifting, and Finite Obstruction Certificates
- Well-posedness result for a stochastic model of contact with adhesion
- Reach-Stabilize Control of Control-Affine Systems with Unknown Affine Parameters
BibTeX
@misc{xia2026reachavoid,
title = {{Reach-Avoid Certificates for Contact-based Stochastic Hybrid Systems}},
author = {Tianyi Xia and Ryan K. Cosner},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.17308},
eprint = {2610.17308},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.17308},
}
RIS
TY - UNPB
TI - Reach-Avoid Certificates for Contact-based Stochastic Hybrid Systems
AU - Tianyi Xia
AU - Ryan K. Cosner
PY - 2026
DA - 2026/10/12
PB - arXiv
DO - 10.48550/arxiv.2610.17308
UR - https://arxiv.org/abs/2610.17308
AB - 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.
ER -