Primal-Dual Tests for Safety and Reachability
Primal-Dual Tests for Safety and Reachability
复制标题
安全性和可达性的原始双重测试
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
A. Rantzer
中科院分区：
文献类型：
--
作者：
S. Prajna;A. Rantzer
最近提出了一种使用屏障证书进行安全验证的方法。障碍证书必须满足的条件可以表示为一个凸规划，该规划的可行性意味着系统的安全性，即不存在从给定的一组初始状态开始到达给定的不安全区域的轨迹。这个问题的对偶，即可达性问题，涉及证明从初始集合开始到达另一个给定集合的轨迹的存在性。本文利用凸对偶性和密度函数的概念，证明了可达性也可以通过凸规划来验证。给出了几个用于验证安全性、可达性和其他性质(如可能性)的凸规划。文中举例说明了它们的应用。
A methodology for safety verification using barrier certificates has been proposed recently. Conditions that must be satisfied by a barrier certificate can be formulated as a convex program, and the feasibility of the program implies system safety, in the sense that there is no trajectory starting from a given set of initial states that reaches a given unsafe region. The dual of this problem, i.e., the reachability problem, concerns proving the existence of a trajectory starting from the initial set that reaches another given set. Using insights from convex duality and the concept of density functions, in this paper we show that reachability can also be verified through convex programming. Several convex programs for verifying safety, reachability, and other properties such as eventuality are formulated. Some examples are provided to illustrate their applications.