Controller Synthesis for Hyperproperties

TL;DR

This paper addresses the automatic design of controllers to ensure hyperproperties specified in HyperLTL, demonstrating decidability and analyzing complexity for various system types and specification fragments.

Contribution

It proves the decidability of controller synthesis for HyperLTL specifications on finite-state systems and provides a detailed complexity analysis across different system and specification fragments.

Findings

Controller synthesis for HyperLTL is decidable.

Complexity varies with system type and HyperLTL fragment.

Provides a framework for automating hyperproperty enforcement.

Abstract

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.