Author(s):

Chatterjee, Krishnendu; Jurdziński, Marcin; Henzinger, Thomas A

Title: 
Simple stochastic parity games

Title Series: 
LNCS

Affiliation 

Abstract: 
Many verification, planning, and control problems can be modeled as games played on statetransition graphs by one or two players whose conflicting goals are to form a path in the graph. The focus here is on simple stochastic parity games, that is, twoplayer games with turnbased probabilistic transitions and omegaregular objectives formalized as parity (Rabin chain) winning conditions. An efficient translation from simple stochastic parity games to nonstochastic parity games is given. As many algorithms are known for solving the latter, the translation yields efficient algorithms for computing the states of a simple stochastic parity game from which a player can win with probability 1. An important special case of simple stochastic parity games are the Markov decision processes with Buchi objectives. For this special case a first provably subquadratic algorithm is given for computing the states from which the single player has a strategy to achieve a Buchi objective with probability 1. For game graphs with m edges the algorithm works in time O(mrootm). Interestingly, a similar technique sheds light on the question of the computational complexity of solving simple Buchi games and yields the first provably subquadratic algorithm, with a running time of O(n(2)/log n) for game graphs with n vertices and O(n) edges.

Conference Title:

CSL: Computer Science Logic

Volume: 
2803

Conference Dates:

August 2530, 2003

Conference Location:

Vienna, Austria

ISBN:

3540454586

Publisher:

Springer

Location:

Berlin, Heidelberg

Date Published:

20030818

Start Page: 
100

End Page:

113

Sponsor: 
This research was supported in part by the DARPA grant F33615C983614, the ONR grant N000140210671, the NSF grants CCR9988172 and CCR0225610, and the Polish KBN grant 7T11C02720.

DOI: 
10.1007/9783540452201_11

Open access: 
no 