Skip to main content
SpringerLink
Log in

Expected Termination Time in BPA Games

  • Conference paper
Book cover Automated Technology for Verification and Analysis

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8172))

Abstract

We consider the problem of computing the value and finding the epsilon-optimal strategies for concurrent Basic Process Algebra games, which is a subclass of two-player infinite-state stochastic games with imperfect information. These games are played on the transition graph of stateless pushdown systems, or equivalently 1-exit recursive state machines, and can model recursive procedural program execution with probabilistic transitions. The objective of one player in these games is to minimise the expected termination time of such a program, while the objective of the other is to maximise it. We show that the quantitative decision questions regarding the value of the game as well as checking whether this value is infinite can be answered in PSPACE. We also show the latter problem to be as hard as the square root sum, whose containment even in the polynomial hierarchy is an open problem since the 1970s. Furthermore, an optimal strategy may require an infinite amount of memory in general, but we show that both player have epsilon-optimal stackless&memoryless strategies (i.e. strategies that do not use memory nor depend on the stack content). Finally, we show how to find such strategies using a strategy improvement algorithm.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Allender, E., Bürgisser, P., Kjeldgaard-Pedersen, J., Miltersen, P.B.: On the complexity of numerical analysis. SIAM Journal on Computing 38(5), 1987–2006 (2009)

    Article  MathSciNet  Google Scholar 

  2. Brázdil, T., Brožek, V., Kučera, A., Obdrzálek, J.: Qualitative reachability in stochastic BPA games. Information and Computation 209(8), 1160–1183 (2011)

    Article  MathSciNet  Google Scholar 

  3. Brázdil, T., Kučera, A., Novotný, P., Wojtczak, D.: Minimizing expected termination time in one-counter Markov decision processes. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 141–152. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  4. Condon, A.: The complexity of stochastic games. Inf. & Comp. 96(2), 203–224 (1992)

    Article  MathSciNet  Google Scholar 

  5. de Alfaro, L., Henzinger, T.A.: Concurrent omega-regular games. In: Proc. of the 15th IEEE Symposium on Logic in Computer Science, pp. 141–154. IEEE Computer Society Press (2000)

    Google Scholar 

  6. de Alfaro, L., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. In: Proc. of FOCS 1998, pp. 564–575 (1998)

    Google Scholar 

  7. de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374–397 (2004)

    Article  MathSciNet  Google Scholar 

  8. Esparza, J., Kučera, A., Mayr, R.: Model checking probabilistic pushdown automata. In: Proc. of 19th IEEE LICS 2004 (2004)

    Google Scholar 

  9. Etessami, K., Wojtczak, D., Yannakakis, M.: Recursive stochastic games with positive rewards. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part I. LNCS, vol. 5125, pp. 711–723. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  10. Etessami, K., Yannakakis, M.: Algorithmic verification of recursive probabilistic state machines. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 253–270. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of non-linear equations. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol. 3404, pp. 340–352. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  12. Etessami, K., Yannakakis, M.: Recursive Markov decision processes and recursive stochastic games. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 891–903. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Etessami, K., Yannakakis, M.: Efficient qualitative analysis of classes of recursive Markov decision processes and simple stochastic games. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 634–645. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Etessami, K., Yannakakis, M.: Recursive concurrent stochastic games. Logical Methods in Computer Science 4(4) (2008)

    Google Scholar 

  15. Etessami, K., Yannakakis, M.: On the complexity of Nash equilibria and other fixed points. SIAM Journal on Computing 39(6), 2531–2597 (2010)

    Article  MathSciNet  Google Scholar 

  16. Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer (1997)

    Chapter  Google Scholar 

  17. Garey, M.R., Graham, R.L., Johnson, D.S.: Some NP-complete geometric problems. In: Proc. of the 8th ACM Symposium on Theory of Computing, STOC 1976, pp. 10–22 (1976)

    Google Scholar 

  18. Hansen, K.A., Ibsen-Jensen, R., Miltersen, P.B.: The complexity of solving reachability games using value and strategy iteration. In: Kulikov, A., Vereshchagin, N. (eds.) CSR 2011. LNCS, vol. 6651, pp. 77–90. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  19. Hoffman, A.J., Karp, R.M.: On nonterminating stochastic games. Management Sci. 12, 359–370 (1966)

    Article  MathSciNet  Google Scholar 

  20. Manning, C.D., Schütze, H.: Foundations of statistical natural language processing. MIT Press (1999)

    Google Scholar 

  21. Martin, D.A.: The Determinacy of Blackwell Games. J. Symb. Logic 63(4), 1565–1581 (1998)

    Article  MathSciNet  Google Scholar 

  22. Nerode, A., Yakhnis, A., Yakhnis, V.: Concurrent programs as strategies in games. In: Logic from Computer Science. Mathematical Sciences Research Institute Publications, vol. 21, pp. 405–479. Springer, New York (1992)

    Chapter  Google Scholar 

  23. Osborne, M.J., Rubinstein, A.: Course in game theory. MIT Press (1994)

    Google Scholar 

  24. Pliska, S.R.: Optimization of multitype branching processes. Management Science 23(2), 117–124 (1976)

    Article  MathSciNet  Google Scholar 

  25. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. of the 16th Symposium on Principles of Programming Languages, pp. 179–190. ACM (1989)

    Google Scholar 

  26. Rothblum, U.G., Whittle, P.: Growth optimality for branching Markov decision chains. Mathematics of Operations Research 7(4), 582–601 (1982)

    Article  MathSciNet  Google Scholar 

  27. Shapley, L.S.: Stochastic games. Proc. Nat. Acad. Sci. 39, 1095–1100 (1953)

    Article  MathSciNet  Google Scholar 

  28. Wojtczak, D.: Expected termination time in BPA games. Technical Report ULCS-13-005, University of Liverpool (2013), http://www.csc.liv.ac.uk/research/techreports

Download references

Author information

Authors and Affiliations

  1. University of Liverpool, UK

    Dominik Wojtczak

Authors
  1. Dominik Wojtczak
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Engineering and Technology, Vietnam National University, Xuan Thuy Street, 144, Hanoi, Vietnam

    Dang Van Hung

  2. School of Information Science, Japan Advanced Institute of Science and Technology, 1-1 Asahidai, 923-1292, Nomi, Ishikawa, Japan

    Mizuhito Ogawa

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer International Publishing Switzerland

About this paper

Cite this paper

Wojtczak, D. (2013). Expected Termination Time in BPA Games. In: Van Hung, D., Ogawa, M. (eds) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol 8172. Springer, Cham. https://doi.org/10.1007/978-3-319-02444-8_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-02444-8_22

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-02443-1

  • Online ISBN: 978-3-319-02444-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation