Document Open Access Logo

Prophecies All the Way: Game-Based Model-Checking for HyperQPTL Beyond ∀*∃*

Authors Sarah Winter , Martin Zimmermann

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.37.pdf
  • Filesize: 0.98 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Verification by model checking
Keywords
  • HyperLTL
  • HyperQPTL
  • model-checking games
  • prophecies

Metrics

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

Abstract

Model-checking HyperLTL, a temporal logic expressing properties of sets of traces with applications to information-flow based security and privacy, has a decidable, but TOWER-complete, model-checking problem. While the classical model-checking algorithm for full HyperLTL is automata-theoretic, more recently, a game-based alternative for the ∀*∃*-fragment has been presented.
Here, we employ imperfect information-games to extend the game-based approach to full HyperQPTL, which features arbitrary quantifier prefixes and quantification over propositions and can express every ω-regular hyperproperty. As a byproduct of our game-based algorithm, we obtain finite-state implementations of Skolem functions via transducers with lookahead that explain satisfaction or violation of HyperQPTL properties.

Cite As Get BibTex

Sarah Winter and Martin Zimmermann. Prophecies All the Way: Game-Based Model-Checking for HyperQPTL Beyond ∀*∃*. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 37:1-37:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.37

Author Details

Sarah Winter
  • IRIF, Université Paris Cité, Paris, France
Martin Zimmermann
  • Aalborg University, Denmark

Funding

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

References

  1. Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theor. Comput. Sci., 82(2):253-284, 1991. URL: https://doi.org/10.1016/0304-3975(91)90224-P.
  2. Luca Aceto, Antonis Achilleos, Elli Anastasiadi, and Adrian Francalanza. Monitoring hyperproperties with circuits. In Mohammad Reza Mousavi and Anna Philippou, editors, FORTE 2022, volume 13273 of LNCS, pages 1-10. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-08679-3_1.
  3. Rajeev Alur, Emmanuel Filiot, and Ashutosh Trivedi. Regular transformations of infinite strings. In LICS 2012, pages 65-74. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/LICS.2012.18.
  4. Dietmar Berwanger, Anup Basil Mathew, and Marie van den Bogaard. Hierarchical information and the synthesis of distributed strategies. Acta Informatica, 55(8):669-701, 2018. URL: https://doi.org/10.1007/S00236-017-0306-5.
  5. Raven Beutner and Bernd Finkbeiner. Prophecy variables for hyperproperty verification. In CSF 2022, pages 471-485. IEEE, 2022. URL: https://doi.org/10.1109/CSF54842.2022.9919658.
  6. 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.
  7. 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.
  8. Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. Verifying hyperliveness. In Isil Dillig and Serdar Tasiran, editors, CAV 2019, Part I, volume 11561 of LNCS, pages 121-139. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25540-4_7.
  9. Samuel Eilenberg. Automata, languages, and machines. A. Pure and applied mathematics. Academic Press, 1974. URL: https://www.worldcat.org/oclc/310535248.
  10. 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.
  11. Joost Engelfriet. Top-down tree transducers with regular look-ahead. Math. Syst. Theory, 10:289-303, 1977. URL: https://doi.org/10.1007/BF01683280.
  12. Emmanuel Filiot and Sarah Winter. Synthesizing computable functions from rational specifications over infinite words. Int. J. Found. Comput. Sci., 35(01n02):179-214, 2024. URL: https://doi.org/10.1142/S012905412348009X.
  13. 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.
  14. 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.
  15. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002. URL: https://doi.org/10.1007/3-540-36387-4.
  16. Frederick A. Hosch and Lawrence H. Landweber. Finite delay solutions for sequential conditions. In ICALP 1972, pages 45-60, 1972. Google Scholar
  17. Felix Klein and Martin Zimmermann. How much lookahead is needed to win infinite games? Log. Methods Comput. Sci., 12(3), 2016. URL: https://doi.org/10.2168/LMCS-12(3:4)2016.
  18. 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.
  19. Daryl McCullough. Noninterference and the composability of security properties. In SSP 1988, pages 177-186. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/SECPRI.1988.8110.
  20. 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.
  21. Amir Pnueli and Roni Rosner. Distributed reactive systems are hard to synthesize. In FOCS 1990, Volume II, pages 746-757. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/FSCS.1990.89597.
  22. 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/.
  23. A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for Büchi automata with appplications to temporal logic. Theor. Comput. Sci., 49:217-237, 1987. URL: https://doi.org/10.1016/0304-3975(87)90008-9.
  24. Sarah Winter and Martin Zimmermann. Finite-state strategies in delay games. Inf. Comput., 272:104500, 2020. URL: https://doi.org/10.1016/J.IC.2019.104500.
  25. Sarah Winter and Martin Zimmermann. Prophecies all the way: Game-based model-checking for HyperQPTL beyond ∀^*∃^*. arXiv, 2504.08575, 2025. URL: https://doi.org/10.48550/arXiv.2504.08575.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact