Saved in:
Bibliographic Details
Main Authors: Lutz, Sterre, Spaan, Matthijs T. J., Lukina, Anna
Format: Preprint
Published: 2025
Subjects:
Online Access:https://arxiv.org/abs/2505.14001
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866912383092391936
author Lutz, Sterre
Spaan, Matthijs T. J.
Lukina, Anna
author_facet Lutz, Sterre
Spaan, Matthijs T. J.
Lukina, Anna
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2505_14001
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change
Lutz, Sterre
Spaan, Matthijs T. J.
Lukina, Anna
Artificial Intelligence
Systems and Control
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.
title VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change
topic Artificial Intelligence
Systems and Control
url https://arxiv.org/abs/2505.14001