Deciding Hyperproperties

This talk is based on the paper “Deciding Hyperproperties” by Bernd Finkbeiner and Christopher Hahn, which appeared on the 27th International Conference on Concurrency Theory (CONCUR 2016). 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. 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.

Authors

• Bernd Finkbeiner CISPA Helmholtz Center for Information Security
• Christopher Hahn

Keywords

No keywords are indexed for this paper.