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

1 Introduction

Autonomous systems often exhibit nonlinear stochastic behavior. In safety-critical applications (e.g., robot navigation), it is crucial to provide provable guarantees for autonomous systems, both in terms of performance (e.g., reaching a target) and safety (e.g., avoiding material damage) [Kwiatkowska and Zhang, 2023]. The latter is particularly challenging to guarantee for the multitude of uncertainties of the real world. For instance, a spill of water may violate the friction threshold for a robot to move at the required safe speed.

Designing safe control for a stochastic nonlinear dynamical system, as a general model for many real-world autonomous systems, is enabled by the Lyapunov theory [Kalman and Bertram, 1959]. Initially developed for proving the stability of deterministic dynamical systems, Lyapunov theory prescribes the construction of a potential-energy function, which characterizes system dynamics and, when obeying a set of given conditions, becomes a formal certificate for the desired specification. Reaching the target while avoiding unsafe states can be naturally formulated as Lyapunov stability: the system's potential energy decreases towards the target region and increases around unsafe regions. Lyapunov certification extends to stochastic dynamical systems [Blumenthal and Getoor, 1968] and to proving reach-avoid properties thereof [Prajna et al., 2004].

Overwhelming success of neural networks in visual recognition and especially feasibility of their verification [Katz et al., 2017; Gehr et al., 2018; Zhang et al., 2018; Kouvaros and Lomuscio, 2021; Wu et al., 2024] galvanized the research community into adoption of neural components in control design. Verification of dynamical systems under neural control called for an alternative to sum-ofsquare programming [Papachristodoulou and Prajna, 2002; Topcu et al., 2008], limited to polynomial dynamics. Neural Lyapunov certification proved successful for deterministic systems [Richards et al., 2018; Chang et al., 2019; Abate et al., 2021; Edwards et al., 2023; Dawson et al., 2023]. Recently, inspired by termination analysis of stochastic programs [Giacobbe et al., 2022], probabilistic neural Lyapunov certification solidified its place as the state-of-theart for reach-avoid properties of stochastic dynamical systems under neural control [Žikeli´c et al., 2023a; Ansaripour et al., 2023; Chatterjee et al., 2023; Mathiesen et al., 2023; Abate et al., 2024; Badings et al., 2024].

For a given model of dynamics and a control policy, stateof-the-art probabilistic reach-avoid certificates guarantee that with probability above a given threshold, the system will reach a target set of states while avoiding unsafe states. However, in scenarios where the system dynamics deviate from their stochastic model, even if only in a known subset of system states, the originally computed certificate requires revalidation to transfer its guarantee. Yet, there exists no principled way to infer if the changes in the dynamics affect the guarantees or to reuse the corresponding certificate, without repeating costly (neural) certification.

Example 1. A robot navigates a warehouse with slippery floors, meaning the result of the robot's actions is probabilistic. To safely reach room 8 starting from room 0 (dotted squares in Figure 1 mark the centers of the rooms), the robot is controlled by a composition of neural policies, including one guiding it from room 4 to 5, avoiding collision with the walls. Figure 1 visualizes a probabilistic neural certificate, which guarantees that starting anywhere close to the center of room 4, the robot will safely reach the center of room 5 with probability at least 0.88. Suppose that an unidentified obstacle appeared in room 2 and the whole room is now deemed unsafe. Although the obstacle is not interfering with the given subtask, visual inspection shows the certificate is now invalid (dashed line crosses the area around the obstacle).

In this work, we propose the first, to the best of our knowledge, theoretical justification for reclaiming probabilistic reach-avoid guarantees for neural control policies of discretetime stochastic dynamical systems affected by a localized change, i.e., for which the dynamics changed in a given subset of the state space. In that, we assume no knowledge about the nature of the change.

