Qualitative Reachability in Stochastic BPA Games

Tomas Brazdil, Vaclav Brozek, Antonin Kucera & Jan Obdrzalek
We consider a class of infinite-state stochastic games generated by stateless pushdown automata (or, equivalently, 1-exit recursive state machines), where the winning objective is specified by a regular set of target configurations and a qualitative probability constraint `${>}0$' or `${=}1$'. The goal of one player is to maximize the probability of reaching the target set so that the constraint is satisfied, while the other player aims at the opposite. We show that the winner in...