Stochastic Parity Games on Lossy Channel Systems

  • Parosh Aziz Abdulla
  • Lorenzo Clemente
  • Richard Mayr
  • Sven Sandberg
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8054)


We give an algorithm for solving stochastic parity games with almost-sure winning conditions on lossy channel systems, for the case where the players are restricted to finite-memory strategies. First, we describe a general framework, where we consider the class of \(2\frac{1}{2}\)-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game contains a finite attractor. An attractor is a set of states (not necessarily absorbing) that is almost surely re-visited regardless of the players’ decisions. We present a scheme that characterizes the set of winning states for each player. Then, we instantiate this scheme to obtain an algorithm for stochastic game lossy channel systems.


Player Game Regular Language Stochastic Game Winning Strategy Memory Strategy 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abdulla, P.A., Bertrand, N., Rabinovich, A., Schnoebelen, P.: Verification of probabilistic systems with faulty communication. Information and Computation 202(2), 105–228 (2005)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Abdulla, P.A., Bouajjani, A., d’Orso, J.: Deciding monotonic games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 1–14. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  3. 3.
    Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation 160, 109–127 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Abdulla, P.A., Clemente, L., Mayr, R., Sandberg, S.: Stochastic parity games on lossy channel systems. Technical Report EDI-INF-RR-1416, University of Edinburgh (2013),,
  5. 5.
    Abdulla, P.A., Henda, N.B., de Alfaro, L., Mayr, R., Sandberg, S.: Stochastic games with lossy channels. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 35–49. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. 6.
    Abdulla, P.A., Henda, N.B., Mayr, R.: Decisive Markov chains. Logical Methods in Computer Science 3 (2007)Google Scholar
  7. 7.
    Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: LICS, pp. 160–170 (1993)Google Scholar
  8. 8.
    Abdulla, P.A., Rabinovich, A.: Verification of probabilistic systems with faulty communication. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 39–53. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Baier, C., Bertrand, N., Schnoebelen, P.: Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties. ACM Trans. on Comp. Logic 9 (2007)Google Scholar
  10. 10.
    Bertr, N., Schnoebelen, P.: Model checking lossy channels systems is probably decidable. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 120–135. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    Bertrand, N., Schnoebelen, P.: Solving stochastic büchi games on infinite arenas with a finite attractor. In: Proceedings of the 11th International Workshop on Quantitative Aspects of Programming Languages (QAPl 2013), Roma, Italy (to appear March 2013)Google Scholar
  12. 12.
    Billingsley, P.: Probability and Measure, 2nd edn. Wiley, New York (1986)zbMATHGoogle Scholar
  13. 13.
    Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM 2(5), 323–342 (1983)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Chatterjee, K., de Alfaro, L., Henzinger, T.: Strategy improvement for concurrent reachability games. In: QEST, pp. 291–300. IEEE Computer Society Press (2006)Google Scholar
  15. 15.
    Chatterjee, K., Jurdziński, M., Henzinger, T.: Simple stochastic parity games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 100–113. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  16. 16.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (December 1999)Google Scholar
  17. 17.
    Condon, A.: The complexity of stochastic games. Information and Computation 96(2), 203–224 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  18. 18.
    de Alfaro, L., Henzinger, T.: Concurrent omega-regular games. In: LICS, Washington - Brussels - Tokyo, pp. 141–156. IEEE (2000)Google Scholar
  19. 19.
    de Alfaro, L., Henzinger, T., Kupferman, O.: Concurrent reachability games. In: FOCS, pp. 564–575. IEEE Computer Society Press (1998)Google Scholar
  20. 20.
    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)CrossRefGoogle Scholar
  21. 21.
    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)CrossRefGoogle Scholar
  22. 22.
    Etessami, K., Yannakakis, M.: Recursive concurrent stochastic games. LMCS 4 (2008)Google Scholar
  23. 23.
    Rabinovich, A.: Quantitative analysis of probabilistic lossy channel systems. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 1008–1021. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  24. 24.
    Shapley, L.S.: Stochastic games. Proceedings of the National Academy of Sciences 39(10), 1095–1100 (1953)MathSciNetzbMATHCrossRefGoogle Scholar
  25. 25.
    Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327–338 (1985)Google Scholar
  26. 26.
    Wang, K., Li, N., Jiang, Z.: Queueing system with impatient customers: A review. In: IEEE International Conference on Service Operations and Logistics and Informatics (SOLI), pp. 82–87. IEEE (2010)Google Scholar
  27. 27.
    Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS 200, 135–183 (1998)MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Parosh Aziz Abdulla
    • 1
  • Lorenzo Clemente
    • 2
  • Richard Mayr
    • 3
  • Sven Sandberg
    • 1
  1. 1.Uppsala UniversitySweden
  2. 2.LaBRIUniversity of Bordeaux IFrance
  3. 3.University of EdinburghUK

Personalised recommendations