Our approach, called VeRecycle, takes as input a neural control policy and a probabilistic neural reach-avoid certificate with a particular probability threshold. For an arbitrary, possibly unknown, change in the system dynamics affecting a known subset of the state space, VeRecycle automatically infers a new certified reach-avoid probability threshold.

In Example 1, VeRecycle quickly identifies the affected certificate and updates its threshold to 0.70 (solid line has no intersection with the unsafe area), without any additional neural training. This enables further use of existing neural policies and reclaiming the global probabilistic guarantee.

VeRecycle magnifies the advantages of tackling the problems with innate modular structure through the prism of localized analysis, for which compositional approaches to control and-with VeRecycle-certification demonstrate greater scalability [Neary et al., 2023; Žikeli´c et al., 2023b; Zhang et al., 2023; Delgrange et al., 2024]. In compositional control, our approach 1) automatically identifies which components of the compositional policy are affected by the change and 2) eliminates-when possible-the need for costly repairs of neural control policies, certificates, or system models by using unaffected components in a new compositional policy.

To summarize, we propose VeRecycle, a framework to formally reclaim guarantees from probabilistic neural certificates for discrete-time stochastic dynamical systems after localized changes. First, we formally prove that sound guarantees are inferred by VeRecycle from (approximated) infima of the original certificates. Second, our experimental evaluation demonstrates scenarios where VeRecycle's guarantees are competitive-particularly for compositional controlcompared to complete re-certification, with computational cost reduced by three orders of magnitude. Thus, VeRecycle enables higher flexibility and scalability of the state-ofthe-art probabilistic reach-avoid certification of discrete-time stochastic dynamical systems.

2 Preliminaries

We consider discrete-time stochastic dynamical systems Σ = (X, U, W, f, µ), defined by the following equation ∀t ∈ N>0:

where xt ∈ X ⊆ Rn is the n-dimensional state of Σ at time t with x0 as the initial state, ut ∈ U ⊆ Rm is the mdimensional control input Σ at time t, and wt ∈ W ⊆ Rp is the p-dimensional realization of stochastic disturbance of Σ at time t. Transitions between states follow the dynamics function f : X×U×W→ X, and the probability distribution µ over W, from which wt is sampled independently at each time step. When the control inputs are determined by a policy π : X → U, i.e., ut := π(xt), Σ is said to be controlled by π.

An infinite sequence of state, action, and disturbance triples (xt, ut,wt)t∈N0 is a trajectory if for all time steps t ∈ N>0, it holds that xt+1 = f(xt, ut, wt), ut = π(xt), and wt ∈ support(µ). Given a fixed initial state x0, Markov decision process (MDP) semantics establish a probability space over all such trajectories [Puterman, 2014]. The probability measure and expectation within this probability space are denoted PΣ,π x0 and EΣ,π x0 , respectively.

For the system semantics and probability measures to be well-defined, we assume X, U, and W to be Borelmeasurable. Moreover, we follow the standard assumptions from control theory that f and π are Lipschitz continuous, and that X and W are closed and bounded.

2.1 Reach-avoid Verification

A common way to quantify the performance and safety of control policies for stochastic dynamical systems is via probabilistic reach-avoid specifications, which enforce a threshold on the probability of reaching a target state without encountering unsafe states.

Definition 1. A reach-avoid specification is a tuple (X⋆,X⊘,X0, ρ), where X⋆,X⊘,X0 ⊆ X are target states, unsafe states, and initial states, respectively, and ρ ∈ [0, 1] is a probability threshold, i.e., minimally acceptable probability with which the specification holds. A system Σ controlled by a policy π satisfies a reach-avoid specification, denoted Σ, π ⊨ (X⋆, X⊘, X0, ρ), if and only if, for all x0 ∈ X0,

