Rectangular hybrid games Conference Paper


Author(s): Henzinger, Thomas A; Horowitz, Benjamin; Majumdar, Ritankar S
Title: Rectangular hybrid games
Title Series: LNCS
Affiliation
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 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) [9] 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.
Conference Title: CONCUR: Concurrency Theory
Volume: 1664
Conference Dates: August 24—27, 1999
Conference Location: Eindhoven, The Netherlands
ISBN: 978-3-95977-017-0
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik  
Date Published: 1999-01-01
Start Page: 320
End Page: 335
DOI: 10.1007/3-540-48320-9_23
Notes: This research was supported in part by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the DARPA (NASA Ames) grant NAG2-1214, by the DARPA (Wright-Patterson AFB) grant F33615-98-C-3614, and by the ARO MURI grant DAAH-04-96-1-0341.
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work