Decidability and complexity of infinite-state stochastic games
Václav Brožek · 2007
In this thesis we are concerned in 1 1/2-player stochastic games with infinitely many vertices. We are especially interested in games generated by pushdown automata (PDA) and stateless pushdown automata (BPA). We also define the extended reachability objective (ERO) and prove that for PDA games the reachability problem wrt. ERO is undecidable. On the other hand we give a polynomial-time algorithm to decide it for BPA games and we also present an application of our results to PCTL model checking of these games, which we show to be EXPTIME-complete. At the end we show the directions of possible future work, involving solving similar problems for 2 1/2-player games or generalizing ERO to Buchi winning objectives.