Certifying the LTL Formula p Until q in Hybrid Systems.

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.