The Complexity of Fragments of Second-Order HyperLTL

2025/01/31 by Gaëtan Regaud, Regaud, Gaëtan, Martín Zimmermann +1
Biochemistry, Genetics and Molecular Biology · Computer Science · #DNA and Biological Computing #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.2501.19046

openalex publication_date 2025/01/31 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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

Related

• The Complexity of Second-order HyperLTL
• The Complexity of Generalized HyperLTL with Stuttering and Contexts
• The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas
• HyperLTL Satisfiability is Σ₁¹-complete, HyperCTL* Satisfiability is Σ₁²-complete
• The Complexity of HyperQPTL