Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
<|reference_start|>Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time 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.<|reference_end|>
@article{xue2024sufficient,
    title={Sufficient and Necessary Barrier-like Conditions for Safety and
  Reach-avoid Verification of Stochastic Discrete-time Systems},
    author={Bai Xue},
    journal={arXiv preprint arXiv:2408.15572},
    year={2024},
    archivePrefix={arXiv},
    eprint={2408.15572},
    primaryClass={eess.SY cs.SY}
}