×

zbMATH — the first resource for mathematics

Quantitative verification and strategy synthesis for stochastic games. (English) Zbl 1347.93240
Summary: Design and control of computer systems that operate in uncertain, competitive or adversarial, environments can be facilitated by formal modeling and analysis. In this paper, we focus on analysis of complex computer systems modelled as turn-based \(2\frac{1}{2}\)-player games, or stochastic games for short, that are able to express both stochastic and non-stochastic uncertainties. We offer a systematic overview of the body of knowledge and algorithmic techniques for verification and strategy synthesis for stochastic games with respect to a broad class of quantitative properties expressible in temporal logic. These include probabilistic linear-time properties, expected total, discounted and average reward properties, and their branching-time extensions and multi-objective combinations. To demonstrate applicability of the framework as well as its practical implementation in a tool called PRISM-games, we describe several case studies that rely on analysis of stochastic games, from areas such as robotics, and networked and distributed systems.

MSC:
93E03 Stochastic systems in control theory (general)
91A15 Stochastic games, stochastic differential games
93B50 Synthesis problems
90C29 Multi-objective and goal programming
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] R. Alur, T. Henzinger, F. Mang, S. Qadeer, S. Rajamani, S. Tasiran, MOCHA: modularity in model checking, in: Proceedings of Computer Aided Verification CAV, 1998, pp. 521-525.
[2] D. Andersson, P.B. Miltersen, The complexity of solving stochastic games on graphs, in: Algorithms and Computation, Series, Lecture Notes in Computer Science, vol. 5878, 2009, pp. 112-121. · Zbl 1272.91025
[3] Ash, R.; Doléans-Dade, C., Probability and measure theory, (2000), Harcourt, Academic Press Burlington, MA, USA · Zbl 0944.60004
[4] Z. Aslanyan, F. Nielson, D. Parker, Quantitative Verification and Synthesis of Attack-Defence Scenarios, in: Proceedings of Computer Security Foundations Symposium CSF, 2016, In press.
[5] Bagnara, R.; Hill, P. M.; Zaffanella, E., The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Sci. Comput. Program., 72, 1-2, 3-21, (2008)
[6] N. Basset, M.Z. Kwiatkowska, U. Topcu, C. Wiltsche, Strategy synthesis for stochastic games with multiple long-run objectives, in: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS, 2015, pp. 256-271.
[7] N. Basset, M.Z. Kwiatkowska, C. Wiltsche, Compositional controller synthesis for stochastic games, in: Proceedings of Concurrency Theory CONCUR, 2014, pp. 173-187. · Zbl 1421.93053
[8] A. Bianco, L. de Alfaro, Model checking of probabilistic and nondeterministic systems, in: Proceedings of Foundations of Software Technology and Theoretical Computer Science FSTTCS, Series, Lecture Notes in Computer Science, vol. 1026, 1995, pp. 499-513. · Zbl 1354.68167
[9] U. Boker, O. Kupferman, A. Steinitz, Parityizing Rabin and Streett, in: Proceedings of Foundations of Software Technology and Theoretical Computer Science FSTTCS, 2010, pp. 412-423. · Zbl 1245.68120
[10] E. Boros, K.M. Elbassioni, V. Gurvich, K. Makino, A pumping algorithm for ergodic stochastic mean payoff games with perfect information, in: Proceedings of Integer Programming and Combinatorial Optimization IPCO, 2010, pp. 341-354. · Zbl 1285.91014
[11] P. Bouyer, V. Forejt, Reachability in stochastic timed games, in: Proceedings of International Colloquium on Automata, Languages and Programming ICALP, Series, Lecture Notes in Computer Science, 2009, pp. 103-114. · Zbl 1248.91014
[12] H. Björklund, S. Sandberg, and S. Vorobyov, On Combinatorial Structure and Algorithms for Parity Games, Department of Information Technology, Uppsala University, Technical Report 2003-002, 2003.
[13] F. Blahoudek, M. Křetínský, J. Strejček, Comparison of LTL to deterministic Rabin automata translators, in: Proceedings of Logic for Programming, Artificial Intelligence, and Reasoning LPAR, Series, Lecture Notes in Computer Science, vol. 8312, 2013, pp. 164-172. · Zbl 1406.68050
[14] Brázdil, T.; Forejt, V.; Krčál, J.; Křetínský, J.; Kučera, A., Continuous-time stochastic games with time-bounded reachability, Inf. Comput., 224, 46-70, (2013) · Zbl 1264.91016
[15] T. Brázdil, K. Chatterjee, V. Forejt, A. Kucera, MultiGain: a controller synthesis tool for mdps with multiple mean-payoff objectives, in: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS, 2015, pp. 181-187.
[16] T. Brázdil, V. Brozek, V. Forejt, A. Kucera, Stochastic games with branching-time winning objectives, in: Proceedings of Logic in Computer Science LICS, 2006, pp. 349-358.
[17] R. Brenguier, PRALINE: a tool for computing Nash equilibria in concurrent games, in: Proceedings of Computer Aided Verification CAV, Series, Lecture Notes in Computer Science, vol. 8044, 2013, pp. 890-895.
[18] Brown, G.; Carlyle, M.; Salmerón, J.; Wood, K., Defending critical infrastructure, Interfaces, 36, 6, 530-544, (2006)
[19] J. Cámara, G.A. Moreno, D. Garlan, Stochastic game analysis and latency awareness for proactive self-adaptation, in: Proceedings of Software Engineering for Adaptive and Self-Managing Systems SEAMS, 2014, pp. 155-164.
[20] Chatterjee, K.; Doyen, L., Partial-observation stochastic gameshow to win when belief fails, Trans. Comput. Logic, 15, 2, 16, (2014) · Zbl 1291.91021
[21] Chatterjee, K.; Doyen, L.; Henzinger, T. A., A survey of partial-observation stochastic parity games, Formal Methods Syst. Des., 43, 2, 268-284, (2013) · Zbl 1291.91022
[22] Chatterjee, K.; Henzinger, T. A., A survey of stochastic ømega-regular games, J. Comput. Syst. Sci., 78, 2, 394-413, (2012) · Zbl 1237.91036
[23] K. Chatterjee, M. Jurdzinski, T.A. Henzinger, Quantitative stochastic parity games, in: Proceedings of Symposium on Discrete Algorithms SODA, 2004, pp. 121-130. · Zbl 1318.91027
[24] K. Chatterjee, L. Doyen, S. Nain, M.Y. Vardi, The complexity of partial-observation stochastic parity games with finite-memory strategies, in: Proceedings of Foundations of Software Science and Computation Structures FOSSACS, 2014, pp. 242-257. · Zbl 1405.68135
[25] K. Chatterjee, T.A. Henzinger, Value iteration, in: 25 Years of Model Checking—History, Achievements, Perspectives, 2008, pp. 107-138. · Zbl 1143.68042
[26] K. Chatterjee, L. de Alfaro, T. A. Henzinger, The complexity of stochastic Rabin and Streett games, in: Proceedings of International Colloquium on Automata, Languages and Programming ICALP, 2005, pp. 878-890. · Zbl 1085.68060
[27] K. Chatterjee, T.A. Henzinger, Strategy Improvement for Stochastic Rabin and Streett Games, in: Proceedings of Concurrency Theory CONCUR, 2006, pp. 375-389. · Zbl 1151.68474
[28] K. Chatterjee, T.A. Henzinger, Strategy improvement and randomized subexponential algorithms for stochastic parity games, in: Proceedings of Symposium on Theoretical Aspects of Computer Science STACS, 2006, pp. 512-523. · Zbl 1136.91322
[29] K. Chatterjee, V. Forejt, D. Wojtczak, Multi-objective discounted reward verification in graphs and MDPs, in: Proceedings of Logic for Programming, Artificial Intelligence, and Reasoning LPAR, Series, Lecture Notes in Computer Science, vol. 8312, 2013, pp. 228-242. · Zbl 1406.68051
[30] K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, QUASY: quantitative synthesis tool, in: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS, 2011, pp. 267-271. · Zbl 1316.68071
[31] K. Chatterjee, T. Henzinger, B. Jobstmann, A. Radhakrishna, Gist: a solver for probabilistic games, in: Proceedings of Computer Aided Verification CAV, Series, Lecture Notes in Computer Science, vol. 6174, 2010, pp. 665-669.
[32] T. Chen, V. Forejt, M.Z. Kwiatkowska, A. Simaitis, C. Wiltsche, On stochastic games with multiple objectives, in: Proceedings of Mathematical Foundations of Computer Science MFCS, 2013, pp. 266-277. · Zbl 1400.91040
[33] T. Chen, M.Z. Kwiatkowska, A. Simaitis, C. Wiltsche, Synthesis for multi-objective stochastic games: an application to autonomous urban driving, in: Proceedings of Quantitative Evaluation of Systems QEST, 2013, pp. 322-337.
[34] T. Chen, V. Forejt, M. Kwiatkowska, A. Simaitis, A. Trivedi, M. Ummels, Playing stochastic games precisely, in: Proceedings of Concurrency Theory CONCUR, Series, Lecture Notes in Computer Science, vol. 7454, 2012, pp. 348-363. · Zbl 1364.91024
[35] T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, A. Simaitis, Automatic verification of competitive stochastic systems, in: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS, Series, Lecture Notes in Computer Science, vol. 7214, 2012, pp. 315-330. · Zbl 1352.68150
[36] T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, A. Simaitis, PRISM-games: a model checker for stochastic multi-player games, in: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS, Series, Lecture Notes in Computer Science, vol. 7795, 2013, pp. 185-191. · Zbl 1381.68151
[37] C. Cheng, A. Knoll, M. Luttenberger, C. Buckl, GAVS+: an open platform for the research of algorithmic game solving, in: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS, 2011, pp. 258-261.
[38] J. Cámara, D. Garlan, B. Schmerl, A. Pandey, Optimal planning for architecture-based self-adaptation via model checking of stochastic games, in: Proceedings of Symposium on Applied Computing SAC, 2015, pp. 428-435.
[39] J. Cámara, G.A. Moreno, D. Garlan, Reasoning about human participation in self-adaptive systems, in: Proceedings of Software Engineering for Adaptive and Self-Managing Systems SEAMS, 2015, pp. 146-156.
[40] Condon, A., The complexity of stochastic games, Inf. Comput., 96, 203-224, (1992) · Zbl 0756.90103
[41] Condon, A., On algorithms for simple stochastic games, Adv. Comput. Complex. Theory, 13, 51-73, (1993) · Zbl 0808.90141
[42] A. David, P. Jensen, K. Larsen, M. Mikuionis, J. Taankvist, Uppaal Stratego, in: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS, Series, Lecture Notes in Computer Science, vol. 9035, 2015, pp. 206-211.
[43] T. Deshpande, P. Katsaros, S. Smolka, S. Stoller, Stochastic game-based analysis of the dns bandwidth amplification attack using probabilistic model checking, in: Proceedings of European Dependable Computing Conference EDCC, 2014, pp. 226-237.
[44] C. Essen, D. Giannakopoulou, Analyzing the Next Generation Airborne Collision Avoidance System, in: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS, 2014, pp. 620-635.
[45] K. Etessami, M. Yannakakis, Recursive Concurrent Stochastic Games, CoRR, vol. abs/0810.3581, 2008. · Zbl 1161.68619
[46] L. Feng, C. Wiltsche, L. Humphrey, U. Topcu, Controller synthesis for autonomous systems interacting with human operators, in: Proceedings of International Conference on Cyber-Physical Systems ICCPS, 2015, pp. 70-79.
[47] Filar, J.; Vrieze, K., Competitive Markov decision processes, (1996), Springer-Verlag New York Inc. New York, NY, USA
[48] V. Forejt, M. Kwiatkowska, G. Norman, D. Parker, Automated verification techniques for probabilistic systems, in: Proceedings of Formal Methods for Eternal Networked Software System SFM, Series, Lecture Notes in Computer Science, vol. 6659, 2011, pp. 53-113. · Zbl 1315.68177
[49] V. Forejt, M. Kwiatkowska, G. Norman, A. Trivedi, Expected reachability-time games, in: Proceedings of Formal Modelling and Analysis of Timed Systems FORMATS, Series, Lecture Notes in Computer Science, 2010, pp. 122-136. · Zbl 1290.68073
[50] D. Gillette, Stochastic games with zero stop probabilities, in: Contributions to the Theory of Games, vol. 39, 1957, pp. 179-187. · Zbl 0078.33001
[51] T. Glazier, J. Camara, B. Schmerl, D. Garlan, Analyzing resilience properties of different topologies of collective adaptive systems, in: Proceedings of Self-Adaptive and Self-Organizing Systems Workshops SASOW, 2015, pp. 55-60.
[52] [Online]. Available: 〈http://www.prismmodelchecker.org/files/ecc16/〉
[53] Kwiatkowska, M.; Norman, G.; Parker, D.; Qu, H., Compositional probabilistic verification through multi-objective model checking, Inf. Comput., 232, 38-65, (2013) · Zbl 1277.68138
[54] M. Kwiatkowska, D. Parker, Automated verification and strategy synthesis for probabilistic systems, in: Proceedings of Automated Technology for Verification and Analysis ATVA, Series, Lecture Notes in Computer Science, vol. 8172, 2013, pp. 5-22. · Zbl 1410.68233
[55] M. Kwiatkowska, D. Parker, C. Wiltsche, PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games, in: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS, 2016, In press.
[56] M. Kwiatkowska, G. Norman, D. Parker, PRISM 4.0: Verification of Probabilistic Real-time Systems, in: Proceedings of Computer Aided Verification CAV, Series, Lecture Notes in Computer Science, vol. 6806, 2011, pp. 585-591.
[57] Lahijanian, M.; Andersson, S. B.; Belta, C., Formal verification and synthesis for discrete-time stochastic systems, Trans. Autom. Control, 60, 8, 2031-2045, (2015) · Zbl 1360.93650
[58] Liggett, T. M.; Lippman, S. A., Stochastic games with perfect information and time average payoff, SIAM Rev., 11, 4, 604-607, (1969) · Zbl 0193.19602
[59] Ludwig, W., A subexponential randomized algorithm for the simple stochastic game problem, Inf. Comput., 117, 1, 151-155, (1995) · Zbl 0827.90141
[60] Martin, D. A., The determinacy of blackwell games, J. Symbol. Logic, 63, 4, 1565-1581, (1998) · Zbl 0926.03071
[61] A. Neyman, S. Sorin, NATO SA Division, Stochastic Games and Applications, Series, NATO Science Series: Mathematical and Physical Sciences. Springer, Netherlands, 2003.
[62] Nilim, A.; El Ghaoui, L., Robust control of Markov decision processes with uncertain transition matrices, Oper. Res., 53, 5, 780-798, (2005) · Zbl 1165.90674
[63] Papadimitriou, C.; Tsitsiklis, J. N., The complexity of Markov decision processes, Math. Oper. Res., 12, 3, 441-450, (1987) · Zbl 0638.90099
[64] A. Pnueli, The temporal logic of programs, in: Proceedings of Foundations of Computer Science, 1977, pp. 46-57.
[65] PRISM-games Website. [Online]. Available: 〈http://www.prismmodelchecker.org/games/〉
[66] PRISM and PRISM-Games Case Studies. [Online]. Available: 〈http://www.prismmodelchecker.org/casestudies/〉
[67] A. Puggelli, W. Li, A.L. Sangiovanni-Vincentelli, S.A. Seshia, Polynomial-time verification of PCTL properties of MDPs with convex uncertainties, in: Proceedings of Computer Aided Verification CAV, 2013, pp. 527-542.
[68] Rabe, M. N.; Schewe, S., Optimal time-abstract schedulers for CTMDPs and continuous-time Markov games, Theoret. Comput. Sci., 467, 53-67, (2013) · Zbl 1261.90087
[69] Rabin, M. O., Probabilistic automata, Inf. Control, 6, 3, 230-245, (1963) · Zbl 0182.33602
[70] D. Rosenberg, E. Solan, N. Vieille, Stochastic games with imperfect monitoring, in: Advances in Dynamic Games, Series, Annals of the International Society of Dynamic Games, vol. 8, 2006, pp. 3-22. · Zbl 1218.91019
[71] L.S. Shapley, Stochastic games, in: National Academy of Sciences, 1953, pp. 1095-1100. · Zbl 0051.35805
[72] E. Shieh, B. An, R. Yang, M. Tambe, C. Baldwin, J. DiRenzo, B. Maule, G. Meyer, PROTECT: a deployed game theoretic system to protect the ports of the United States, in: Proceedings of Conference on Autonomous Agents and Multiagent Systems AAMAS, 2012, pp. 13-20.
[73] A. Simaitis, Automatic verification of competitive stochastic systems (Ph.D. dissertation), Department of Computer Science, University of Oxford, 2014.
[74] Thompson, K., Retrograde analysis of certain endgames, Int. Comput. Chess Assoc., 9, 3, 131-139, (1986)
[75] A. Toumi, J. Gutierrez, M. Wooldridge, A tool for the automated verification of nash equilibria in concurrent games, in: Proceedings of International Conference on Theoretical Aspects of Computing ICTAC, Series, Lecture Notes in Computer Science, vol. 9399, 2015, pp. 583-594. · Zbl 06545749
[76] M. Ummels, Stochastic multiplayer games: theory and algorithms (Ph.D. dissertation), RWTH Aachen University, 2010.
[77] Ummels, M.; Wojtczak, D., The complexity of Nash equilibria in stochastic multiplayer games, Log. Methods Comput. Sci., 7, 3, (2011) · Zbl 1238.91025
[78] C. Wiltsche, Assume-guarantee strategy synthesis for stochastic games (Ph.D. dissertation), Department of Computer Science, University of Oxford, 2015.
[79] T. Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, R.M. Murray, TuLiP: a software toolbox for receding horizon temporal logic planning, in: Proceedings of Conference on Hybrid Systems: Computation and Control HSCC, 2011, pp. 313-314.
[80] E.M. Wolff, U. Topcu, R.M. Murray, Robust control of uncertain Markov decision processes with temporal logic specifications, in: Proceedings of Conference on Decision and Control CDC, 2012, pp. 3372-3379.
[81] T. Wongpiromsarn, E. Frazzoli, Control of probabilistic systems under dynamic, partially known environments with temporal logic specifications, in: Proceedings of Conference on Decision and Control CDC, 2012, pp. 7644-7651.
[82] Yin, Z.; Jiang, A. X.; Tambe, M.; Kiekintveld, C.; Leyton-Brown, K.; Sandholm, T.; Sullivan, J. P., Trustsscheduling randomized patrols for fare inspection in transit systems using game theory, AI Mag., 33, 4, 59-72, (2012)
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.