Abstract

We study stochastic turn based games played by two players ($\Box$ and $\Diamond$) and environment $\bigcirc$. The aim of the player $\Box$ is to provide a strategy that ensures satisfying of an objective no matter what strategy the player $\Diamond$ provides. Objectives are specified by the formulae of the logic PCTL (probabilistic extension of CTL) or \PE{} (logic similar to PCTL$^*$ with B\"uchi automata as temporal operators). These games are not determined and the problem of synthesizing a winning strategy is undecidable. We prove that if we restrict ourselves to memoryless strategies, problems become decidable. For certain subclasses, we give completeness results. Our main result is synthesizing finite memory winning strategies for \ohp games and \PE{} objectives. We show that this problem is decidable in 2-\EXPTIME. …víceméně