发表机构
Institute of Software, Chinese Academy of Sciences; College of Computing and Data Science, Nanyang Technological University（中国科学院软件研究所; 南洋理工大学计算与数据科学学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文针对紧致初始集合，将随机离散时间系统单个初始状态的反向障碍证书表征扩展至集合设定，解决了初始集合的随机可达规避验证问题。
AI 中文摘要
近期研究针对从单个初始状态出发的随机离散时间系统的无限时域可达规避验证，建立了必要且充分的类障碍条件。然而，此类反向表征是否可扩展至初始状态集合的问题仍未解决。本文针对紧致初始集合给出了肯定回答。我们考虑一种均匀可达规避规范，要求紧致集合内每个初始状态的可达规避概率超过规定阈值。在适当假设（包括连续系统转移及严格均匀概率裕度）下，我们将逐点反向表征扩展至均匀设定。
英文摘要
Recent work established sufficient and necessary barrier-like conditions for infinite-horizon reach-avoid verification of stochastic discrete-time systems from a single initial state. Whether such a converse characterization extends to a set of initial states, however, remains open. In this paper, we answer this question affirmatively for compact initial sets. We consider a uniform reach-avoid specification requiring the reach-avoid probability to exceed a prescribed threshold for every initial state in a compact set. Under appropriate assumptions, including continuous system transitions, together with a strict uniform probability margin, we extend the pointwise converse characterization to the uniform setting.
