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

2025/06/07 by Ting Wu, Wu, Taoran, Dejin Ren +8
Computer Science · Engineering · #Advanced Control Systems Optimization #FOS: Electrical engineering #Formal Methods in Verification #Stability and Control of Uncertain Systems #Systems and Control (eess.SY) #electronic engineering #information engineering

paper · pdf · doi:10.48550/arxiv.2506.06679

openalex publication_date 2025/06/07 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

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.

Citations

• Finite-time Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
• Simultaneous Synthesis and Verification of Neural Control Barrier Functions through Branch-and-Bound Verification-in-the-loop Training
• Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis
• Neural Lyapunov Control for Discrete-Time Systems
• Reach-avoid Controllers Synthesis for Safety Critical Systems
• Safety Verification and Controller Synthesis for Systems with Input Constraints
• Verification and Synthesis of Control Barrier Functions
• Learning Safe Neural Network Controllers with Barrier Certificates
• Neural Lyapunov Control
• Computing Probabilistic Controlled Invariant Sets
• Control Barrier Functions: Theory and Applications
• Controller Synthesis for Discrete-Time Polynomial Systems via Occupation Measures
• Permissive Barrier Certificates for Safe Stabilization Using Sum-of-squares
• Controller design and region of attraction estimation for nonlinear dynamical systems
• Convex computation of the region of attraction of polynomial control systems

Related

• Reach-avoid Verification Based on Convex Optimization
• Upper bounds for the reach-avoid probability via robust optimization
• Reach-Avoid Analysis for Polynomial Stochastic Differential Equations
• Reach-Avoid Problems via Sum-of-Squares Optimization and Dynamic Programming
• Robust Regions of Attraction Generation for State-Constrained Perturbed Discrete-Time Polynomial Systems