Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2506.16775 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911015213465600 |
|---|---|
| author | Gerlach, Lina Löding, Christof Ábrahám, Erika |
| author_facet | Gerlach, Lina Löding, Christof Ábrahám, Erika |
| contents | We propose a probabilistic hyperlogic called HyperSt$^2$ that can express hyperproperties of strategies in turn-based stochastic games. To the best of our knowledge, HyperSt$^2$ is the first hyperlogic for stochastic games. HyperSt$^2$ can relate probabilities of several independent executions of strategies in a stochastic game. For example, in HyperSt$^2$ it is natural to formalize optimality, i.e., to express that some strategy is better than all other strategies, or to express the existence of Nash equilibria. We investigate the expressivity of HyperSt$^2$ by comparing it to existing logics for stochastic games, as well as existing hyperlogics. Though the model-checking problem for HyperSt$^2$ is in general undecidable, we show that it becomes decidable for bounded memory and is in EXPTIME and PSPACE-hard over memoryless deterministic strategies, and we identify a fragment for which the model-checking problem is PSPACE-complete. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_16775 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Hyperlogic for Strategies in Stochastic Games (Extended Version) Gerlach, Lina Löding, Christof Ábrahám, Erika Logic in Computer Science We propose a probabilistic hyperlogic called HyperSt$^2$ that can express hyperproperties of strategies in turn-based stochastic games. To the best of our knowledge, HyperSt$^2$ is the first hyperlogic for stochastic games. HyperSt$^2$ can relate probabilities of several independent executions of strategies in a stochastic game. For example, in HyperSt$^2$ it is natural to formalize optimality, i.e., to express that some strategy is better than all other strategies, or to express the existence of Nash equilibria. We investigate the expressivity of HyperSt$^2$ by comparing it to existing logics for stochastic games, as well as existing hyperlogics. Though the model-checking problem for HyperSt$^2$ is in general undecidable, we show that it becomes decidable for bounded memory and is in EXPTIME and PSPACE-hard over memoryless deterministic strategies, and we identify a fragment for which the model-checking problem is PSPACE-complete. |
| title | A Hyperlogic for Strategies in Stochastic Games (Extended Version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2506.16775 |