BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Bai Xue

Bai Xue contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Systems and Controleess.SYFormal Languages and Automata TheoryMachine Learningmath.DSmath.OCArtificial Intelligence

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
11works
0followers
7topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

11 published item(s)

preprint2026arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2026arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2026arXiv

Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems

This paper investigates necessary and sufficient barrier-like conditions for infinite-horizon safety and reach-avoid verification of stochastic discrete-time systems, derived via a relaxation of the Bellman equations. Unlike prior approaches that primarily focus on sufficient conditions, our work rigorously establishes both necessity and sufficiency for infinite-horizon properties. Safety verification concerns certifying that, starting from a given initial state, the system remains within a safe set at all future time steps with probability at least equal to a specified threshold. For this purpose, we formulate a necessary and sufficient barrier-like condition that captures this infinite-time safety property. In contrast, reach-avoid verification generalizes safety verification by also incorporating reachability. Specifically, it aims to ensure that the probability of the system, starting from a given initial state, eventually reaching a target set while remaining within the safe set until the first hit of the target is no less than a prescribed bound. Under suitable assumptions, we establish two necessary and sufficient barrier-like conditions for this reach-avoid specification.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Reach-avoid Verification Based on Convex Optimization

In this paper we propose novel optimization-based methods for verifying reach-avoid (or, eventuality) properties of continuous-time systems modelled by ordinary differential equations. Given a system, an initial set, a safe set and a target set of states, we say that the reach-avoid property holds if for all initial conditions in the initial set, any trajectory of the system starting at them will eventually, i.e.\ in unbounded yet finite time, enter the target set while remaining inside the safe set until that first target hit. Based on a discount value function, two sets of quantified constraints are derived for verifying the reach-avoid property via the computation of exponential/asymptotic guidance-barrier functions (they form a barrier escorting the system to the target set safely at an exponential or asymptotic rate). It is interesting to find that one set of constraints whose solution is termed exponential guidance-barrier functions is just a simplified version of the existing one derived from the moment based method, while the other one whose solution is termed asymptotic guidance-barrier functions is completely new. Furthermore, built upon this new set of constraints, we derive a set of more expressive constraints, which includes the aforementioned two sets of constraints as special instances, providing more chances for verifying the reach-avoid properties successfully. When the involved datum are polynomials, i.e., the initial set, safe set and target set are semi-algebraic, and the system has polynomial dynamics, the problem of solving these sets of constraints can be framed as a semi-definite optimization problem using sum-of-squares decomposition techniques and thus can be efficiently solved in polynomial time via interior point methods. Finally, several examples demonstrate the theoretical developments and performance of proposed methods.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Synthesizing Invariant Clusters for Polynomial Programs by Semidefinite Programming

In this paper, we present a novel approach to synthesize invariant clusters for polynomial programs. An invariant cluster is a set of program invariants that share a common structure, which could, for example, be used to save the needs for repeatedly synthesizing new invariants when the specifications and programs are evolving. To that end, we search for sets of parameters $R_k$ w.r.t. a parameterized multivariate polynomial $I(a, x)$ (i.e. a template) such that $I(a, x) \leq 0$ is a valid program invariant for all $a \in R_k$. Instead of using time-consuming symbolic routines such as quantifier eliminations, we show that such sets of parameters can be synthesized using a hierarchy of semidefinite programming (SDP). Moreover, we show that, under some standard non-degenerate assumptions, almost all possible valid parameters can be included in the synthesized sets. Such kind of completeness result has previously only been provided by symbolic approaches. Further extensions such as using semialgebraic and general algebraic templates (instead of polynomial ones) and allowing non-polynomial continuous functions in programs are also discussed.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning

To analyse local robustness properties of deep neural networks (DNNs), we present a practical framework from a model learning perspective. Based on black-box model learning with scenario optimisation, we abstract the local behaviour of a DNN via an affine model with the probably approximately correct (PAC) guarantee. From the learned model, we can infer the corresponding PAC-model robustness property. The innovation of our work is the integration of model learning into PAC robustness analysis: that is, we construct a PAC guarantee on the model level instead of sample distribution, which induces a more faithful and accurate robustness evaluation. This is in contrast to existing statistical methods without model learning. We implement our method in a prototypical tool named DeepPAC. As a black-box method, DeepPAC is scalable and efficient, especially when DNNs have complex structures or high-dimensional inputs. We extensively evaluate DeepPAC, with 4 baselines (using formal verification, statistical methods, testing and adversarial attack) and 20 DNN models across 3 datasets, including MNIST, CIFAR-10, and ImageNet. It is shown that DeepPAC outperforms the state-of-the-art statistical method PROVERO, and it achieves more practical robustness analysis than the formal verification tool ERAN. Also, its results are consistent with existing DNN testing work like DeepGini.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Nonlinear Craig Interpolant Generation

