The Complexity of Fragments of Second-Order HyperLTL

Gaëtan Regaud, Martin Zimmermann

Published: 2025/1/31

Abstract

We settle the complexity of satisfiability, finite-state satisfiability, and model-checking for several fragments of second-order HyperLTL, which extends HyperLTL with quantification over sets of traces: they are all in the analytical hierarchy and beyond