The Complexity of Fragments of Second-Order HyperLTL
Ga\"etan Regaud, Martin Zimmermann
TL;DR
This paper determines the high computational complexity of satisfiability and model-checking problems for various fragments of second-order HyperLTL, an extension of HyperLTL with set quantification over traces.
Contribution
It establishes that these problems are in the analytical hierarchy, providing a comprehensive complexity classification for second-order HyperLTL fragments.
Findings
Satisfiability and model-checking are highly complex, beyond the arithmetical hierarchy.
All studied fragments are in the analytical hierarchy, indicating non-elementary complexity.
The results unify and extend previous complexity analyses of HyperLTL variants.
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
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
Topicssemigroups and automata theory · DNA and Biological Computing