Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P.A., Bertrand, N., Rabinovich, A., Schnoebelen, P.: Verification of probabilistic systems with faulty communication. Information and Computation 202(2), 105–228 (2005)
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)
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)
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), http://arxiv.org/abs/1305.5228 , http://www.inf.ed.ac.uk/publications/report/1416.html
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)
Abdulla, P.A., Henda, N.B., Mayr, R.: Decisive Markov chains. Logical Methods in Computer Science 3 (2007)
Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: LICS, pp. 160–170 (1993)
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)
Baier, C., Bertrand, N., Schnoebelen, P.: Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties. ACM Trans. on Comp. Logic 9 (2007)
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)
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)
Billingsley, P.: Probability and Measure, 2nd edn. Wiley, New York (1986)
Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM 2(5), 323–342 (1983)
Chatterjee, K., de Alfaro, L., Henzinger, T.: Strategy improvement for concurrent reachability games. In: QEST, pp. 291–300. IEEE Computer Society Press (2006)
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)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (December 1999)
Condon, A.: The complexity of stochastic games. Information and Computation 96(2), 203–224 (1992)
de Alfaro, L., Henzinger, T.: Concurrent omega-regular games. In: LICS, Washington - Brussels - Tokyo, pp. 141–156. IEEE (2000)
de Alfaro, L., Henzinger, T., Kupferman, O.: Concurrent reachability games. In: FOCS, pp. 564–575. IEEE Computer Society Press (1998)
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)
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)
Etessami, K., Yannakakis, M.: Recursive concurrent stochastic games. LMCS 4 (2008)
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)
Shapley, L.S.: Stochastic games. Proceedings of the National Academy of Sciences 39(10), 1095–1100 (1953)
Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327–338 (1985)
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)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS 200, 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abdulla, P.A., Clemente, L., Mayr, R., Sandberg, S. (2013). Stochastic Parity Games on Lossy Channel Systems. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds) Quantitative Evaluation of Systems. QEST 2013. Lecture Notes in Computer Science, vol 8054. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40196-1_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-40196-1_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40195-4
Online ISBN: 978-3-642-40196-1
eBook Packages: Computer ScienceComputer Science (R0)