论文标题
通过混合系统的复发工具对线性时间逻辑规格的满意度
Satisfaction of linear temporal logic specifications through recurrence tools for hybrid systems
论文作者
论文摘要
在这项工作中，我们制定了通过最近的混合系统形式主义在带有输出反馈的线性植物上满足线性时间逻辑公式的问题。我们将这个问题与为被考虑的形式主义引入的复发概念联系起来，然后我们扩展了类似Lyapunov的条件，以重复出现开放的，无限的集合。提议的放松条件之一允许证明合适的集合的复发，这保证了植物的高级演变可以满足该配方，而无需依赖植物的离散化。模拟说明了提出的方法。
In this work we formulate the problem of satisfying a linear temporal logic formula on a linear plant with output feedback, through a recent hybrid systems formalism. We relate this problem to the notion of recurrence introduced for the considered formalism, and we then extend Lyapunov-like conditions for recurrence of an open, unbounded set. One of the proposed relaxed conditions allows certifying recurrence of a suitable set, and this guarantees that the high-level evolution of the plant satisfies the formula, without relying on discretizations of the plant. Simulations illustrate the proposed approach.