Example 2. Consider the original system described in Example 1, i.e., before water was spilled. This stochastic dynamical system Σ has a two-dimensional state space X = [0, 3]2 , the two features being x and y coordinates, respectively. The navigation task of safely moving from room 4 to 5 (yellow and green in Figure 1 respectively) with at least a probability of 0.88, is a reach-avoid specification φ where X⋆ = [2.4, 2.6] × [1.4, 1.6], X⊘ is the union of the walls, X0 = [1.4, 1.6]2 , and ρ = 0.88.

To verify that a reach-avoid specification holds for a system under a particular policy, one can construct probabilistic reach-avoid certificates, whose existence serves as proof.

Definition 2 ([Žikeli´c et al., 2023a]). A continuous function C : X → R≥0 is a reach-avoid certificate for a system Σ, policy π, and reach-avoid specification φ = (X⋆, X⊘, X0, ρ), if and only if the following conditions hold:

1. Initial condition: for all x ∈ X0, C(x) ≤ 1;
2. Safety condition: for all x ∈ X⊘, C(x) ≥ 1 1-ρ ;
3. Decrease condition: there exists ε > 0, such that for all x ∈ X\X⋆ either Ew∼µ[C(x) -C(f (x, π(x), w))] ≥ ε or C(x) ≥ 1 1-ρ .

The existence of a probabilistic reach-avoid certificate proves (i.e., certifies) that Σ, π ⊨ φ. We use the shorthand C(S) := {C(x) | x ∈ S} for the image of a subset S ⊆ X under C.

The z axis (color gradient) in Figure 1 shows an example of a reach-avoid certificate for the specification φ and system Σ defined in Example 2. Intuitively, the third condition requires that, in any state, Σ is unlikely to transition to a state with a higher value in C, with larger differences being increasingly improbable. Consequently, the first and second conditions establish that from the initial states (with values ≤ 1), it is rare to reach the unsafe states (with values ≥ 1 1-ρ ). Furthermore, Σ is likely to progress toward the lowest-valued part of the certificate. Since only the target area is permitted to violate the decrease condition and fall below the safety value 1 1-ρ , the certificate takes its lowest value in the target area, to which the state of the system eventually converges.

Constructing probabilistic reach-avoid certificates analytically is challenging, especially for nonlinear system dynamics or neural policies. Thus, the state-of-the-art is a counterexample guided synthesis procedure that outputs a certificate in the form of a neural network-a neural certificate [Žikeli´c et al., 2023a; Chatterjee et al., 2023; Badings et al., 2024].

The procedure loops between learning and verification until a correct certificate is found or the allotted time is exceeded; in the latter case, the result is inconclusive.

The learning procedure optimizes the candidate certificate on differentiable versions of conditions 1-3 from Definition 2 for a set of randomly sampled states and a set of counterexamples produced by the verification procedure. The verification procedure discretizes the continuous state space into "cells", verifying conditions 1-3 soundly for all states within the cells using Lipschitz constants and interval bound propagation (IBP) [Mirman et al., 2018; Gowal et al., 2019]. If the verification is inconclusive for a cell, i.e., when the bounds given by IBP and Lipschitz reasoning are not tight enough to prove or disprove the conditions for all states in the cell, the cell is split into smaller cells to attempt verification again. If a condition is certainly violated for a cell, the verification procedure feeds all states in the cell back into the learning procedure as counterexamples for further optimization.

3 Problem Statement

We formulate the general problem of reclaiming guarantees from probabilistic reach-avoid certificates after a change in system dynamics. Our problem formulation specifically addresses changes that affect the system dynamics only in a known subset of states X?. Importantly, this definition does not require additional knowledge of the new dynamics. Instead, the aim is to determine guarantees that are valid for any alternative dynamics function, as long as anywhere outside X?, the function is equivalent to the original dynamics.

This formulation captures a wide range of changes, such as the detection of unidentified obstacles, the appearance of materials with unknown friction coefficients within a specific region, or the onset of unexplained stochastic phenomena occurring exclusively within a certain velocity range.

