The Complexity of Second-order HyperLTL
This work addresses complexity challenges in formal verification for logics like HyperLTL, providing foundational insights but is incremental in refining known theoretical bounds.
The paper determines the complexity of second-order HyperLTL problems, showing that satisfiability, finite-state satisfiability, and model-checking are equivalent to truth in third-order arithmetic, and analyzes fragments and semantics to identify reductions in complexity, such as one fragment achieving Σ₁²-completeness for satisfiability.
We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that have been introduced with the aim to facilitate effective model-checking by restricting the sets one can quantify over. The first one restricts second-order quantification to smallest/largest sets that satisfy a guard while the second one restricts second-order quantification further to least fixed points of (first-order) HyperLTL definable functions. All three problems for the first fragment are still equivalent to truth in third-order arithmetic while satisfiability for the second fragment is $Σ_1^2$-complete, and finite-state satisfiability and model-checking are equivalent to truth in second-order arithmetic. Finally, we also introduce closed-world semantics for second-order HyperLTL, where set quantification ranges only over subsets of the model, while set quantification in standard semantics ranges over arbitrary sets of traces. Here, satisfiability for the least fixed point fragment becomes $Σ_1^1$-complete, but all other results are unaffected.