发表机构
ios.ac.cn（中国科学院自动化研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文针对离散时间随机系统无限时域可达-避让验证，提出基于连续障碍函数的充要条件，并利用SOS和SDP方法实现多项式障碍函数的综合，同时保证方法的可靠性与完备性。
AI 中文摘要
本文针对离散时间随机系统的无限时域可达-避让验证问题，利用连续障碍函数发展了必要且充分的障碍类特征刻画。已有结果通过涉及可测或下半连续障碍函数的函数不等式建立了必要且充分的条件。然而，此类函数的有限正则性可能阻碍其数值逼近和计算综合。基于我们先前针对有限时域可达-避让验证的障碍类条件，我们证明该条件也可用于无限时域可达-避让验证，并且在对转移核施加一致绝对连续性条件时，只要初始集合中每个状态的精确可达-避让概率严格大于给定阈值，就存在连续障碍函数。我们进一步证明，所得连续障碍函数可以被多项式函数一致逼近，同时保持所需的障碍类条件。对于多项式系统，我们将这些条件表述为紧致基本半代数集上的多项式正性约束。随后，Putinar's Positivstellensatz将正性条件转化为平方和（SOS）证书，从而产生用于综合多项式障碍函数的半定规划（SDP）公式。我们建立了所得基于SOS方法的可靠性和完备性。最后，两个数值示例说明了理论结果并展示了所提出的SDP方法。
英文摘要
This paper develops necessary and sufficient barrier-like characterizations using continuous barrier functions for infinite-horizon reach-avoid verification of discrete-time stochastic systems. Existing results establish necessary and sufficient conditions in terms of functional inequalities involving measurable or lower semicontinuous barrier functions. However, the limited regularity of such functions may hinder their numerical approximation and computational synthesis. Building on our previous barrier-like condition for finite-horizon reach-avoid verification, we show that this condition can also be used for infinite-horizon reach-avoid verification and, under a uniform absolute continuity condition on the transition kernels, admits a continuous barrier function whenever the exact reach-avoid probability is strictly larger than the prescribed threshold for every state in the initial set. We further show that the resulting continuous barrier function can be uniformly approximated by a polynomial one while preserving the required barrier-like conditions. For polynomial systems, we formulate these conditions as polynomial positivity constraints over compact basic semialgebraic sets. Putinar's Positivstellensatz then converts the positivity conditions into sum-of-squares (SOS) certificates, yielding semidefinite programming (SDP) formulations for synthesizing polynomial barrier functions. We establish both soundness and completeness of the resulting SOS-based procedure. Finally, two numerical examples illustrate the theoretical results and demonstrate the resulting SDP approach.
