학술논문
Satisfaction of Linear Temporal Logic Specifications Through Recurrence Tools for Hybrid Systems
Document Type
Periodical
Author
Source
IEEE Transactions on Automatic Control IEEE Trans. Automat. Contr. Automatic Control, IEEE Transactions on. 66(2):818-825 Feb, 2021
Subject
Language
ISSN
0018-9286
1558-2523
2334-3303
1558-2523
2334-3303
Abstract
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.