Formally, we consider a stochastic dynamical system Σ = (X, U, W, f, µ) controlled by a policy π, that satisfies a reachavoid specification φ = (X⋆,X⊘,X0, ρ), and a reach-avoid certificate C proving that relation, i.e., C certifies Σ, π ⊨ φ.

Definition 3. Given states X? ⊂ X, a threshold ρ′ ∈ [0, 1] is reclaimable, if and only if C certifies ˜Σ, π ⊨ (X⋆, X⊘, X0, ρ′ ) for all ˜Σ = (X,U,W, ˜ f, µ), such that

Problem 1. Given a certificate C, original threshold ρ, and states X? ⊂ X, determine the maximum reclaimable threshold ρ′ ≤ ρ, denoted ˜ ρ .

Example 3 (Example 2 continued). The spilled water in the blue hatched area in Figure 1 creates a new, alternative system with dynamics function ˜ f ,

The solution to Problem 1 for X? = [2, 3] × [0, 1] gives us a threshold ˜ ρ on the probability of reaching green without colliding with walls. Whether the consequences of the spilled water are erratic movements, a complete shut-down, or barely noticeable, should not matter for this threshold: C

should certify ˜ ρ for any possible realization of ˜ f and be the largest threshold ≤ ρ for which this holds.

We remark that Problem 1 defines a maximum threshold that is always valid, i.e., without any assumptions on the new dynamics function beyond Equation 2, and for a fixed C and π. While higher probability thresholds might be obtainable once the actual new dynamics are specified, such thresholds are not the generally valid thresholds of Problem 1: we are specifically interested in solving the problem for unknown dynamics in a known set of states. Similarly, updating the certificate or policy for the changed dynamics could also result in a higher threshold than ˜ ρ. However, since the state-ofthe-art certification of nonlinear, stochastic dynamics and/or neural policies is done with neural networks, changing them requires costly additional training and verification.

Thus, for applications where a new model of the dynamics can be obtained and alternative policies and certificates can be trained, the general solution to Problem 1 still serves a practical purpose. If the general threshold already matches the original specification or falls within some acceptable margin, there is no need to update the system model and repeat costly re-certification. Thus, a solution to Problem 1 serves as proof that such updates are truly necessary before spending significant computational resources.

4 VeRecycle

We propose VeRecycle, a framework to reclaim guarantees from reach-avoid certificates given a subset of states X? in which dynamics may have changed, as formulated in Problem 1. VeRecycle exploits a relation between the maximum reclaimable probability threshold ˜ ρ and the infimum of a certificate on X?. First, we formalize this relation and prove that it provides an exact solution to Problem 1. Second, we discuss how VeRecycle reduces computational costs through approximations of infima for neural certificates while still providing soundness guarantees.

4.1 Exact Solution

In this subsection, we prove that an exact solution ˜ ρ to Problem 1 depends only on the original bound ρ and the lowest value the certificate takes for states in X?: the infimum inf{C(X?)}. In particular, we show that whenever inf{C(X?)} ≥ 1, ˜ ρ equals

and that otherwise no reclaimable threshold exists.

We first show that whenever inf{C(X?)} ≥ 1, Equation 4 upper-bounds and lower-bounds ˜ ρ (Lemmas 1 and 2 respectively). Subsequently, we combine these results with a proof of the non-existence of ˜ ρ in case inf{C(X?)} < 1, completing our proof of the relation.

Lemma 1 (Lower bound of ˜ ρ). If inf{C(X?)} ≥ 1, then Equation 4 lower-bounds the maximum reclaimable threshold ˜ ρ defined in Problem 1.

Proof sketch (proof in the extended version). We set ρ′ to Equation 4 and prove that it is a reclaimable threshold for C.

By definition of a maximum, it follows that the maximum of all such reclaimable thresholds, ˜ ρ, is lower-bounded by Equation 4.

