A Hyperlogic for Strategies in Stochastic Games (Extended Version)

TL;DR

This paper introduces HyperSt$^2$, a novel probabilistic hyperlogic designed to express hyperproperties of strategies in stochastic games, enabling formal reasoning about optimality and equilibria.

Contribution

HyperSt$^2$ is the first hyperlogic tailored for stochastic games, expanding the expressivity and formal analysis capabilities for strategies and equilibria.

Findings

HyperSt$^2$ can express optimality and Nash equilibria.

Model-checking is decidable for bounded memory strategies.

Complexity results include EXPTIME and PSPACE-hard bounds.

Abstract

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.