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.
Original language | English |
---|---|
Pages (from-to) | 818-825 |
Number of pages | 8 |
Journal | IEEE Transactions on Automatic Control |
Volume | 66 |
Issue number | 2 |
Early online date | 2-Apr-2020 |
DOIs | |
Publication status | Published - Feb-2021 |