Document Open Access Logo

The Complexity of Second-Order HyperLTL

Authors Hadar Frenkel , Martin Zimmermann

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CSL.2025.10.pdf
  • Filesize: 0.91 MB
  • 23 pages
HTML5 Logo HTML (experimental)
LIPIcs.CSL.2025.10.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
  • Theory of computation → Logic and verification
Keywords
  • HyperLTL
  • Satisfiability
  • Model-checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Hadar Frenkel and Martin Zimmermann. The Complexity of Second-Order HyperLTL. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.10

Author Details

Hadar Frenkel
  • Bar-Ilan University, Ramat Gan, Israel
Martin Zimmermann
  • Aalborg University, Denmark

Funding

  • Zimmermann, Martin: Supported by DIREC – Digital Research Centre Denmark.

Acknowledgements

This work was initiated by a discussion at Dagstuhl Seminar 23391 "The Futures of Reactive Synthesis" and some results were obtained at Dagstuhl Seminar 24111 "Logics for Dependence and Independence: Expressivity and Complexity". We are grateful to Gaëtan Regaud for finding and fixing a bug in the proof of Theorem 18 and to the reviewers for their detailed and valuable feedback, which improved the paper considerably.

References

  1. Ezio Bartocci, Thomas A. Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. Hypernode automata. In Guillermo A. Pérez and Jean-François Raskin, editors, CONCUR 2023, volume 279 of LIPIcs, pages 21:1-21:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CONCUR.2023.21.
  2. Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez. A temporal logic for asynchronous hyperproperties. In Alexandra Silva and K. Rustan M. Leino, editors, CAV 2021, Part I, volume 12759 of LNCS, pages 694-717. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-81685-8_33.
  3. Raven Beutner and Bernd Finkbeiner. HyperATL^*: A logic for hyperproperties in multi-agent systems. Log. Methods Comput. Sci., 19(2), 2023. URL: https://doi.org/10.46298/LMCS-19(2:13)2023.
  4. Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, and Niklas Metzger. Second-order hyperproperties. In Constantin Enea and Akash Lal, editors, CAV 2023, Part II, volume 13965 of LNCS, pages 309-332. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-37703-7_15.
  5. Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, and Niklas Metzger. Monitoring second-order hyperproperties. In Mehdi Dastani, Jaime Simão Sichman, Natasha Alechina, and Virginia Dignum, editors, AAMAS 2024, pages 180-188. International Foundation for Autonomous Agents and Multiagent Systems / ACM, 2024. URL: https://doi.org/10.5555/3635637.3662865.
  6. Alberto Bombardelli, Laura Bozzelli, César Sánchez, and Stefano Tonetta. Unifying asynchronous logics for hyperproperties. arXiv, 2404.16778, 2024. URL: https://doi.org/10.48550/arXiv.2404.16778.
  7. Laura Bozzelli, Bastien Maubert, and Aniello Murano. On the complexity of model checking knowledge and time. ACM Trans. Comput. Log., 25(1):8:1-8:42, 2024. URL: https://doi.org/10.1145/3637212.
  8. Laura Bozzelli, Bastien Maubert, and Sophie Pinchinat. Unifying hyper and epistemic temporal logics. In Andrew M. Pitts, editor, FoSSaCS 2015, volume 9034 of LNCS, pages 167-182. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46678-0_11.
  9. Laura Bozzelli, Adriano Peron, and César Sánchez. Asynchronous extensions of HyperLTL. In LICS 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470583.
  10. Laura Bozzelli, Adriano Peron, and César Sánchez. Expressiveness and decidability of temporal logics for asynchronous hyperproperties. In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, CONCUR 2022, volume 243 of LIPIcs, pages 27:1-27:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.27.
  11. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In Martín Abadi and Steve Kremer, editors, POST 2014, volume 8414 of LNCS, pages 265-284. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8_15.
  12. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  13. Catalin Dima. Revisiting satisfiability and model-checking for CTLK with synchrony and perfect recall. In Michael Fisher, Fariba Sadri, and Michael Thielscher, editors, CLIMA IX, volume 5405 of LNCS, pages 117-131. Springer, 2008. URL: https://doi.org/10.1007/978-3-642-02734-5_8.
  14. E. Allen Emerson and Joseph Y. Halpern. "sometimes" and "not never" revisited: on branching versus linear time temporal logic. J. ACM, 33(1):151-178, 1986. URL: https://doi.org/10.1145/4904.4999.
  15. Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning About Knowledge. MIT Press, 1995. URL: https://doi.org/10.7551/MITPRESS/5803.001.0001.
  16. Bernd Finkbeiner and Christopher Hahn. Deciding hyperproperties. In Josée Desharnais and Radha Jagadeesan, editors, CONCUR 2016, volume 59 of LIPIcs, pages 13:1-13:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.13.
  17. Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. Algorithms for Model Checking HyperLTL and HyperCTL^*. In Daniel Kroening and Corina S. Pasareanu, editors, CAV 2015, Part I, volume 9206 of LNCS, pages 30-48. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_3.
  18. Bernd Finkbeiner and Martin Zimmermann. The First-Order Logic of Hyperproperties. In STACS 2017, volume 66 of LIPIcs, pages 30:1-30:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.30.
  19. Marie Fortin, Louwe B. Kuijer, Patrick Totzke, and Martin Zimmermann. HyperLTL satisfiability is Σ₁¹-complete, HyperCTL* satisfiability is Σ₁²-complete. In Filippo Bonchi and Simon J. Puglisi, editors, MFCS 2021, volume 202 of LIPIcs, pages 47:1-47:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.MFCS.2021.47.
  20. Marie Fortin, Louwe B. Kuijer, Patrick Totzke, and Martin Zimmermann. HyperLTL satisfiability is highly undecidable, HyperCTL* is even harder. arXiv, 2303.16699, 2023. Journal version of [Marie Fortin et al., 2021]. Under submission. URL: https://doi.org/10.48550/arXiv.2303.16699.
  21. Hadar Frenkel and Martin Zimmermann. The complexity of second-order HyperLTL. arXiv, 2311.15675, 2023. URL: https://doi.org/10.48550/arXiv.2311.15675.
  22. Jens Oliver Gutsfeld, Arne Meier, Christoph Ohrem, and Jonni Virtema. Temporal team semantics revisited. In Christel Baier and Dana Fisman, editors, LICS 2022, pages 44:1-44:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533360.
  23. Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang., 5(POPL):1-29, 2021. URL: https://doi.org/10.1145/3434319.
  24. David Harel. Recurring Dominoes: Making the Highly Undecidable Highly Understandable. North-Holland Mathematical Studies, 102:51-71, 1985. URL: https://doi.org/10.1016/S0304-0208(08)73075-5.
  25. Juha Kontinen and Max Sandström. On the expressive power of TeamLTL and first-order team logic over hyperproperties. In Alexandra Silva, Renata Wassermann, and Ruy J. G. B. de Queiroz, editors, WoLLIC 2021, volume 13038 of LNCS, pages 302-318. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-88853-4_19.
  26. Juha Kontinen, Max Sandström, and Jonni Virtema. Set semantics for asynchronous TeamLTL: Expressivity and complexity. In Jérôme Leroux, Sylvain Lombardy, and David Peleg, editors, MFCS 2023, volume 272 of LIPIcs, pages 60:1-60:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.MFCS.2023.60.
  27. Juha Kontinen, Max Sandström, and Jonni Virtema. A remark on the expressivity of asynchronous TeamLTL and HyperLTL. In Arne Meier and Magdalena Ortiz, editors, FoIKS 2024, volume 14589 of LNCS, pages 275-286. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-56940-1_15.
  28. Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann. Team semantics for the specification and verification of hyperproperties. In Igor Potapov, Paul G. Spirakis, and James Worrell, editors, MFCS 2018, volume 117 of LIPIcs, pages 10:1-10:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.MFCS.2018.10.
  29. Alessio Lomuscio and Franco Raimondi. The complexity of model checking concurrent programs against CTLK specifications. In Hideyuki Nakashima, Michael P. Wellman, Gerhard Weiss, and Peter Stone, editors, AAMAS 2006, pages 548-550. ACM, 2006. URL: https://doi.org/10.1145/1160633.1160733.
  30. Martin Lück. On the complexity of linear temporal logic with team semantics. Theor. Comput. Sci., 837:1-25, 2020. URL: https://doi.org/10.1016/j.tcs.2020.04.019.
  31. Corto Mascle and Martin Zimmermann. The keys to decidable HyperLTL satisfiability: Small models or very simple formulas. In Maribel Fernández and Anca Muscholl, editors, CSL 2020, volume 152 of LIPIcs, pages 29:1-29:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.29.
  32. Amir Pnueli. The temporal logic of programs. In FOCS 1977, pages 46-57. IEEE, October 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  33. Markus N. Rabe. A temporal logic approach to information-flow control. PhD thesis, Saarland University, 2016. URL: http://scidok.sulb.uni-saarland.de/volltexte/2016/6387/.
  34. Gaëtan Regaud and Martin Zimmermann. The complexity of fragments of second-order HyperLTL, 2025. Under preparation. Google Scholar
  35. Hartley Rogers. Theory of Recursive Functions and Effective Computability. MIT Press, Cambridge, MA, USA, 1987. Google Scholar
  36. Ron van der Meyden and Nikolay V. Shilov. Model checking knowledge and time in systems with perfect recall (extended abstract). In C. Pandu Rangan, Venkatesh Raman, and Ramaswamy Ramanujam, editors, FSTTCS 1999, volume 1738 of LNCS, pages 432-445. Springer, 1999. URL: https://doi.org/10.1007/3-540-46691-6_35.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact