Controller Synthesis for Hyperproperties

Bonakdarpour, B. and Finkbeiner, B.
(2020) Controller Synthesis for Hyperproperties.
In: 2020 IEEE 33rd Computer Security Foundations Symposium (CSF).
Conference: CSF IEEE Computer Security Foundations Symposium (was CSFW)

Full text not available from this repository.
Official URL:


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.


Actions (login required)

View Item View Item