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

Andrea Bisoffi, Dimos V. Dimarogonas

Onderzoeksoutput: ArticleAcademicpeer review

2 Citaten (Scopus)
61 Downloads (Pure)


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.
Originele taal-2English
Pagina's (van-tot)818-825
Aantal pagina's8
TijdschriftIEEE Transactions on Automatic Control
Nummer van het tijdschrift2
Vroegere onlinedatum2-apr.-2020
StatusPublished - feb.-2021

Citeer dit