Continuous-Time VeRecycle
Reclaiming Reach-Avoid Guarantees from Neural Certificates for Stochastic Dynamical Systems after Localised Changes
S.M. Grădinariu (TU Delft - Electrical Engineering, Mathematics and Computer Science)
A. Lukina – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
S. Lutz – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
L. Laurenti – Graduation committee member (TU Delft - Mechanical Engineering)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Safety-critical autonomous systems, such as robots or drones, often depend on formal guarantees. These show that they will reach a desired target while avoiding unsafe states. These guarantees can be provided by a certificate: a mathematical proof object that summarises the system's behaviour without requiring all possible trajectories to be simulated. However, once the system is deployed, its dynamics may change locally, for example, because of altered friction, disturbances, or unexpected environmental effects. Recomputing a new certificate from scratch can be expensive, especially when the certificate is represented by a neural network.
This thesis studies whether an existing certificate can still be reused when such a localised change occurs in a continuous-time stochastic system. It extends the VeRecycle reclaiming principle, originally developed for discrete-time stochastic dynamical systems, to continuous-time stochastic differential equations. VeRecycle provides a mathematical framework for determining how much of an existing reach-avoid guarantee can still be recovered after the dynamics change within a known region of the state space. This extension is important because many physical control systems evolve continuously, while the existing VeRecycle theory is formulated only for discrete-time models.
The main contribution is a continuous-time reclaiming rule for reach-avoid certificates. The rule shows that, for a fixed certified tuple (V, α, β, ζ), the maximal guarantee that can be recovered by reusing the certificate V depends on the changed region only through the minimum certificate value over that region. In other words, the changed region affects the reclaimed guarantee only through the lowest value that the original certificate reaches on that region.
The framework is implemented using neural reach-avoid certificates and interval-bound propagation, and is evaluated on a stochastic inverted pendulum benchmark. The performed experiments show that the recovered guarantees depend on the local certificate minimum, and can be computed considerably faster than full re-certification, while avoiding failure modes caused by naive discretise-then-reclaim approaches.