  In the formal approach to reactive controller synthesis, a symbolic
controller for a possibly hybrid system is obtained by algorithmically
computing a winning strategy in a two-player game. Such game-solving algorithms
scale poorly as the size of the game graph increases. However, in many
applications, the game graph has a natural hierarchical structure. In this
paper, we propose a modeling formalism and a synthesis algorithm that exploits
this hierarchical structure for more scalable synthesis.
  We define local games on hierarchical graphs as a modeling formalism which
decomposes a large-scale reactive synthesis problem in two dimensions. First,
the construction of a hierarchical game graph introduces abstraction layers,
where each layer is again a two-player game graph. Second, every such layer is
decomposed into multiple local game graphs, each corresponding to a node in the
higher level game graph. While local games have the potential to reduce the
state space for controller synthesis, they lead to more complex synthesis
problems where strategies computed for one local game can impose additional
requirements on lower-level local games.
  Our second contribution is a procedure to construct a dynamic controller for
local game graphs over hierarchies. The controller computes assume-admissible
winning strategies that satisfy local specifications in the presence of
environment assumptions, and dynamically updates specifications and strategies
due to interactions between games at different abstraction layers at each step
of the play. We show that our synthesis procedure is sound: the controller
constructs a play which satisfies all local specifications. We illustrate our
results through an example controlling an autonomous robot in a known,
multistory building.
