SearcharxivSearch

arXiv subjects

Taoran Wu

Publications and source records attributed to Taoran Wu.

14 recordsLinked to original sources

Cost-Aware Adaptive Conformal Inference for Runtime Assurance in Dynamic Environments

This paper addresses the problem of providing runtime assurance for systems operating online under unknown and potentially time-varying data distributions. We propose Cost-Aware Adaptive Conformal Inference (ACI), a novel framework that incorporates constraint violation costs directly into the conformal adaptation mechanism. Our key insight is that uncertainty margins should adapt not only to the frequency of constraint violations but also to their severity. We formalize this through a cost-aware loss function that couples the miscoverage indicator with violation costs. Unlike existing methods that regulate a single controlled metric, our approach provides a dual statistical guarantee: simultaneously bounding the long-run average violation frequencies (reliability) and cumulative violation cost (harm). By weighting prediction failures according to their severity, the algorithm enables the controller to respond proportionally to violation severity, expanding prediction sets aggressively when necessary while maintaining efficiency during nominal operation. We integrate Cost-Aware ACI into a robust control synthesis framework, creating a closed-loop system that balances task performance with runtime risk control without requiring explicit model knowledge. Experiments validate its effectiveness for online risk-aware controller synthesis.

eess.SY

Stochastic Minimum-Cost Reach-Avoid Reinforcement Learning

We study stochastic minimum-cost reach-avoid reinforcement learning, where an agent must satisfy a reach-avoid specification with probability at least $p$ while minimizing expected cumulative costs in stochastic environments. Existing safe and constrained reinforcement learning methods typically fail to jointly enforce probabilistic reach-avoid constraints and optimize cost in the learning setting in stochastic environments. To address this challenge, we introduce reach-avoid probability certificates (RAPCs), which identify states from which stochastic reach-avoid constraints are satisfiable. Building on RAPCs, we develop a contraction-based Bellman formulation that serves as a principled surrogate for integrating reach-avoid considerations into reinforcement learning, enabling cost optimization under probabilistic constraints. We establish almost sure convergence of the proposed algorithms to locally optimal policies with respect to the resulting objective. Experiments in the MuJoCo simulator demonstrate improved cost performance and consistently higher reach-avoid satisfaction rates.

cs.LG

PAC Finite-Time Safety Guarantees for Stochastic Systems with Unknown Disturbance Distributions

We investigate the problem of establishing finite-time probabilistic safety guarantees for discrete-time stochastic dynamical systems subject to unknown disturbance distributions, using barrier certificate methods. Our approach develops a data-driven safety certification framework that relies only on a finite collection of independent and identically distributed (i.i.d.) disturbance samples. Within this framework, we propose a certification procedure such that, with confidence at least $1-\delta$ over the sampled disturbances, if the output of the certification procedure is accepted, the probability that the system remains within a prescribed safe set over a finite horizon is at least $1-\epsilon$. A key challenge lies in formally characterizing the probably approximately correct (PAC) generalization behavior induced by finite samples. To address this, we derive PAC generalization bounds using tools from VC dimension, scenario optimization, and Rademacher complexity. These results illuminate the fundamental trade-offs between sample size, model complexity, and safety tolerance, providing both theoretical insight and practical guidance for designing reliable, data-driven safety certificates in discrete-time stochastic systems.

eess.SY

PAC One-Step Safety Certification for Black-Box Discrete-Time Stochastic Systems

This paper investigates the problem of safety certification for black-box discrete-time stochastic systems, where both the system dynamics and disturbance distributions are unknown, and only sampled data are available. Under such limited information, ensuring robust or classical quantitative safety over finite or infinite horizons is generally infeasible. To address this challenge, we propose a data-driven framework that provides theoretical one-step safety guarantees in the Probably Approximately Correct (PAC) sense. This one-step guarantee can be applied recursively at each time step, thereby yielding step-by-step safety assurances over extended horizons. Our approach formulates barrier certificate conditions based solely on sampled data and establishes PAC safety guarantees by leveraging the VC dimension, scenario approaches, Markov's inequality, and Hoeffding's inequality. Two sampling procedures are proposed, and three methods are proposed to derive PAC safety guarantees. The properties and comparative advantages of these three methods are thoroughly discussed. Finally, the effectiveness of the proposed methods are demonstrated through several numerical examples.

eess.SY

Efficient Verification and Falsification of ReLU Neural Barrier Certificates

Barrier certificates play an important role in verifying the safety of continuous-time systems, including autonomous driving, robotic manipulators and other critical applications. Recently, ReLU neural barrier certificates -- barrier certificates represented by the ReLU neural networks -- have attracted significant attention in the safe control community due to their promising performance. However, because of the approximate nature of neural networks, rigorous verification methods are required to ensure the correctness of these certificates. This paper presents a necessary and sufficient condition for verifying the correctness of ReLU neural barrier certificates. The proposed condition can be encoded as either an Satisfiability Modulo Theories (SMT) or optimization problem, enabling both verification and falsification. To the best of our knowledge, this is the first approach capable of falsifying ReLU neural barrier certificates. Numerical experiments demonstrate the validity and effectiveness of the proposed method in both verifying and falsifying such certificates.

