TL;DR
This paper investigates the problem of repairing system models to satisfy hyperproperties specified in HyperLTL, proving decidability and analyzing complexity for various system structures.
Contribution
It establishes decidability of the repair problem for HyperLTL and finite-state systems, with detailed complexity analysis across different HyperLTL fragments and system types.
Findings
Repair problem is decidable for HyperLTL and finite-state structures.
Complexity varies with HyperLTL fragments and system structures.
Provides a foundation for automated system repair based on hyperproperty specifications.
Abstract
We study the repair problem for hyperproperties specified in the temporal logic HyperLTL. Hyperproperties are system properties that relate multiple computation traces. This class of properties includes information flow policies like noninterference and observational determinism. The repair problem is to find, for a given Kripke structure, a substructure that satisfies a given specification. We show that the repair problem is decidable for HyperLTL specifications and finite-state Kripke structures. We provide a detailed complexity analysis for different fragments of HyperLTL and different system types: tree-shaped, acyclic, and general Kripke structures.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
Program Repair for Hyperproperties· youtube
