  We investigate the problem of controller synthesis for hyperproperties
specified in the temporal logic HyperLTL. Hyperproperties are system properties
that relate multiple execution traces. Hyperproperties can elegantly express
information-flow policies like noninterference and observational determinism.
The controller synthesis problem is to automatically design a controller for a
plant that ensures satisfaction of a given specification in the presence of the
environment or adversarial actions. We show that the controller synthesis
problem is decidable for HyperLTL specifications and finite-state plants. We
provide a rigorous complexity analysis for different fragments of HyperLTL and
different system types: tree-shaped, acyclic, and general graphs.