Interpolation-based techniques have become popularized in recent years because of their inherently modular and local reasoning, which can scale up existing formal verification techniques like theorem proving, model-checking, abstraction interpretation, and so on, while the scalability is the bottleneck of these techniques. Craig interpolant generation plays a central role in interpolation-based techniques, and therefore has drawn increasing attentions. In the literature, there are various works done on how to automatically synthesize interpolants for decidable fragments of first-order logic, linear arithmetic, array logic, equality logic with uninterpreted functions (EUF), etc., and their combinations. But Craig interpolant generation for non-linear theory and its combination with the aforementioned theories are still in infancy, although some attempts have been done. In this paper, we first prove that a polynomial interpolant of the form $h(\mathbf{x})>0$ exists for two mutually contradictory polynomial formulas $ϕ(\mathbf{x},\mathbf{y})$ and $ψ(\mathbf{x},\mathbf{z})$, with the form $f_1\ge0\wedge\cdots\wedge f_n\ge0$, where $f_i$ are polynomials in $\mathbf{x},\mathbf{y}$ or $\mathbf{x},\mathbf{z}$, and the quadratic module generated by $f_i$ is Archimedean. Then, we show that synthesizing such interpolant can be reduced to solving a semi-definite programming problem (${\rm SDP}$). In addition, we propose a verification approach to assure the validity of the synthesized interpolant and consequently avoid the unsoundness caused by numerical error in ${\rm SDP}$ solving. Finally, we discuss how to generalize our approach to general semi-algebraic formulas.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Over- and Under-Approximating Reachable Sets for Perturbed Delay Differential Equations

This note explores reach set computations for perturbed delay differential equations (DDEs). The perturbed DDEs of interest in this note is a class of DDEs whose dynamics are subject to perturbations, and their solutions feature the local homeomorphism property with respect to initial states. Membership in this class of perturbed DDEs is determined by conducting sensitivity analysis of solution mappings with respect to initial states to impose a bound constraint on the time-lag term. The homeomorphism property of solutions to such class of perturbed DDEs enables us to construct over- and under-approximations of reach sets by performing reachability analysis on just the boundaries of their permitted initial sets, thereby permitting an extension of reach set computation methods for ordinary differential equations to perturbed DDEs. Three examples demonstrate the performance of our approach.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

PAC Model Checking of Black-Box Continuous-Time Dynamical Systems

In this paper we present a novel model checking approach to finite-time safety verification of black-box continuous-time dynamical systems within the framework of probably approximately correct (PAC) learning. The black-box dynamical systems are the ones, for which no model is given but whose states changing continuously through time within a finite time interval can be observed at some discrete time instants for a given input. The new model checking approach is termed as PAC model checking due to incorporation of learned models with correctness guarantees expressed using the terms error probability and confidence. Based on the error probability and confidence level, our approach provides statistically formal guarantees that the time-evolving trajectories of the black-box dynamical system over finite time horizons fall within the range of the learned model plus a bounded interval, contributing to insights on the reachability of the black-box system and thus on the satisfiability of its safety requirements. The learned model together with the bounded interval is obtained by scenario optimization, which boils down to a linear programming problem. Three examples demonstrate the performance of our approach.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Robust Regions of Attraction Generation for State-Constrained Perturbed Discrete-Time Polynomial Systems

In this paper we propose a convex programming based method for computing robust regions of attraction for state-constrained perturbed discrete-time polynomial systems. The robust region of attraction of interest is a set of states such that every possible trajectory initialized in it will approach an equilibrium state while never violating the specified state constraint, regardless of the actual perturbation. Based on a Bellman equation which characterizes the interior of the maximal robust region of attraction as the strict one sub-level set of its unique bounded and continuous solution, we construct a semi-definite program for computing robust regions of attraction. Under appropriate assumptions, the existence of solutions to the constructed semi-definite program is guaranteed and there exists a sequence of solutions such that their strict one sub-level sets inner-approximate and converge to the interior of the maximal robust region of attraction in measure. Finally, we demonstrate the method by two examples.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Unbounded-Time Safety Verification of Stochastic Differential Dynamics

In this paper, we propose a method for bounding the probability that a stochastic differential equation (SDE) system violates a safety specification over the infinite time horizon. SDEs are mathematical models of stochastic processes that capture how states evolve continuously in time. They are widely used in numerous applications such as engineered systems (e.g., modeling how pedestrians move in an intersection), computational finance (e.g., modeling stock option prices), and ecological processes (e.g., population change over time). Previously the safety verification problem has been tackled over finite and infinite time horizons using a diverse set of approaches. The approach in this paper attempts to connect the two views by first identifying a finite time bound, beyond which the probability of a safety violation can be bounded by a negligibly small number. This is achieved by discovering an exponential barrier certificate that proves exponentially converging bounds on the probability of safety violations over time. Once the finite time interval is found, a finite-time verification approach is used to bound the probability of violation over this interval. We demonstrate our approach over a collection of interesting examples from the literature, wherein our approach can be used to find tight bounds on the violation probability of safety properties over the infinite time horizon.

0 citations0 reviewsNo code linkedOpen access