This paper introduces operators, semantics, characterizations, and solution-independent conditions to guarantee temporal logic specifications for hybrid dynamical systems. Hybrid dynamical systems are given in terms of differential inclusions -- capturing the continuous dynamics -- and difference inclusions -- capturing the discrete dynamics or events -- with constraints. State trajectories (or solutions) to such systems are parameterized by a hybrid notion of time. For such broad class of solutions, the operators and semantics needed to reason about temporal logic are introduced. Characterizations of temporal logic formulas in terms of dynamical properties of hybrid systems are presented -- in particular, forward invariance and finite time attractivity. These characterizations are exploited to formulate sufficient conditions assuring the satisfaction of temporal logic formulas -- when possible, these conditions do not involve solution information. Combining the results for formulas with a single operator, ways to certify more complex formulas are pointed out, in particular, via a decomposition using a finite state automaton. Academic examples illustrate the results throughout the paper.
Hybrid control strategy for a semi active suspension system using fuzzy logic and bio-inspired chaotic fruit fly algorithm
Carnegie Mellon University（卡内基梅隆大学）；Jadavpur University（贾达普大学）；Sun Yat-sen University-Carnegie Mellon University (SYSU-CMU) Joint Institute of Engineering（中山大学-卡内基梅隆大学（SYSU-CMU）联合工程学院）
