Certifying the LTL Formula p Until q in Hybrid Systems

• 成果类型: Article
• 署名作者: Han, Hyejin; Maghenem, Mohamed; Sanfelice, Ricardo G.
• 署名单位: University of California System; University of California Santa Cruz; Communaute Universite Grenoble Alpes; Institut National Polytechnique de Grenoble; Universite Grenoble Alpes (UGA); Centre National de la Recherche Scientifique (CNRS)
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2022.3207417
• 发表日期: 2023
• 页码: 4451-4458
• 关键词: Hybrid systems; invariance notions; Lyapunov methods; temporal logic

摘要

In this article, we propose sufficient conditions to guarantee that a linear temporal logic formula of the form p Until q, denoted by p Uq, is satisfied for a hybrid system. Roughly speaking, the formula p Uq is satisfied means that the solutions, initially satisfying proposition p, keep satisfying this proposition until proposition q is satisfied. To certify such a formula, connections to invariance notions-specifically, conditional invariance and eventual conditional invariance-as well as finite-time convergence properties are established. As a result, sufficient conditions involving the data of the hybrid system and an appropriate choice of Lyapunov-like functions, such as barrier functions, are derived. Examples illustrate the results throughout the article.