基于采样的线性系安全证伪的分辨率完全算法
Sampling-Based Resolution-Complete Algorithms for Safety Falsification of Linear Systems
摘要：
在本文中，我们描述了一种新的方法来检查一个动力系统的安全规格与外源输入在无限的时间范围内，保证终止在有限的时间与一个结论性的答案。我们引入解析完备性的概念来分析安全证伪算法，并提出了基于采样的线性定常离散时间系统安全证伪的解析完备算法.该算法是基于确定性增量搜索过程，探索可达集的可行的反例，以安全地增加分辨率水平的输入。给定输入的目标分辨率，保证算法以违反安全规范的可达状态终止，或者证明在给定分辨率下不存在违反规范的输入。
英文摘要：
In this paper, we describe a novel approach for checking safety specifications of a dynamical system with exogenous inputs over infinite time horizon that is guaranteed to terminate in finite time with a conclusive answer. We introduce the notion of resolution completeness for analysis of safety falsification algorithms and propose sampling-based resolution-complete algorithms for safety falsification of linear time-invariant discrete time systems over infinite time horizon. The algorithms are based on deterministic incremental search procedures, exploring the reachable set for feasible counter examples to safety at increasing resolution levels of the input. Given a target resolution of inputs, the algorithms are guaranteed to terminate either with a reachable state that violates the safety specification, or prove that no input exists at the given resolution that violates the specification.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
