I study controller synthesis for discrete-time nonlinear stochastic systems: how to design policies that reach a target while avoiding unsafe regions under stochastic disturbances, with a verifiable lower bound on the reach-avoid probability for every state in the initial set over an infinite time horizon.
My work connects stochastic control, formal methods, and learning-enabled control, focusing on the relationship among control performance, probabilistic guarantees, and computational scalability.
Stochastic Systems · Reach-Avoid Control · Formal Guarantees
Robots, autonomous systems, and other cyber-physical systems are often affected by stochastic disturbances, sensor noise, and model mismatch during operation. Even from the same initial state, a controller may induce different system trajectories. For safety-critical tasks, average performance or a small number of successful trajectories is therefore insufficient to characterize system risk.
A reach-avoid task combines reachability and safety: the system must eventually enter a designated target region while remaining outside the unsafe region until it reaches the target. Because the system trajectory is stochastic, this requirement is generally expressed in terms of the probability with which the task is completed, rather than as an assumption of absolute success.
Learning-enabled control methods can use data to address complex, nonlinear, and high-dimensional systems, but training data and finite simulations cover only a limited set of states and disturbance samples. A high empirical success rate does not automatically imply that the controller satisfies the specification for every state in the initial set, under the stated disturbance distribution, and over an infinite time horizon. Safety-critical systems therefore require formal analysis that makes the conditions, scope, and probability lower bound of a guarantee explicit.
Consider a discrete-time stochastic system:
Given a state space Ψ, an initial set Θ, a target set Xg, an unsafe set Xu, and a disturbance distribution 𝒫, the objective is to synthesize a policy π such that, for every x0 ∈ Θ,
Here, δ is a formally verified lower bound on the reach-avoid probability. The research question is not limited to a controller’s empirical success rate in simulation; it asks whether this lower bound holds for every state in the initial set over an infinite time horizon.
Design control policies for nonlinear stochastic systems so that the closed-loop system achieves strong reach-avoid performance under stochastic disturbances.
Certify meaningful lower bounds on reach-avoid satisfaction probabilities for every state in the initial set.
Balance the expressive power of learning-enabled controllers with the computational tractability of subsequent formal verification.
Scale controller synthesis and formal verification to higher-dimensional and nonlinear stochastic systems with more general disturbance distributions.
Formal analysis of reach-avoid control in stochastic systems often relies on certificate functions, which convert difficult infinite-horizon probabilistic properties into checkable functional conditions. As learning methods have entered control, a broader paradigm has emerged: learn a candidate controller or certificate and then subject it to formal verification.
Lyapunov functions, barrier functions, and supermartingale-based certificates provide formal tools for reasoning about stability, safety, and reach-avoid properties. For stochastic systems, certificate functions connect local conditions on expected system evolution to global probabilistic properties.
Reinforcement learning and neural networks can obtain control policies for complex nonlinear systems and can also assist in constructing candidate certificate functions. These methods improve control performance and expressive capacity, but their learned outputs are usually supported empirically on training samples and still require additional formal verification.
Existing approaches often use interval bounds, Lipschitz bounds, and state-space partitioning to verify learned controllers and certificates. As the system dimension increases, the number of state-space partitions grows rapidly. Some verification techniques also assume bounded disturbance spaces, making distributions with unbounded support more difficult to handle directly.
Simulation describes how a controller performs in sampled scenarios. A formal probabilistic guarantee goes further by stating, under a specified system model, initial set, and disturbance distribution, a lower bound on the probability of task completion, giving risk a precise mathematical meaning.
Reach-avoid control considers target reaching, unsafe-region avoidance, and probabilistic requirements during controller synthesis, making the formal guarantee a design objective rather than an after-the-fact check.
Improving the scalability of synthesis and verification for nonlinear, higher-dimensional systems with general stochastic disturbances can extend formal probabilistic guarantees beyond low-dimensional examples to more complex control tasks.
The items below are directly related to my current research direction. For submitted work, only the research topic and submission status that can be made public are listed; no anonymous manuscript, methodological, experimental, or review information is included.
The project studies formal safety verification of neural-network control policies in nonlinear systems.
MEMOCODE 2026 · CCF Class C conference
First authorFormal Aspects of Computing · CCF Class B journal
Second author; advisor is first authorWork on reach-avoid controller synthesis and formal probabilistic guarantees for stochastic systems
CCF Class A conference