Certifying the LTL Formula p Until q in Hybrid Systems

TL;DR

This paper develops sufficient conditions using Lyapunov-like functions to certify that hybrid systems satisfy the LTL formula p Until q, linking invariance and attractivity notions.

Contribution

It introduces a novel approach to verify p Until q in hybrid systems via invariance and attractivity conditions using barrier functions.

Findings

Conditions involving hybrid system data and Lyapunov functions are derived.

The approach is applicable to systems with differential and difference inclusions.

Examples demonstrate the effectiveness of the certification method.

Abstract

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.