In order to study control problems for hybrid systems, we generalize hybrid automata to hybrid games -- say, controller vs. plant. If we specify the continuous dynamics by constant lower and upper bounds, we obtain rectangular games. We show that for rectangular games with objectives expressed in LTL (linear temporal logic), the winning states for each player can be computed, and winning strategies can be synthesized. Our result is sharp, as already reachability is undecidable for generalizations of rectangular systems, and optimal -- singly exponential in the game structure and doubly exponential in the LTL objective. We also show how symbolic methods, whose proof of convergence depends on the existence of certain finite quotient structures for hybrid games, can be used to obtain more practical algorithms for solving many rectangular control problems. In this way we are able to systematically generalize the theory of hybrid systems from automata (single-player structures) to games (multi-player structures).
展开▼