Threshold ρ′ is reclaimable because it is chosen precisely such that for all states in X?, the certificate value is at least 1 1-ρ′ . Intuitively, this means that the states with unknown dynamics are visited rarely enough that we do not need to have an expected decrease of the certificate's value there: we reach those states with a probability ≤ 1 - ρ′ .

For states outside of the changed states X?, the expected value of the subsequent states remains unchanged since the dynamics function in X\X? and the certificates' values remain unchanged. Note that even if one of the future subsequent states is within X? and may therefore have new dynamics, this does not change the expectation in the current state, since the expectation is calculated over one time-step only. Conditions 1 and 2 follow similarly because they were satisfied for the original system and threshold, which concludes the proof of Lemma 1.

Lemma 2 (Upper bound of ˜ ρ). If inf{C(X?)} ≥ 1, then Equation 4 upper-bounds the maximum reclaimable threshold ˜ ρ defined in Problem 1.

Proof sketch (proof in the extended version). Any reclaimable threshold, including the maximum (˜ ρ), must be a valid threshold for all realizations of ˜ f, including fully absorbing dynamics, i.e., where ˜ f(x, u, w) = x, ∀x ∈ X?. For such absorbing dynamics, it is impossible to prove the expected decrease of the certificate, since the expectation always equals the certificate's value in the current state. Thus, by condition 3 of Definition 2, the infimum of the certificate in X? must be above 1 1-˜ ρ , from which we derive the inequality in Lemma 2.

Proof sketch (proof in the extended version). We prove the implication of Lemma 3 by assuming that ˜ ρ exists, and concluding that inf{C(X?)} ≥ 1. If ˜ ρ exists, it must be valid for fully absorbing dynamics: ˜ f(x, u,w) = x, ∀x ∈ X?. Thus, by condition 3 of Definition 2, the infimum of the certificate in X? must be above 1 1-˜ ρ , from which we derive inf{C(X?)} ≥ 1.

Theorem 1 (Equality to ˜ ρ). The maximum reclaimable threshold ˜ ρ defined in Problem 1 does not exist if inf{C(X?)} < 1, and otherwise ˜ ρ equals Equation 4.

Theorem 1 follows directly from Lemmas 1 to 3. A formal proof is given in the extended version.

4.2 Sound Approximation

Theorem 1 proves that the exact solution to Problem 1 only depends on the infimum of the certificate for X? and the original certified threshold ρ. In practice, however, finding the infimum of a certificate can be expensive and difficult to scale, particularly for neural certificates. To address this, VeRecycle is equipped to work with approximations of the infimum, while still producing only sound thresholds.

Specifically, methods such as interval bound propagation (IBP) [Gowal et al., 2019] can be used to determine values I - and I + such that I - ≤ inf{C(X?)} ≤ I +. With these bounds on the infimum, we can determine guaranteed bounds on the exact solution in Equation 4:

Theorem 2. If I - ≤ inf{C(X?)} ≤ I + and I - ≥ 1, then ˜ ρ- ≤ ˜ ρ ≤ ˜ ρ+.

Proof sketch (proof in the extended version). We show that the function in Equation 4 is monotonically increasing for inf{C(X?)} on the interval (0,∞). Additionally, if inf{C(X?)} ≥ 1 the formula in Equation 4 is, by Theorem 1, equal to ˜ ρ. Thus, if 1 ≤ I - ≤ inf{C(X?)} ≤ I +, it follows that ˜ ρ- ≤ ˜ ρ ≤ ˜ ρ+.

If ˜ ρ- is unsatisfactory, e.g., it does not match the original guarantee, or exceeds some permissible drop in probability, X? can be split up using a finer mesh. Such a refinement is only done if the desired threshold is below ˜ ρ+: otherwise, the desired threshold cannot be obtained by refinement. In those cases, VeRecycle's output serves as proof that certification of the specification cannot be achieved without making additional assumptions on the changed dynamics, and/or performing additional training of the neural certificate.

