2026-07-21T20:03:35Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23987 2025-11-12T13:25:18Z ddc:004 open_access

Prophecies All the Way: Game-Based Model-Checking for HyperQPTL Beyond ∀*∃* Winter, Sarah Zimmermann, Martin HyperLTL HyperQPTL model-checking games prophecies 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sarah Winter and Martin Zimmermann 2025 Is Part Of LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2025.37 urn:nbn:de:0030-drops-239872 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.37 eng https://creativecommons.org/licenses/by/4.0/legalcode