Deciding Hyperproperties Combined with Functional Specifications

TL;DR

This paper explores the satisfiability of HyperLTL with complex quantifier prefixes, identifying decidable fragments and proposing a new algorithm, thereby advancing understanding of hyperproperty verification in system specifications.

Contribution

It defines safety and liveness fragments of HyperLTL with complex quantifiers, characterizes their satisfiability complexity, and introduces a new algorithm for satisfiability checking.

Findings

Identified decidable fragments of HyperLTL with $orall^*orall^*$ and $orall^*orall^*orall^*$ quantifiers.

Characterized the complexity of satisfiability for these fragments.

Proposed a new, albeit incomplete, algorithm for $orallorall^*$-HyperLTL satisfiability.

Abstract

We study satisfiability for HyperLTL with a $\forall^*\exists^*$ quantifier prefix, known to be highly undecidable in general. HyperLTL can express system properties that relate multiple traces (so-called hyperproperties), which are often combined with trace properties that specify functional behavior on single traces. Following this conceptual split, we first define several safety and liveness fragments of $\forall^*\exists^*$ HyperLTL, and characterize the complexity of their (often much easier) satisfiability problem. We then add LTL trace properties as functional specifications. Though (highly) undecidable in many cases, this way of combining "simple" HyperLTL and arbitrary LTL also leads to interesting new decidable fragments. This systematic study of $\forall^*\exists^*$ fragments is complemented by a new (incomplete) algorithm for $\forall\exists^*$-HyperLTL satisfiability.