We propose a probabilistic hyperlogic called \({\textsf {HyperSt}^{\textsf{2}}}\) that can express hyperproperties of strategies in turn-based stochastic games. To the best of our knowledge, \({\textsf {HyperSt}^{\textsf{2}}}\) is the first hyperlogic for stochastic games. \({\textsf {HyperSt}^{\textsf{2}}}\) can relate probabilities of several independent executions of strategies in a stochastic game. For example, in \({\textsf {HyperSt}^{\textsf{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 \({\textsf {HyperSt}^{\textsf{2}}}\) by comparing it to existing logics for stochastic games, as well as existing hyperlogics. Though the model-checking problem for \({\textsf {HyperSt}^{\textsf{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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A Hyperlogic for Strategies in Stochastic Games

  • Lina Gerlach,
  • Christof Löding,
  • Erika Ábrahám

摘要

We propose a probabilistic hyperlogic called \({\textsf {HyperSt}^{\textsf{2}}}\) that can express hyperproperties of strategies in turn-based stochastic games. To the best of our knowledge, \({\textsf {HyperSt}^{\textsf{2}}}\) is the first hyperlogic for stochastic games. \({\textsf {HyperSt}^{\textsf{2}}}\) can relate probabilities of several independent executions of strategies in a stochastic game. For example, in \({\textsf {HyperSt}^{\textsf{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 \({\textsf {HyperSt}^{\textsf{2}}}\) by comparing it to existing logics for stochastic games, as well as existing hyperlogics. Though the model-checking problem for \({\textsf {HyperSt}^{\textsf{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.