UC Santa Cruz

This dissertation focuses on developing tools for certifying temporal logic properties in hybrid dynamical systems that combine continuous and discrete dynamics. In particular, operators, semantics, characterizations, and solution-independent conditions to guarantee temporal logic specifications for hybrid dynamical systems are presented. 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. Characterizations of temporal logic formulas in terms of dynamical properties of hybrid systems are presented -- in particular, forward invariance, conditional 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. Notions for specifying dynamical properties of systems with robustness to perturbations are proposed. Characterizations of basic signal temporal logic formulas are presented. 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. An object grasping application and academic examples are given to illustrate the results.