Sie befinden Sich nicht im Netzwerk der Universität Paderborn. Der Zugriff auf elektronische Ressourcen ist gegebenenfalls nur via VPN oder Shibboleth (DFN-AAI) möglich. mehr Informationen...
Certifying the LTL Formula p Until q in Hybrid Systems
Ist Teil von
IEEE transactions on automatic control, 2023-07, Vol.68 (7), p.4451-4458
Ort / Verlag
Institute of Electrical and Electronics Engineers
Erscheinungsjahr
2023
Link zum Volltext
Quelle
IEEE Electronic Library (IEL)
Beschreibungen/Notizen
In this paper, we propose sufficient conditions to guarantee that a linear temporal logic formula of the form p Until q , denoted by pUq , is satisfied for a hybrid system. Roughly speaking, the formula pUq 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 paper.