Qualitative analysis, model checking, and controller synthesis of hybrid systems

This thesis addresses problems of qualitative analysis, model checking, and controller synthesis of hybrid systems. The contributions are the following. We derive conditions for completeness of the space of non-Zeno hybrid trajectories accepted by a hybrid automaton. We derive conditions for continuous selections of hybrid trajectories, which had been elusive due to the inherent discontinuities permitted by hybrid systems. These results provide tools for qualitative analysis and are obtained in the general setting of hybrid systems with differential inclusions. Next, we present a new method of obtaining bisimulations for hybrid systems which is inspired by a geometric interpretation of the bisimulation for timed automata. This provides a much needed breakthrough for applying model checking to hybrid automata with non-trivial dynamics. We demonstrate the method through examples drawn from coordinated autonomous agent applications and from widely used models such as linear systems. Next, we turn to problems of controller synthesis. We present a theory of optimal controller synthesis for continuous time and hybrid systems using bisimulation. The resulting formulation leads to a dynamic programming problem on a finite graph. We obtain an single-pass algorithmic solution to this problem. Finally, we consider strategies for model checking when we do not have the benefit of bisimulation, as in hybrid systems with differential inclusions. We present a new intuitive proof of decidability of reachability for rectangular automata.