## Rectangular Hybrid Games

*
Thomas A. Henzinger,
Benjamin Horowitz, and Rupak Majumdar*

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 size of the game
structure and doubly exponential in the size of the LTL objective. Our proof
systematically generalizes the theory of hybrid systems from automata
(single-player structures) to games (multi-player structures): we show that
the successively more general infinite-state classes of timed, 2D
rectangular, and rectangular games induce successively weaker, but still
finite, quotient structures called game bisimilarity, game similarity, and
game trace equivalence. These quotients can be used, in particular, to solve
the LTL control problem.

*Proceedings of the
Tenth International Conference on Concurrency Theory*
(CONCUR),
Lecture Notes in Computer Science 1664,
Springer, 1999, pp. 320-335.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1999 Springer.