eess.SY

Controlled Reach-avoid Set Computation for Discrete-time Polynomial Systems via Convex Optimization

This paper addresses the computation of controlled reach-avoid sets (CRASs) for discrete-time polynomial systems subject to control inputs. A CRAS is a set encompassing initial states from which there exist control inputs driving the system into a target set while avoiding unsafe sets. However, efficiently computing CRASs remains an open problem, especially for discrete-time systems. In this paper, we propose a novel framework for computing CRASs which takes advantage of a probabilistic perspective. This framework transforms the fundamentally nonlinear problem of computing CRASs into a computationally tractable convex optimization problem. By regarding control inputs as disturbances obeying certain probability distributions, a CRAS can be equivalently treated as a 0-reach-avoid set in the probabilistic sense, which consists of initial states from which the probability of eventually entering the target set while remaining within the safe set is greater than zero. Thus, we can employ the convex optimization method of computing 0-reach-avoid sets to estimate CRASs. Furthermore, inspired by the $ε$-greedy strategy widely used in reinforcement learning, we propose an approach that iteratively updates the aforementioned probability distributions imposed on control inputs to compute larger CRASs. We demonstrate the effectiveness of the proposed method on extensive examples.

eess.SY

Convex Computations for Controlled Safety Invariant Sets of Black-box Discrete-time Dynamical Systems

Identifying controlled safety invariant sets (CSISs) is essential for safety-critical systems. This paper addresses the problem of computing CSISs for black-box discrete-time systems, where the dynamics are unknown and only limited simulation data are available. Traditionally, a CSIS requires that for every state in the set, there exists a control input that keeps the system within the set at the next step. However, enforcing such universal invariance, i.e., requiring the set to remain controlled invariant for all states, is often overly restrictive or impractical for black-box systems. To address this, we introduce the notion of a Probably Approximately Correct (PAC) CSIS, in which, with prescribed confidence, there exists a suitable control input to keep the system within the set at the next step for at least a specified fraction of the states. Our approach leverages barrier functions and scenario optimization, yielding a tractable linear programming method for estimating PAC CSISs. Several illustrative examples demonstrate the effectiveness of the proposed framework.

eess.SY

A Framework for Safe Probabilistic Invariance Verification of Stochastic Dynamical Systems

Ensuring safety through set invariance has proven to be a valuable method in various robotics and control applications. This paper introduces a comprehensive framework for the safe probabilistic invariance verification of both discrete- and continuous-time stochastic dynamical systems over an infinite time horizon. The objective is to ascertain the lower and upper bounds of liveness probabilities for a given safe set and set of initial states. The liveness probability signifies the likelihood of the system remaining within the safe set indefinitely, starting from a state in the initial set. To address this problem, we propose optimizations for verifying safe probabilistic invariance in discrete-time and continuous-time stochastic dynamical systems. These optimizations are constructed via either using the Doob's nonnegative supermartingale inequality-based method or relaxing the equations described in [30,32], which can precisely characterize the probability of reaching a target set while avoiding unsafe states. Finally, we demonstrate the effectiveness of these optimizations through several examples using semi-definite programming tools.

eess.SY

Inner-approximate Reachability Computation via Zonotopic Boundary Analysis

Inner-approximate reachability analysis involves calculating subsets of reachable sets, known as inner-approximations. This analysis is crucial in the fields of dynamic systems analysis and control theory as it provides a reliable estimation of the set of states that a system can reach from given initial states at a specific time instant. In this paper, we study the inner-approximate reachability analysis problem based on the set-boundary reachability method for systems modelled by ordinary differential equations, in which the computed inner-approximations are represented with zonotopes. The set-boundary reachability method computes an inner-approximation by excluding states reached from the initial set's boundary. The effectiveness of this method is highly dependent on the efficient extraction of the exact boundary of the initial set. To address this, we propose methods leveraging boundary and tiling matrices that can efficiently extract and refine the exact boundary of the initial set represented by zonotopes. Additionally, we enhance the exclusion strategy by contracting the outer-approximations in a flexible way, which allows for the computation of less conservative inner-approximations. To evaluate the proposed method, we compare it with state-of-the-art methods against a series of benchmarks. The numerical results demonstrate that our method is not only efficient but also accurate in computing inner-approximations.

eess.SY

Converse Barrier Certificates for Finite-time Safety Verification of Continuous-time Perturbed Deterministic Systems

In this paper, we investigate the problem of verifying the finite-time safety of continuous-time perturbed deterministic systems represented by ordinary differential equations in the presence of measurable disturbances. Given a finite-time horizon, if the system is safe, it, starting from a compact initial set, will remain within an open and bounded safe region throughout the specified time horizon, regardless of the disturbances. The main contribution of this work is a converse theorem: we prove that a continuously differentiable, time-dependent barrier certificate exists if and only if the system is safe over the finite-time horizon. The existence problem is explored by finding a continuously differentiable approximation of a unique Lipschitz viscosity solution to a Hamilton-Jacobi equation.

