Thomas A. Henzinger and Benjamin Horowitz and Rupak Majumdar

EECS Department, University of California, Berkeley

Technical Report No. UCB/CSD-99-1044

, 1999

http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/CSD-99-1044.pdf

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).

---

BibTeX citation:

@techreport{Henzinger:CSD-99-1044,
    Author= {Henzinger, Thomas A. and Horowitz, Benjamin and Majumdar, Rupak},
    Title= {Rectangular Hybrid Games (Extended Abstract)},
    Year= {1999},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/5566.html},
    Number= {UCB/CSD-99-1044},
    Abstract= {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).},
}

EndNote citation:

%0 Report
%A Henzinger, Thomas A. 
%A Horowitz, Benjamin 
%A Majumdar, Rupak 
%T Rectangular Hybrid Games (Extended Abstract)
%I EECS Department, University of California, Berkeley
%D 1999
%@ UCB/CSD-99-1044
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/5566.html
%F Henzinger:CSD-99-1044