VeRecycle outputs ˜ ρ- as a guaranteed threshold, certified by the original certificate for any realization of ˜ f. The tightness of I - to inf{C(X?)}-and, consequently, ˜ ρ- to ˜ ρdepends on the size of the interval used for IBP. Thus, VeRecycle uses a mesh to split up X? into smaller intervals, increasing the tightness of ˜ ρ- to ˜ ρ .

The complexity of VeRecycle depends only on the complexity of determining (approximate) infima. For neural certificates, it is therefore determined by the complexity of IBP and the mesh size used.

5 VeRecycle for Compositional Control

VeRecycle is particularly valuable for systems under compositional control, in which a selection of policies is executed sequentially to complete a complex task. The modularity of such control allows VeRecycle to first reclaim guarantees for each component individually. Subsequently, the least affected components can be reused directly in a new composition, minimizing the need for costly repairs to neural control policies, certificates, and systemmodels.

We consider compositional control based on a reach-avoid specification that is decomposed into several connected subtasks, either manually or automatically [Jothimurugan et al., 2021]. This task decomposition is represented as a directed graph G = (V,E, v0, v⋆, β) where the mapping function β : V ∪ E → X relates the graph's elements to a stochastic dynamical system's state space: an edge e from vertex va to vb represents the task of reaching β(vb) from β(va) while avoiding β(e).

A compositional policy for G then consists of a set of edge-associated policies {πe | e ∈ E} and a path π⋆ = (v0, . . . , vk) in G, representing sequential execution of the policies πe associated with each traversed edge e. Certification of the global reach-avoid specification φ with threshold ρ, requires that valid probability thresholds ρe and corresponding certificates Ce are given for all edge-associated policies πe, and that multiplying them along the edges of the path π⋆ results in a value above the global probability threshold, i.e. ∏ki=1 ρ(vi-1,vi) ≤ ρ.

Example 4. We return to the running example of a robot navigating a warehouse with nine rooms. The goal-to navigate from the center of room 0 to the center of room 8-is broken down into subtasks of moving between two specific rooms. The specific task decomposition graph G is shown in Figure 2, with function β mapping vertices 0-8 to the dashed regions in Figure 1, and each edge to the walls (X⊘). The compositional policy used to control the robot consists of the path π⋆ = (0, 1, 2, 5, 8) highlighted in red, and for each edge e, a policy πe. This compositional policy is certified for the original dynamics of the system: for each edge e, some certificate Ce is given that proves a threshold ρe.

Algorithm 1 shows how VeRecycle can be used to reclaim guarantees for such compositional policies, given the set X? with changed dynamics, the graph G, and the sets of edgeassociated certificates. For each edge in the task decomposition graph G used by the compositional controller, VeRecycle is invoked to reclaim a guaranteed threshold for the original certificate, ensuring validity for any change within X? (Line 3). Each edge in G is assigned the weight -log(p), where p is the threshold obtained from VeRecycle (Line 4). The problem of maximizing the probability threshold of a path becomes a minimization problem that can be solved by an out-of-the-box shortest-path solver (Line 5). The sum of the weights along the shortest path is then converted into the probability threshold for that path (Line 6).

Example 5 (Example 4 continued). Once water has been spilled, the new dynamics ˜ f-unknown in the states X? = [2, 3] × [0, 1]-take effect. Given X?,G, {Ce | e ∈ E}, and {ρe | e ∈ E}, Algorithm 1-invoking VeRecycle for each edge-outputs an alternative blue path ˜ π⋆ = (0, 3, 4, 7, 8) highlighted in Figure 2 which is certified to have at least ˜ ρ = 0.88 · 0.84 · 0.75 · 0.62 ≥ 0.33, regardless of the effect of the spilled water. Although the certified threshold on the original path π⋆ has dropped to zero, an alternative with non-trivial guarantees could still be obtained. This illustrates how VeRecycle can exploit the modular nature of compositional policies while leaving policies and certificates (often neural networks) unaltered.

