×

zbMATH — the first resource for mathematics

Qualitative reachability in stochastic BPA games. (English) Zbl 1237.91035
Summary: 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 \(P\) for the “\(>0\)” constraint, and in \(\mathbf {NP} \cap \mathbf {co}-\mathbf {NP}\) 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.

MSC:
91A15 Stochastic games, stochastic differential games
68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdulla, P.; Henda, N.B.; de Alfaro, L.; Mayr, R.; Sandberg, S., Stochastic games with lossy channels, (), 35-49 · Zbl 1138.91336
[2] Athreya, K.B.; Ney, P.E., Branching processes, (1972), Springer · Zbl 0259.60002
[3] Baeten, J.C.M.; Weijland, W.P., Process algebra, Cambridge tracts in theoretical computer science, vol. 18, (1990), Cambridge University Press · Zbl 0716.68002
[4] Baier, C.; Bertrand, N.; Schnoebelen, Ph., Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties, ACM transactions on computational logic, 9, 1, (2007) · Zbl 1367.68181
[5] Brázdil, T.; Brožek, V.; Forejt, V.; Kučera, A., Reachability in recursive Markov decision processes, Information and computation, 206, 5, 520-537, (2008) · Zbl 1145.91011
[6] V. Brožek, Basic model checking problems for stochastic games, PhD thesis, Masaryk University, Faculty of Informatics, 2009.
[7] Chatterjee, K.; de Alfaro, L.; Henzinger, T., The complexity of stochastic rabin and streett games, (), 878-890 · Zbl 1085.68060
[8] Chatterjee, K.; Jurdziński, M.; Henzinger, T., Simple stochastic parity games, (), 100-113 · Zbl 1116.68493
[9] Chatterjee, K.; Jurdziński, M.; Henzinger, T., Quantitative stochastic parity games, (), 121-130 · Zbl 1318.91027
[10] Condon, A., The complexity of stochastic games, Information and computation, 96, 2, 203-224, (1992) · Zbl 0756.90103
[11] de Alfaro, L.; Majumdar, R., Quantitative solution of omega-regular games, Journal of computer and system sciences, 68, 374-397, (2004) · Zbl 1093.91001
[12] Esparza, J.; Kučera, A.; Schwoon, S., Model-checking LTL with regular valuations for pushdown systems, Information and computation, 186, 2, 355-376, (2003) · Zbl 1078.68081
[13] Etessami, K.; Wojtczak, D.; Yannakakis, M., Recursive stochastic games with positive rewards, (), 711-723 · Zbl 1153.91328
[14] Etessami, K.; Yannakakis, M., Recursive Markov decision processes and recursive stochastic games, (), 891-903 · Zbl 1085.68089
[15] Etessami, K.; Yannakakis, M., Efficient qualitative analysis of classes of recursive Markov decision processes and simple stochastic games, (), 634-645 · Zbl 1136.90499
[16] Etessami, K.; Yannakakis, M., Recursive concurrent stochastic games, (), 324-335 · Zbl 1133.91317
[17] Fagin, R.; Karlin, A.R.; Kleinberg, J.; Raghavan, P.; Rajagopalan, S.; Rubinfeld, R.; Sudan, M.; Tomkins, A., Random walks with “back buttons”, (), 484-493 · Zbl 1296.60191
[18] Harris, T.E., The theory of branching processes, (1963), Springer · Zbl 0117.13002
[19] Hopcroft, J.E.; Ullman, J.D., Introduction to automata theory, languages, and computation, (1979), Addison-Wesley · Zbl 0196.01701
[20] Maitra, A.; Sudderth, W., Finitely additive stochastic games with Borel measurable payoffs, International journal of game theory, 27, 257-267, (1998) · Zbl 0947.91013
[21] Manning, C.; Schütze, H., Foundations of statistical natural language processing, (1999), The MIT Press · Zbl 0951.68158
[22] Martin, D.A., The determinacy of blackwell games, Journal of symbolic logic, 63, 4, 1565-1581, (1998) · Zbl 0926.03071
[23] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific journal of mathematics, 5, 2, 285-309, (1955) · Zbl 0064.26004
[24] Thomas, W., Infinite games and verification, (), 58-64
[25] Vieille, N., Stochastic games: recent results, Handbook of game theory, (2002), Elsevier Science, pp. 1833-1850
[26] Walukiewicz, I., A landscape with games in the background, (), 356-366
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.