VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change

TL;DR

VeRecycle tackles the costly re-certification problem for probabilistic neural reach-avoid certificates under localized dynamics changes in discrete-time stochastic systems. It formalizes a tight link between the reclaimable threshold $\widetilde{\rho}$ and the infimum $\inf\{C(\mathbb{X}_{?})\}$ of the original certificate on the changed region, and provides an exact solution plus sound interval-based approximations. The framework supports compositional control by reclaiming per-edge guarantees and recombining them via a shortest-path optimization to obtain a new global bound. Empirical results on the Stochastic Nine Rooms task show substantial computational savings with competitive probabilistic guarantees, enabling flexible, scalable deployment of learning-based certificates in environments with localized changes.

Abstract

Autonomous systems operating in the real world encounter a range of uncertainties. Probabilistic neural Lyapunov certification is a powerful approach to proving safety of nonlinear stochastic dynamical systems. When faced with changes beyond the modeled uncertainties, e.g., unidentified obstacles, probabilistic certificates must be transferred to the new system dynamics. However, even when the changes are localized in a known part of the state space, state-of-the-art requires complete re-certification, which is particularly costly for neural certificates. We introduce VeRecycle, the first framework to formally reclaim guarantees for discrete-time stochastic dynamical systems. VeRecycle efficiently reuses probabilistic certificates when the system dynamics deviate only in a given subset of states. We present a general theoretical justification and algorithmic implementation. Our experimental evaluation shows scenarios where VeRecycle both saves significant computational effort and achieves competitive probabilistic guarantees in compositional neural control.

Figures (3)

• Figure 1: A probabilistic certificate (color gradient) for a navigation subtask ${\color{yellow}4\:\square}$ (yellow) $\rightarrow$${\color{green}5\:\square}$ (green), with darker color indicating higher probability of the system (with trajectories sampled in white) to complete the subtask while avoiding the walls (outlined in red). Dashed line shows original certified probability threshold, solid line shows threshold reclaimed by VeRecycle after a localized change in the system's dynamics (slanted blue pattern).
• Figure 2: A compositional policy (blue) for a decomposed reach-avoid task: $0$ (yellow) $\rightarrow 8$ (green). Vertices are discrete abstractions of the rooms in the continuous environment. A directed edge signifies the existence of a certified policy between two rooms. Updated thresholds (black; original in red) reveal that the old path (red edges) no longer maximizes the global probability threshold.
• Figure 3: Example of a "loose" original certificate (gradient left) refined by baseline algorithm (gradient right) to obtain an updated threshold $\widetilde{\rho_{}}_{}$ (solid line) closer to the original $\rho_{}$ (dashed line). Yellow ($\mathbb{X}_{0}$), green ($\mathbb{X}_{\star}$), red ($\mathbb{X}_{\oslash}$), and blue ($\mathbb{X}_{?}$) denote task sets.

Theorems & Definitions (23)

• Example 1
• Definition 1
• Example 2
• Definition 2: zikelic_learning_2023
• Definition 3
• Example 3: Example \ref{['ex:nine-rooms-prelim-monolithic']} continued
• Lemma 1: Lower bound of $\widetilde{\rho_{}}_{}$
• Lemma 2: Upper bound of $\widetilde{\rho_{}}_{}$
• Lemma 3
• Theorem 1: Equality to $\widetilde{\rho_{}}_{}$