# Controller Synthesis for Hyperproperties

arXiv: https://arxiv.org/abs/2101.08880 · HTML: https://mlsanity.com/paper/2101.08880/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 Jan 2021.

## Built on by (most cited first, 2 of 2)

- [Deductive Controller Synthesis for Probabilistic Hyperproperties](https://mlsanity.com/paper/2307.04503/) (2023)
- [Hyperproperty-Constrained Secure Reinforcement Learning](https://mlsanity.com/paper/2508.00106/) (2025)

## Abstract (arXiv)

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.