Satisfaction of Linear Temporal Logic Specifications Through Recurrence Tools for Hybrid Systems

• 成果类型: Article
• 署名作者: Bisoffi, Andrea; Dimarogonas, Dimos V.
• 署名单位: Royal Institute of Technology
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2020.2984724
• 发表日期: 2021
• 页码: 818-825
• 关键词: Bchi automata; Hybrid dynamical systems; linear temporal logic; Lyapunov-like functions; Output feedback; recurrence; weak stability properties

摘要

In this article, 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.