Document Open Access Logo

Logics for Context-Free Hyperproperties

Authors Sarah Winter , Martin Zimmermann

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2026.54.pdf
  • Filesize: 0.83 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Verification by model checking
  • Theory of computation → Automata over infinite objects
Keywords
  • Hyperproperties
  • model-checking
  • context-free languages

Metrics

Abstract

We introduce a novel logic for the specification of context-free hyperproperties, which capture, e.g., the flow of information in security-critical recursive systems. Intuitively, the logic extends visibly pushdown automata by quantification over traces, just like HyperLTL, the most important logic for regular hyperproperties, extends LTL by quantification over traces. Using a game-based approach, we show that model-checking is decidable for formulas with a single quantifier alternation, provided the stack height of the visibly pushdown automaton only depends on the traces bound to the variables of the first quantifier block. A single quantifier alternation suffices to express many information-flow properties studied in the literature. Complementarily, we show that model-checking is undecidable for formulas with a single quantifier alternation, if the stack behavior of the visibly pushdown automaton may depend on the second quantifier block. This also implies that model-checking is undecidable for almost all fragments with more than one quantifier alternation.

Cite As Get BibTex

Sarah Winter and Martin Zimmermann. Logics for Context-Free Hyperproperties. In 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 386, pp. 54:1-54:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.MFCS.2026.54

Author Details

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

Funding

  • Zimmermann, Martin: Partly supported by the project "Hyperlogics: Expressiveness, Monitorability and Tools (H.-Lo)" of the Icelandic Research Fund, project no. 2612260-051.

References

  1. Rajeev Alur and P. Madhusudan. Visibly pushdown languages. In László Babai, editor, STOC 2004, pages 202-211. ACM, 2004. URL: https://doi.org/10.1145/1007352.1007390.
  2. Ali Bajwa, Minjian Zhang, Rohit Chadha, and Mahesh Viswanathan. Stack-aware hyperproperties. In Sriram Sankaranarayanan and Natasha Sharygina, editors, TACAS 2023, Part I, LNCS, pages 308-325. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30823-9_16.
  3. Raven Beutner and Bernd Finkbeiner. Prophecy variables for hyperproperty verification. In CSF 2022, pages 471-485, , 2022. IEEE. URL: https://doi.org/10.1109/CSF54842.2022.9919658.
  4. Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In Antoni W. Mazurkiewicz and Józef Winkowski, editors, CONCUR 1997, LNCS, pages 135-150. Springer, 1997. URL: https://doi.org/10.1007/3-540-63141-0_10.
  5. Laura Bozzelli. Alternating automata and a temporal fixpoint calculus for visibly pushdown languages. In Luís Caires and Vasco Thudichum Vasconcelos, editors, CONCUR 2007, LNCS, pages 476-491. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74407-8_32.
  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, , 2014. Springer. 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, , 2019. Springer. URL: https://doi.org/10.1007/978-3-030-25540-4_7.
  9. Marie Fortin, Louwe B. Kuijer, Patrick Totzke, and Martin Zimmermann. HyperLTL satisfiability is highly undecidable, HyperCTL^* is even harder. Log. Methods Comput. Sci., 21(1):3, 2025. URL: https://doi.org/10.46298/LMCS-21(1:3)2025.
  10. Hadar Frenkel and Sarai Sheinvald. Realizable and context-free hyperlanguages. In Pierre Ganty and Dario Della Monica, editors, GandALF 2022, EPTCS, pages 114-130, 2022. URL: https://doi.org/10.4204/EPTCS.370.8.
  11. Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. Deciding asynchronous hyperproperties for recursive programs. Proc. ACM Program. Lang., 8(POPL):33-60, 2024. URL: https://doi.org/10.1145/3632844.
  12. Dexter Kozen. Lower bounds for natural proof systems. In FOCS 1977, pages 254-266. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.16.
  13. Christof Löding, P. Madhusudan, and Olivier Serre. Visibly pushdown games. In Kamal Lodaya and Meena Mahajan, editors, FSTTCS 2004, volume 3328 of LNCS, pages 408-420. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30538-5_34.
  14. 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, , 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.29.
  15. Daryl McCullough. Noninterference and the composability of security properties. In SSP 1988, pages 177-186, , 1988. IEEE Computer Society. URL: https://doi.org/10.1109/SECPRI.1988.8110.
  16. Kurt Mehlhorn. Pebbling mountain ranges and its application of DCFL-recognition. In J. W. de Bakker and Jan van Leeuwen, editors, ICALP 1980, LNCS, pages 422-435. Springer, 1980. URL: https://doi.org/10.1007/3-540-10003-2_89.
  17. Amir Pnueli. The temporal logic of programs. In FOCS 1977, pages 46-57, , October 1977. IEEE. URL: https://doi.org/10.1109/SFCS.1977.32.
  18. Adrien Pommellet and Tayssir Touili. Model-checking HyperLTL for pushdown systems. In María-del-Mar Gallardo and Pedro Merino, editors, SPIN 2018, LNCS, pages 133-152. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94111-0_8.
  19. 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/.
  20. A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  21. Sarah Winter and Martin Zimmermann. Prophecies all the way: Game-based model-checking for HyperQPTL beyond ∀^*∃^*. In Patricia Bouyer and Jaco van de Pol, editors, CONCUR 2025, volume 348 of LIPIcs, pages 37:1-37:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2025.37.
  22. Sarah Winter and Martin Zimmermann. Tracy, traces, and transducers: computable counterexamples and explanations for HyperLTL model-checking. Acta Informatica, 62(3):31, 2025. URL: https://doi.org/10.1007/S00236-025-00499-7.
  23. Sarah Winter and Martin Zimmermann. Logics for context-free hyperproperties. arXiv, 2605.04657, 2026. URL: https://doi.org/10.48550/arXiv.2605.04657.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact