Document Open Access Logo

HyperLTL Satisfiability Is Σ₁¹-Complete, HyperCTL* Satisfiability Is Σ₁²-Complete

Authors Marie Fortin , Louwe B. Kuijer , Patrick Totzke , Martin Zimmermann

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2021.47.pdf
  • Filesize: 0.83 MB
  • 19 pages

Document Identifiers

Author Details

Marie Fortin
  • University of Liverpool, UK
Louwe B. Kuijer
  • University of Liverpool, UK
Patrick Totzke
  • University of Liverpool, UK
Martin Zimmermann
  • University of Liverpool, UK

Funding

Partially funded by EPSRC grants EP/S032207/1 and EP/V025848/1.

Acknowledgements

We thank Karoliina Lehtinen and Wolfgang Thomas for fruitful discussions.

Cite As Get BibTex

Marie Fortin, Louwe B. Kuijer, Patrick Totzke, and Martin Zimmermann. HyperLTL Satisfiability Is Σ₁¹-Complete, HyperCTL* Satisfiability Is Σ₁²-Complete. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 47:1-47:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.MFCS.2021.47

Abstract

Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e. satisfiability is undecidable for both logics. 
In this paper we settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is Σ₁¹-complete and HyperCTL* satisfiability is Σ₁²-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove Σ₁²-membership for HyperCTL*, we prove that every satisfiable HyperCTL* sentence has a model that is equinumerous to the continuum, the first upper bound of this kind. We prove this bound to be tight. Finally, we show that the membership problem for every level of the HyperLTL quantifier alternation hierarchy is Π₁¹-complete.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Formal languages and automata theory
Keywords
  • HyperLTL
  • HyperCTL*
  • Satisfiability
  • Analytical Hierarchy

Metrics

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

Related Versions

