2026-08-18T01:33:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22767 2025-10-02T11:31:28Z ddc:004 open_access

The Complexity of Second-Order HyperLTL Frenkel, Hadar Zimmermann, Martin HyperLTL Satisfiability Model-checking 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 Σ₁¹-complete, i.e., only as hard as for (first-order) HyperLTL and therefore much less complex. Finally, finite-state satisfiability and model-checking are in Σ₂² and are Σ₁¹-hard, and thus also less complex than for full second-order HyperLTL. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Hadar Frenkel and Martin Zimmermann 2025 Is Part Of LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2025.10 urn:nbn:de:0030-drops-227679 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.10 eng https://creativecommons.org/licenses/by/4.0/legalcode