Certifying the LTL Formula p Until q in Hybrid Systems

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.