Name
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. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1109/CSF49147.2020.00033 | 2020 IEEE 33rd Computer Security Foundations Symposium (CSF) |
Keywords | DocType | ISSN |
hyperproperties,temporal logic HyperLTL,system properties,multiple execution traces,information-flow policies,controller synthesis problem,HyperLTL specifications | Conference | 1940-1434 |
ISBN | Citations | PageRank |
978-1-7281-6573-8 | 1 | 0.35 |
References | Authors | |
25 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Borzoo Bonakdarpour | 1 | 490 | 45.02 |
| Bernd Finkbeiner | 2 | 666 | 69.95 |