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

作     者：Xue, Bai 

作者机构：Key Laboratory of System Software Chinese Academy of Sciences State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing China 

出 版 物：《arXiv》 (arXiv)

年 卷 期：2024年

核心收录：

主　　题：Stochastic systems 

摘      要：In this paper, we examine sufficient and necessary barrier-like conditions for the safety verification and reach-avoid verification of stochastic discrete-time systems. Safety verification aims to certify the satisfaction of the safety property, which stipulates that the probability of the system, starting from a specified initial state, remaining within a safe set is greater than or equal to a specified lower bound. A sufficient and necessary barrier-like condition is formulated for safety verification. In contrast, reach-avoid verification extends beyond safety to include reachability, seeking to certify the satisfaction of the reach-avoid property. It requires that the probability of the system, starting from a specified initial state, reaching a target set eventually while remaining within a safe set until the first hit of the target, is greater than or equal to a specified lower bound. Two sufficient and necessary barrier-like conditions are formulated under certain assumptions. These conditions are derived via relaxing Bellman equations. Copyright © 2024, The Authors. All rights reserved.