eess.SY

UR4NNV: Neural Network Verification, Under-approximation Reachability Works!

Recently, formal verification of deep neural networks (DNNs) has garnered considerable attention, and over-approximation based methods have become popular due to their effectiveness and efficiency. However, these strategies face challenges in addressing the "unknown dilemma" concerning whether the exact output region or the introduced approximation error violates the property in question. To address this, this paper introduces the UR4NNV verification framework, which utilizes under-approximation reachability analysis for DNN verification for the first time. UR4NNV focuses on DNNs with Rectified Linear Unit (ReLU) activations and employs a binary tree branch-based under-approximation algorithm. In each epoch, UR4NNV under-approximates a sub-polytope of the reachable set and verifies this polytope against the given property. Through a trial-and-error approach, UR4NNV effectively falsifies DNN properties while providing confidence levels when reaching verification epoch bounds and failing falsifying properties. Experimental comparisons with existing verification methods demonstrate the effectiveness and efficiency of UR4NNV, significantly reducing the impact of the "unknown dilemma".

cs.AI

Reach-avoid Analysis for Sampled-data Systems with Measurement Uncertainties

Digital control has become increasingly prevalent in modern systems, making continuous-time plants controlled by discrete-time (digital) controllers ubiquitous and crucial across industries, including aerospace, automotive, and manufacturing. This paper focuses on investigating the reach-avoid problem in such systems, where the objective is to reach a goal set while avoiding unsafe states, especially in the presence of state measurement uncertainties. We propose an approach that builds upon the concept of exponential control guidance barrier functions, originally used for synthesizing continuous-time feedback controllers. We introduce a sufficient condition that, if met by a given continuous-time feedback controller, ensures the safe guidance of the system into the goal set in its sampled-data implementation, despite state measurement uncertainties. The event of reaching the goal set is determined based on state measurements obtained at the sampling time instants. Numerical examples are provided to demonstrate the validity of our theoretical developments, showcasing successful implementation in solving the reach-avoid problem in sampled-data systems with state measurement uncertainties.

eess.SY

Repairing Deep Neural Networks Based on Behavior Imitation

The increasing use of deep neural networks (DNNs) in safety-critical systems has raised concerns about their potential for exhibiting ill-behaviors. While DNN verification and testing provide post hoc conclusions regarding unexpected behaviors, they do not prevent the erroneous behaviors from occurring. To address this issue, DNN repair/patch aims to eliminate unexpected predictions generated by defective DNNs. Two typical DNN repair paradigms are retraining and fine-tuning. However, existing methods focus on the high-level abstract interpretation or inference of state spaces, ignoring the underlying neurons' outputs. This renders patch processes computationally prohibitive and limited to piecewise linear (PWL) activation functions to great extent. To address these shortcomings, we propose a behavior-imitation based repair framework, BIRDNN, which integrates the two repair paradigms for the first time. BIRDNN corrects incorrect predictions of negative samples by imitating the closest expected behaviors of positive samples during the retraining repair procedure. For the fine-tuning repair process, BIRDNN analyzes the behavior differences of neurons on positive and negative samples to identify the most responsible neurons for the erroneous behaviors. To tackle more challenging domain-wise repair problems (DRPs), we synthesize BIRDNN with a domain behavior characterization technique to repair buggy DNNs in a probably approximated correct style. We also implement a prototype tool based on BIRDNN and evaluate it on ACAS Xu DNNs. Our experimental results show that BIRDNN can successfully repair buggy DNNs with significantly higher efficiency than state-of-the-art repair tools. Additionally, BIRDNN is highly compatible with different activation functions.

cs.LG

Provable Reach-avoid Controllers Synthesis Based on Inner-approximating Controlled Reach-avoid Sets

In this paper, we propose an approach for synthesizing provable reach-avoid controllers, which drive a deterministic system operating in an unknown environment to safely reach a desired target set. The approach falls within the reachability analysis framework and is based on the computation of inner-approximations of controlled reach-avoid sets(CRSs). Given a target set and a safe set, the controlled reach-avoid set is the set of states such that starting from each of them, there exists at least one controller to ensure that the system can enter the target set while staying inside the safe set before the target hitting time. Therefore, the boundary of the controlled reach-avoid set acts as a barrier, which separating states capable of achieving the reach-avoid objective from those that are not, and thus the computed inner-approximation provides a viable space for the system to achieve the reach-avoid objective. Our approach for synthesizing reach-avoid controllers mainly consists of three steps. We first learn a safe set of states in the unknown environment from sensor measurements based on a support vector machine approach. Then, based on the learned safe set and target set, we compute an inner-approximation of the CRS. Finally, we synthesize controllers online to ensure that the system will reach the target set by evolving inside the computed inner-approximation. The proposed method is demonstrated on a Dubin's car system.

eess.SY