Reach-avoid analysis combines the construction of safety and specific progress guarantees, and is able to formalize many important engineering problems. In this paper we study the reach-avoid verification problem of systems modelled by ordinary differential equations using Lyapunov densities. Firstly, the weak reach-avoid verification is considered. Given an initial set, a safe set and a target set, the weak reach-avoid verification is to verify whether the reach-avoid property (i.e., the system will enter the target set eventually while staying inside the safe set before the first target hitting time) holds for almost all states in the initial set. We propose two novel sufficient conditions using Lyapunov densities for the weak reach-avoid verification. These two sufficient conditions are shown to be weaker than existing ones, providing more possibilities of verifying weak reach-avoid properties successfully. Then, we generalize these conditions to the verification of reach-avoid properties for all states in the initial set. Finally, an example demonstrates theoretical developments of proposed conditions.
Optimization of Lyapunov Invariants in Verification of Software Systems (Extended Version)
Laboratory for Information and Decision Systems (LIDS), Massachusetts Institute of Technology（麻省理工学院信息与决策系统实验室）；School of Aerospace Engineering, Georgia Institute of Technology（佐治亚理工学院航空航天学院）
Comparative Analysis of Barrier-like Function Methods for Reach-Avoid Verification in Stochastic Discrete-Time Systems
University of Chinese Academy of Sciences（中国科学院大学）；East China Normal University（华东师范大学）；Nanyang Technological University（南洋理工大学）；Singapore Management University（新加坡管理大学）
Analytical Lyapunov Function Discovery: An RL-based Generative Approach
Department of Electrical and Computer Engineering, UC San Diego, La Jolla, United States（加州大学圣地亚哥分校电子与计算机工程系）；Swiss Federal Institute of Technology in Lausanne（洛桑联邦理工学院）
Converse Barrier Certificates for Set-Based Stochastic Reach-Avoid Verification
Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；College of Computing and Data Science, Nanyang Technological University（南洋理工大学计算与数据科学学院）
Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所，系统软件重点实验室，计算机科学与技术国家重点实验室）
Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates
University of Oxford, Oxford, United Kingdom（牛津大学）；Radboud University, Nijmegen, the Netherlands（拉德博德大学）；Lund University, Lund, Sweden（隆德大学）；University of Copenhagen, Copenhagen, Denmark（哥本哈根大学）；Ruhr-University Bochum, Bochum, Germany（波鸿鲁尔大学）
