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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Satisfaction of linear temporal logic specifications through recurrence tools for hybrid systems
In this work we formulate the problem of satisfying a linear temporal logic formula on a linear plant with output feedback, through a recent hybrid systems formalism. We relate this problem to the notion of recurrence in…
Local Stability and Stabilization of Quadratic-Bilinear Systems using Petersen's Lemma
Quadratic-bilinear (QB) systems arise in many areas of science and engineering. In this paper, we present a scalable approach for designing locally stabilizing state-feedback control laws and certifying the local stabili…
LEMMACertification of Linear Inclusions for Nonlinear Systems
In this work, we propose novel method for certifying if a given set of vertex linear systems constitute a linear difference inclusion for a nonlinear system. The method relies on formulating the verification of the inclu…
Towards a Certifying Grounder
Grounding, the translation of high-level theories into equivalent quantifier-free formulas, is a crucial step in declarative solving, yet it has so far escaped the proof-logging revolution. When this grounding step is no…
Neural State Classification for Hybrid Systems
We introduce the State Classification Problem (SCP) for hybrid systems, and present Neural State Classification (NSC) as an efficient solution technique. SCP generalizes the model checking problem as it entails classifyi…
ClassificationGeneral Classification