The complexity of Algorithm 1 depends on the complexity of the calls to VeRecycle in Line 3, made once for each edge in the graph. While this complexity could likely be reduced further by minimizing the number of VeRecycle calls, e.g., a shortest-path solver with on-demand calls to VeRecycle only, this is outside the scope of this work. Algorithm 1 serves as a proof-of-concept implementation of VeRecycle applied to compositional control.

6 Evaluation

We demonstrate a VeRecycle implementation with interval bound propagation [Gowal et al., 2019] to approximate infima of neural certificates. We analyze the efficiency and quality of reclaimed guarantees by VeRecycle on both standalone and compositional neural control in the "Stochastic Nine Rooms" benchmark (Figure 2) introduced by Žikeli´c et al. [2023b], with new, unknown dynamics in one of the rooms (e.g., the blue hatched area).

Out-of-the-box baselines are unavailable since, to the best of our knowledge, VeRecycle is the first framework to reclaim sound guarantees without requiring updated models of the dynamics. As a baseline, we therefore use state-of-theart neural certification [Badings et al., 2024] on worst-case dynamics in X? (absorbing, i.e., xt+1 = xt), treating X? as part of the unsafe set X⊘. We consider three settings for this baseline. First (B-I), verifying that a given new thresholdoutput by VeRecycle-is valid for the original certificate, i.e., given C and ρ′ , decide correctness. Second (B-II), finding a correct threshold given the original certificate as a candidate, i.e., given C, find a valid ρ′ and C ′ . Third (B-III), finding a correct threshold and certificate from scratch, i.e., determine ρ′ and C ′ , without C. All experiments are run on Delft High Performance Computing Centre (DHPC) [2024] with NVIDIA A100 GPUs.

6.1 Experiment 1: Individual Certificates

We analyze VeRecycle's reclaimed thresholds for 63 unique tasks, combining 9 reach-avoid specifications (graph edges in Figure 2) with 7 different subsets X? (rooms). As input, we use neural policies obtained through proximal policy optimization (PPO) [Schulman et al., 2017] with neural reachavoid certificates [Badings et al., 2024]. Technical details are provided in the extended version.

In runtime (Table 1, column 2), VeRecycle outperforms the baseline on all settings. Searching for a new threshold and certificate from scratch (B-III) requires the highest computation time. Using the original certificate as a candidate (BII) reduces computation time by an order of magnitude, emphasizing the benefit of reusing original verification results. When informed of a correct threshold by VeRecycle (B-I) runtime decreases further, demonstrating the benefit of inferring thresholds from certificates rather than trial-and-error search. VeRecycle outperforms B-I by two orders of magnitude, showing the efficiency of ignoring unaffected states.

In addition to requiring less computational effort, VeRecycle produces tighter probability thresholds (Table 1, columns 3-5) than re-verification from scratch (B-III). While reverification with the original certificate (B-II) produces higher thresholds on average, VeRecycle performs comparably on high-quality input certificates-where C(x) ≥ 1 1-ρ for all rooms outside the initial and target rooms. As illustrated in Figure 3, B-II can refine unnecessary low-valued states in "loose" certificates to achieve a higher threshold than VeRecycle. However, this refinement process is computationally expensive, making VeRecycle a lightweight alternative to identify when certificate refinement is necessary. Future work on improving certification techniques for generating higherquality certificates would further enhance VeRecycle's performance and applicability.

100

101

Table 2: Reclaimed probability bounds for compositional policy (Experiment 2), averaged over 5 random seeds for 7 different sets X? with new dynamics. Grouped by whether X? is adjacent to the target room, i.e., in room 5 or 7. Best results per column are in bold.

6.2 Experiment 2: Compositional Control

