(2020) Controller Synthesis for Hyperproperties.
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.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Uncontrolled Keywords: | complexity theory;protocols;security;maintenance engineering;shape;electronic mail;privacy |
| Divisions: | Bernd Finkbeiner (Reactive Systems Group, RSG) |
| Conference: | CSF IEEE Computer Security Foundations Symposium (was CSFW) |
| Depositing User: | Bernd Finkbeiner |
| Date Deposited: | 04 Mar 2021 16:21 |
| Last Modified: | 04 Mar 2021 16:21 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3379 |
Actions
Actions (login required)
 |
View Item |