  In this paper, we propose sufficient conditions to guarantee that a linear
temporal logic (LTL) formula of the form p Until q, denoted by $p \mathcal{U}
q$, is satisfied for a hybrid system. Roughly speaking, the formula $p
\mathcal{U} q$ 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 such as
conditional invariance (CI) and eventual conditional invariance (ECI), as well
as finite-time attractivity (FTA) 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. The considered
hybrid system is given in terms of differential and difference inclusions,
which capture the continuous and the discrete dynamics present in the same
system, respectively. Examples illustrate the results throughout the paper.