Next, we compare the global thresholds obtained with Algorithm 1 on the graph from Figure 2, using VeRecycle and baselines to reclaim guarantees for each graph edge, and NetworkX's Dijkstra [Hagberg et al., 2008] as shortest-path solver. The results (Table 2) show that VeRecycle performs competitively on the majority of tasks.

In two particular tasks-rooms with vertex 5 and 7 having unknown dynamics-the effect of low-quality certificates on VeRecycle's performance can still be observed. In those cases, the edges (7,8) and (5,8)-both with "loose" certificates-are simultaneously impacted, thus impacting the reclaimed guarantee on all feasible paths to the target states.

Overall, we observe that VeRecycle is particularly powerful in compositional control settings, because the impact of low-quality input certificates is mitigated by the availability of alternative policies.

7 RelatedWork

Probabilistic neural reach-avoid certification. Probabilistic neural certification is the state-of-the-art for verifying reach-avoid specifications for stochastic dynamical systems under neural control [Žikeli´c et al., 2023a; Ansaripour et al., 2023; Chatterjee et al., 2023; Mathiesen et al., 2023; Abate et al., 2024; Badings et al., 2024]. VeRecycle complements these methods by efficiently deciding whether such guarantees are maintained when system dynamics change, minimizing the high computational cost of re-certifying the complete updated system model.

Robust control synthesis. Robust control synthesis addresses changes in dynamics by designing control policies that perform reliably under a modeled range of disturbances. Techniques include adaptations of Markov Decision Process (MDP) solvers for richer models expressing multiple variations of the system: e.g., parametric MDPs [Badings et al., 2022], interval MDPs [Jiang et al., 2022; Coppola et al., 2024], uncertain MDPs [Wolff et al., 2012], and multienvironment MDPs [Raskin and Sankur, 2014]. While the type of changes addressed by VeRecycle could theoretically be addressed by robust synthesis techniques as well, this would require either knowing all possible changes in advance or updating and solving the adapted MDP again. Thus, we see VeRecycle as a lightweight alternative that does not require prior knowledge of possible changes.

Reusing policies in compositional control. Compositional control as described in Section 5 stems from the concept of options [Sutton et al., 1999], adapted for safety-critical applications through correct-by-design synthesis methods for a high-level plan [Jothimurugan et al., 2021; Neary et al., 2023] and formal verification of used components [Ivanov et al., 2021; Delgrange et al., 2024]. Notably, [Žikeli´c et al., 2023b] verify each component with probabilistic neural certification, inspiring our application of VeRecycle to compositional control. In addition to solving more difficult, long-horizon tasks, a motivation for compositional control is reusing the components in alternative high-level plans. This is not straightforward in case of changes in system dynamics, however, since guarantees on components must still be reclaimed before composing a (new) high-level plan, making VeRecycle complementary to compositional control.

8 Conclusion

VeRecycle is the first framework to formally reclaim guarantees from probabilistic neural certificates for discrete-time stochastic dynamical systems after localized changes. We formally prove that VeRecycle infers sound guarantees from (approximated) infima of the original certificates. Our experimental evaluation demonstrates scenarios in which VeRecycle's guarantees are competitive-particularly for compositional control-compared to complete re-certification, with computational cost reduced by three orders of magnitude.

Future work. We plan to extend the presented theoretical foundations to probabilistic neural certificates for continuoustime systems [Neustroev et al., 2025]. Additionally, we aim to explore how the certificate learning process can be optimized to maximize the guarantees reclaimed with VeRecycle. Another avenue of future research is synergies between VeRecycle and learning-enabled certification [Kolter and Manek, 2019; Wu et al., 2023; Takeishi and Kawahara, 2021; Schlaginhaufen et al., 2021], using VeRecycle to pinpoint crucial states for which new dynamics must be learned.

Acknowledgments

This research was funded by the NWO Veni grant Explainable Monitoring (222.119). This work was done in part while Anna Lukina and Sterre Lutz were visiting the Simons Institute for the Theory of Computing.