The Complexity of Generalized HyperLTL with Stuttering and Contexts
For researchers in formal verification and hyperproperties, this paper provides a precise complexity classification for an expressive logic, revealing that adding stuttering or contexts makes model-checking and finite-state satisfiability undecidable.
The paper settles the complexity of satisfiability, finite-state satisfiability, and model-checking for generalized HyperLTL with stuttering and contexts. Satisfiability is Σ₁¹-complete (same as HyperLTL), while model-checking and finite-state satisfiability are equivalent to truth in second-order arithmetic, much harder than HyperLTL.
We settle the complexity of satisfiability, finite-state satisfiability, and model-checking for generalized HyperLTL with stuttering and contexts, an expressive logic for the specification of asynchronous hyperproperties. Such properties cannot be specified in HyperLTL, as it is restricted to synchronous hyperproperties. Nevertheless, we prove that satisfiability is $Σ_1^1$-complete and thus not harder than for HyperLTL. On the other hand, we prove that model-checking and finite-state satisfiability are equivalent to truth in second-order arithmetic, and thus much harder than the decidable HyperLTL model-checking problem and the $Σ_0^1$-complete HyperLTL finite-state satisfiability problem. The lower bounds for the model-checking and finite-state satisfiability problems hold even when only allowing stuttering or only allowing contexts.