Qualitative Reachability in Stochastic BPA Games

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BRÁZDIL Tomáš BROŽEK Václav KUČERA Antonín OBDRŽÁLEK Jan

Year of publication 2011
Type Article in Periodical
Magazine / Source Information and Computation
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords pushdown automata; turn-based games
Description 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 such games can be determined in PTIME for the `>0' constraint, and in NP intersect. coNP for the `=1' constraint. Further, we prove that the winning regions for both players are regular, and we design algorithms which compute the associated finite-state automata. Finally, we show that winning strategies can be synthesized effectively.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.