Exploiting Invariance Properties to Certify Always and Eventually Signal Temporal Logic Operators for Hybrid Dynamical Systems

In this letter, semantics and characterizations of signal temporal logic formulas for hybrid dynamical systems are presented. Hybrid dynamical systems are given in terms of constrained differential and difference inclusions, which, respectively, capture the continuous evolution and the instantaneous events exhibited by solutions. For such systems, the always and eventually operator of signal temporal logic are studied and characterizations in terms of dynamical properties of hybrid systems are presented – in particular, using invariance and finite-time attractivity properties. Sufficient conditions that guarantee the satisfaction of a signal temporal logic formula for a given system through the satisfaction of an untimed formula for an appropriately defined new system are introduced. Specifically, it is shown that satisfying an (untimed) temporal logic formula involving until operators suffices to certify always and eventually signal temporal logic formulas for hybrid systems.