Stochastic game logic (Q715046)

This paper introduces a temporal logic, referred to as stochastic game logic (SGL), for finite-state probabilistic turn-based multi-player games. The logic is a probabilistic variant of alternating-time temporal logic (ATL) and incorporates elements of probabilistic computation tree logic (PCTL) as well as the possibility to describe path properties by means of deterministic Rabin automata. One of the main novelties of SGL is the ability to bind strategies which allows strategies of nested sub-formulas to depend their decision on the outcome of strategies of outer formulas. This feature makes the model-checking PSPACE-hard, whereas ATL model checking can be solved in polynomial time. The paper considers the complexity of the model checking problem, i.e., does a given probabilistic multi-player game satisfy a SGL-formula, for different classes of strategies. The main results are that this problem is undecidable for history-dependent strategies, PSPACE-complete for memoryless deterministic strategies, and PSPACE-hard and in EXPSPACE for memoryless randomized strategies. The latter result is obtained by an encoding into the first-order theory of the reals. Finally, the paper shows that the model checking problem for the qualitative fragment of SGL (where bounds are either of the form \({=}1\) or \({>}0\)) is PSPACE-complete for memoryless strategies.