References

  1. Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour, and Oyendrila Dobe. Probabilistic hyperproperties with nondeterminism. In Dang Van Hung and Oleg Sokolsky, editors, ATVA 2020, volume 12302 of LNCS, pages 518-534. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59152-6_29.
  2. Erika Ábrahám and Borzoo Bonakdarpour. HyperPCTL: A temporal logic for probabilistic hyperproperties. In Annabelle McIver and András Horváth, editors, QEST 2018, volume 11024 of LNCS, pages 20-35. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99154-2_2.
  3. Shreya Agrawal and Borzoo Bonakdarpour. Runtime verification of k-safety hyperproperties in HyperLTL. In CSF 2016, pages 239-252. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/CSF.2016.24.
  4. Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner, and Holger Hermanns. Facets of software doping. In Tiziana Margaria and Bernhard Steffen, editors, ISoLA 2016, Proceedings, Part II, volume 9953 of LNCS, pages 601-608, 2016. URL: https://doi.org/10.1007/978-3-319-47169-3_46.
  5. Ezio Bartocci, Thomas Ferrère, Thomas A. Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. Flavours of sequential information flow. arXiv, 2021. URL: http://arxiv.org/abs/2105.02013.
  6. Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez. A temporal logic for asynchronous hyperproperties. arXiv, 2021. URL: http://arxiv.org/abs/2104.14025.
  7. Béatrice Bérard, Stefan Haar, and Loïc Hélouët. Hyper partial order logic. In Sumit Ganguly and Paritosh K. Pandya, editors, FSTTCS 2018, volume 122 of LIPIcs, pages 20:1-20:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2018.20.
  8. Borzoo Bonakdarpour and Bernd Finkbeiner. Runtime verification for HyperLTL. In Yliès Falcone and César Sánchez, editors, RV 2016, volume 10012 of LNCS, pages 41-45. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-46982-9_4.
  9. Borzoo Bonakdarpour and Bernd Finkbeiner. Controller synthesis for hyperproperties. In CSF 2020, pages 366-379. IEEE, 2020. URL: https://doi.org/10.1109/CSF49147.2020.00033.
  10. Laura Bozzelli, Adriano Peron, and Cesar Sanchez. Asynchronous extensions of hyperltl, 2021. URL: http://arxiv.org/abs/2104.12886.
  11. Noel Brett, Umair Siddique, and Borzoo Bonakdarpour. Rewriting-based runtime verification for alternation-free HyperLTL. In Axel Legay and Tiziana Margaria, editors, TACAS 2017, Part II, volume 10206 of LNCS, pages 77-93, 2017. URL: https://doi.org/10.1007/978-3-662-54580-5_5.
  12. 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.
  13. 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.
  14. Norine Coenen, Bernd Finkbeiner, Christopher Hahn, and Jana Hofmann. The hierarchy of hyperlogics. In LICS 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785713.
  15. Rina S. Cohen and Janusz A. Brzozowski. Dot-depth of star-free events. J. Comput. Syst. Sci., 5(1):1-16, 1971. URL: https://doi.org/10.1016/S0022-0000(71)80003-X.
  16. Rayna Dimitrova, Bernd Finkbeiner, and Hazem Torfah. Probabilistic hyperproperties of Markov decision processes. In Dang Van Hung and Oleg Sokolsky, editors, ATVA 2020, volume 12302 of LNCS, pages 484-500. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59152-6_27.
  17. 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.
  18. Bernd Finkbeiner. Model checking algorithms for hyperproperties (invited paper). In Fritz Henglein, Sharon Shoham, and Yakir Vizel, editors, VMCAI 2021, volume 12597 of LNCS, pages 3-16. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-67067-2_1.
  19. 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.
  20. Bernd Finkbeiner, Christopher Hahn, and Tobias Hans. MGHyper: Checking satisfiability of HyperLTL formulas beyond the ∃^* ∀^* fragment. In ATVA 2018, volume 11138 of LNCS, pages 521-527. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-01090-4_31.
  21. Bernd Finkbeiner, Christopher Hahn, Jana Hofmann, and Leander Tentrup. Realizing omega-regular hyperproperties. In Shuvendu K. Lahiri and Chao Wang, editors, CAV 2020, Part II, volume 12225 of LNCS, pages 40-63. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_4.
  22. Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. Synthesis from hyperproperties. Acta Informatica, 57(1-2):137-163, 2020. URL: https://doi.org/10.1007/s00236-019-00358-2.
  23. Bernd Finkbeiner, Christopher Hahn, and Marvin Stenger. EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties. In Rupak Majumdar and Viktor Kuncak, editors, CAV 2017, Part II, volume 10427 of LNCS, pages 564-570. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_29.
  24. Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. RVHyper: A runtime verification tool for temporal hyperproperties. In Dirk Beyer and Marieke Huisman, editors, TACAS 2018, Part II, volume 10806 of LNCS, pages 194-200. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89963-3_11.
  25. 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.
  26. 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.
  27. Marie Fortin, Louwe B. Kuijer, Patrick Totzke, and Martin Zimmermann. HyperLTL satisfiability is Σ₁¹-complete, HyperCTL^* satisfiability is Σ₁²-complete. arXiv, 2021. URL: http://arxiv.org/abs/2105.04176.
  28. Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. Propositional dynamic logic for hyperproperties. In Igor Konnov and Laura Kovács, editors, CONCUR 2020, volume 171 of LIPIcs, pages 50:1-50:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.50.
  29. 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.
  30. Peter G. Hinman. Recursion-Theoretic Hierarchies. Perspectives in Logic. Cambridge University Press, 2017. URL: https://doi.org/10.1017/9781316717110.
  31. Hsi-Ming Ho, Ruoyu Zhou, and Timothy M. Jones. Timed hyperproperties. Information and Computation, page 104639, 2020. URL: https://doi.org/10.1016/j.ic.2020.104639.
  32. 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.
  33. 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.
  34. 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.
  35. 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/.
  36. Hartley Rogers. Theory of Recursive Functions and Effective Computability. MIT Press, Cambridge, MA, USA, 1987. Google Scholar
  37. Wolfgang Thomas. A combinatorial approach to the theory of omega-automata. Inf. Control., 48(3):261-283, 1981. URL: https://doi.org/10.1016/S0019-9958(81)90663-X.
  38. Wolfgang Thomas. Classifying regular events in symbolic logic. J. Comput. Syst. Sci., 25(3):360-376, 1982. URL: https://doi.org/10.1016/0022-0000(82)90016-2.
  39. Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, and Fan Yang. Linear-time temporal logic with team semantics: Expressivity and complexity. arXiv, 2020. URL: http://arxiv.org/abs/2010.03311.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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