TL;DR
This paper investigates the satisfiability problem of HyperLTL, a logic for expressing hyperproperties involving multiple traces, establishing complexity results and decidability for various classes of formulas.
Contribution
It provides a comprehensive complexity analysis of HyperLTL satisfiability, identifying decidable cases and establishing the boundaries of decidability.
Findings
Satisfiability is PSPACE-complete for alternation-free formulas.
Satisfiability is EXPSPACE-complete for exists-forall formulas.
Satisfiability is undecidable for forall-exists formulas.
Abstract
Hyperproperties, like observational determinism or symmetry, cannot be expressed as properties of individual computation traces, because they describe a relation between multiple computation traces. HyperLTL is a temporal logic that captures such relations through trace variables, which are introduced through existential and universal trace quantifiers and can be used to refer to multiple computations at the same time. In this paper, we study the satisfiability problem of HyperLTL. We show that the problem is PSPACE-complete for alternation-free formulas (and, hence, no more expensive than LTL satisfiability), EXPSPACE-complete for exists-forall-formulas, and undecidable for forall-exists-formulas. Many practical hyperproperties can be expressed as alternation-free formulas. Our results show that both satisfiability and implication are decidable for such properties.
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
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.