Prophecies all the Way: Game-based Model-Checking for HyperQPTL beyond $\forall^*\exists^*$
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913966813347840 |
|---|---|
| author | Winter, Sarah Zimmermann, Martin |
| author_facet | Winter, Sarah Zimmermann, Martin |
| contents | 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 $\forall^*\exists^*$-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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_08575 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Prophecies all the Way: Game-based Model-Checking for HyperQPTL beyond $\forall^*\exists^*$ Winter, Sarah Zimmermann, Martin Logic in Computer Science Formal Languages and Automata Theory 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 $\forall^*\exists^*$-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. |
| title | Prophecies all the Way: Game-based Model-Checking for HyperQPTL beyond $\forall^*\exists^*$ |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2504.08575 |