10.1007/978-3-642-03816-7_4
Chatterjee, Krishnendu
Krishnendu
Chatterjee0000-0002-4561-241X
Henzinger, Thomas A
Thomas A
Henzinger0000−0002−2985−7724
Horn, Florian
Florian
Horn
Stochastic games with finitary objectives
LNCS
Springer
2009
2018-12-11T12:09:24Z
2020-01-16T12:37:16Z
conference
https://research-explorer.app.ist.ac.at/record/4543
https://research-explorer.app.ist.ac.at/record/4543.json
The synthesis of a reactive system with respect to all omega-regular specification requires the solution of a graph game. Such games have been extended in two natural ways. First, a game graph can be equipped with probabilistic choices between alternative transitions, thus allowing the, modeling of uncertain behaviour. These are called stochastic games. Second, a liveness specification can he strengthened to require satisfaction within all unknown but bounded amount of time. These are called finitary objectives. We study. for the first time, the, combination of Stochastic games and finitary objectives. We characterize the requirements on optimal strategies and provide algorithms for Computing the maximal achievable probability of winning stochastic games with finitary parity or Street, objectives. Most notably the set of state's from which a player can win with probability . for a finitary parity objective can he computed in polynomial time even though no polynomial-time algorithm is known in the nonfinitary case.