×

zbMATH — the first resource for mathematics

Compositional strategy synthesis for stochastic games with multiple objectives. (English) Zbl 1395.68265
Summary: Design of autonomous systems is facilitated by automatic synthesis of controllers from formal models and specifications. We focus on stochastic games, which can model interaction with an adverse environment, as well as probabilistic behaviour arising from uncertainties. Our contribution is twofold. First, we study long-run specifications expressed as quantitative multi-dimensional mean-payoff and ratio objectives. We then develop an algorithm to synthesise \(\varepsilon\)-optimal strategies for conjunctions of almost sure satisfaction for mean payoffs and ratio rewards (in general games) and Boolean combinations of expected mean-payoffs (in controllable multi-chain games). Second, we propose a compositional framework, together with assume-guarantee rules, which enables winning strategies synthesised for individual components to be composed to a winning strategy for the composed game. The framework applies to a broad class of properties, which also include expected total rewards, and has been implemented in the software tool PRISM-games.

MSC:
68T40 Artificial intelligence for robotics
68Q60 Specification and verification (program logics, model checking, etc.)
91A15 Stochastic games, stochastic differential games
Software:
MCGP; PRISM-games
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baier, C.; Dubslaff, C.; Klüppelholz, S.; Leuschner, L., Energy-utility analysis for resilient systems using probabilistic model checking, (Petri Nets, (2014), Springer), 20-39 · Zbl 1407.68280
[2] Baier, C.; Größer, M.; Ciesinski, F., Quantitative analysis under fairness constraints, (ATVA, LNCS, vol. 5799, (2009), Springer), 135-150 · Zbl 1262.68102
[3] Baier, C.; Größer, M.; Leucker, M.; Bollig, B.; Ciesinski, F., Controller synthesis for probabilistic systems (extended abstract), IFIP TCS, vol. 155, 493-506, (2004), Springer · Zbl 1073.93037
[4] Basset, N.; Kwiatkowska, M.; Topcu, U.; Wiltsche, C., Strategy synthesis for stochastic games with multiple long-run objectives, (TACAS, LNCS, vol. 9035, (2015), Springer), 256-271
[5] Basset, N.; Kwiatkowska, M.; Wiltsche, C., Compositional controller synthesis for stochastic games, (CONCUR, LNCS, vol. 8704, (2014), Springer), 173-187 · Zbl 1421.93053
[6] Brázdil, T.; Brožek, V.; Chatterjee, K.; Forejt, V.; Kučera, A., Two views on multiple mean-payoff objectives in Markov decision processes, Log. Methods Comput. Sci., 10, 4, (2014)
[7] Brázdil, T.; Brožek, V.; Forejt, V.; Kučera, A., Stochastic games with branching-time winning objectives, (LICS, (2006), ACM/IEEE), 349-358
[8] Brázdil, T.; Jančar, P.; Kučera, A., Reachability games on extended vector addition systems with states, (ICALP, LNCS, vol. 6199, (2010), Springer), 478-489 · Zbl 1288.68179
[9] Brenguier, R.; Raskin, J. F., Optimal values of multidimensional mean-payoff games, (2014), Université Libre de Bruxelles (U.L.B.) Belgium, Research report
[10] Bruyère, Véronique; Filiot, Emmanuel; Randour, Mickael; Raskin, Jean-François, Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games, (Mayr, Ernst W.; Portier, Natacha, 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), STACS 2014, Lyon, France, March 5-8, 2014, LIPIcs, vol. 25, (2014), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik), 199-213 · Zbl 1360.91042
[11] Chatterjee, K.; Doyen, L.; Henzinger, T. A.; Raskin, J. F., Generalized mean-payoff and energy games, (FSTTCS, LIPIcs, vol. 8, (2010), Schloss Dagstuhl), 505-516 · Zbl 1245.68090
[12] Chatterjee, K.; Henzinger, M., Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification, (SODA, (2011), ACM-SIAM), 1318-1336 · Zbl 1374.68272
[13] Chatterjee, K.; Henzinger, T. A., Assume-guarantee synthesis, (TACAS, LNCS, vol. 4424, (2007), Springer), 261-275 · Zbl 1186.68284
[14] Chatterjee, K.; Komárková, Z.; Křetínský, J., Unifying two views on multiple mean-payoff objectives in Markov decision processes, (LICS, (2015), ACM/IEEE), 244-256 · Zbl 1401.68171
[15] Chatterjee, K.; Majumdar, R.; Henzinger, T. A., Markov decision processes with multiple objectives, (STACS, LNCS, vol. 3884, (2006), Springer), 325-336 · Zbl 1136.90498
[16] Chatterjee, K.; Randour, M.; Raskin, J. F., Strategy synthesis for multi-dimensional quantitative objectives, Acta Inform., 51, 3-4, 129-163, (2014) · Zbl 1360.68208
[17] Chatterjee, Krishnendu; Doyen, Laurent, Perfect-information stochastic games with generalized mean-payoff objectives, (Grohe, Martin; Koskinen, Eric; Shankar, Natarajan, Proc. LICS ’16, (2016), ACM), 247-256 · Zbl 1401.68238
[18] Chen, T.; Forejt, V.; Kwiatkowska, M.; Parker, D.; Simaitis, A., PRISM-games: a model checker for stochastic multi-player games, (TACAS, LNCS, vol. 7795, (2013), Springer), 185-191 · Zbl 1381.68151
[19] Chen, T.; Forejt, V.; Kwiatkowska, M.; Simaitis, A.; Trivedi, A.; Ummels, M., Playing stochastic games precisely, (CONCUR, LNCS, vol. 7454, (2012)), 348-363 · Zbl 1364.91024
[20] Chen, T.; Forejt, V.; Kwiatkowska, M.; Simaitis, A.; Wiltsche, C., On stochastic games with multiple objectives, (MFCS, LNCS, vol. 8087, (2013), Springer), 266-277 · Zbl 1400.91040
[21] Chen, T.; Kwiatkowska, M.; Simaitis, A.; Wiltsche, C., Synthesis for multi-objective stochastic games: an application to autonomous urban driving, (QEST, LNCS, vol. 8054, (2013), Springer), 322-337
[22] Cheung, L.; Lynch, N.; Segala, R.; Vaandrager, F., Switched PIOA: parallel composition via distributed scheduling, Theor. Comput. Sci., 365, 1-2, 83-108, (2006) · Zbl 1118.68038
[23] Davey, B. A.; Priestley, H. A., Introduction to lattices and order, (1990), Cambridge University Press · Zbl 0701.06001
[24] De Alfaro, L., Formal verification of probabilistic systems, (1997), Stanford University, PhD thesis
[25] de Alfaro, L.; Henzinger, T. A., Interface automata, SIGSOFT Softw. Eng. Notes, 26, 5, 109-120, (2001)
[26] de Alfaro, L.; Henzinger, T. A.; Jhala, R., Compositional methods for probabilistic systems, (CONCUR, LNCS, vol. 2154, (2001), Springer), 351-365 · Zbl 1006.68083
[27] Ehrenfeucht, A.; Mycielski, J., Positional strategies for mean payoff games, Int. J. Game Theory, 8, 2, 109-113, (1979) · Zbl 0499.90098
[28] Etessami, K.; Kwiatkowska, M.; Vardi, M. Y.; Yannakakis, M., Multi-objective model checking of Markov decision processes, Log. Methods Comput. Sci., 4, 8, 1-21, (2008) · Zbl 1161.68565
[29] Feng, L.; Wiltsche, C.; Humphrey, L.; Topcu, U., Synthesis of human-in-the-loop control protocols for autonomous systems, IEEE Trans. Autom. Sci. Eng., 13, 2, 450-462, (April 2016)
[30] Filar, J.; Vrieze, K., Competitive Markov decision processes, (1996), Springer
[31] Forejt, V.; Kwiatkowska, M.; Parker, D., Pareto curves for probabilistic model checking, (ATVA, LNCS, vol. 7561, (2012), Springer), 317-332 · Zbl 1374.68285
[32] Gelderie, M., Strategy composition in compositional games, (ICALP, LNCS, vol. 7966, (2013), Springer), 263-274 · Zbl 1335.68120
[33] Ghosh, S.; Ramanujam, R.; Simon, S., Playing extensive form games in parallel, (CLIMA, LNCS, vol. 6245, (2010), Springer), 153-170 · Zbl 1286.68413
[34] Gimbert, H.; Horn, F., Solving simple stochastic tail games, (SODA, (2010), ACM-SIAM), 847-862 · Zbl 1288.91020
[35] Gimbert, H.; Kelmendi, E., Two-player perfect-information shift-invariant submixing stochastic games are half-positional, (2014), arXiv preprint
[36] Horn, F., Random games, (2008), Université Denis Diderot-Paris 7 & Rheinisch-Westfälische Technische Hochschule Aachen, PhD thesis
[37] Katz, G.; Peled, D.; Schewe, S., Synthesis of distributed control through knowledge accumulation, (CAV, LNCS, vol. 6806, (2011), Springer), 510-525
[38] Kwiatkowska, M., Model checking and strategy synthesis for stochastic games: from theory to practice, (Proc. 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, (2016), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik), 4:1-4:18 · Zbl 1388.68186
[39] 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
[40] Kwiatkowska, M.; Parker, D., Automated verification and strategy synthesis for probabilistic systems, (ATVA, LNCS, vol. 8172, (2013), Springer), 5-22 · Zbl 1410.68233
[41] Kwiatkowska, M.; Parker, D.; Wiltsche, C., PRISM-games 2.0: a tool for multi-objective strategy synthesis for stochastic games, (Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’16), LNCS, vol. 9636, (2016), Springer), 560-566
[42] Levin, D. A.; Peres, Y.; Wilmer, E. L., Markov chains and mixing times, (2009), AMS
[43] MacDermed, L.; Isbell, C. L., Solving stochastic games, (NIPS, (2009), Curran Associates, Inc.), 1186-1194
[44] Madhusudan, P.; Thiagarajan, P. S., A decidable class of asynchronous distributed controllers, (CONCUR, LNCS, vol. 7454, (2002), Springer), 145-160 · Zbl 1012.68118
[45] Mohalik, S.; Walukiewicz, I., Distributed games, (FSTTCS, LNCS, vol. 2914, (2003), Springer), 338-351 · Zbl 1205.68089
[46] Pneuli, A.; Rosner, R., Distributed reactive systems are hard to synthesize, (FOCS, (1990), IEEE), 746-757
[47] Puterman, M. L., Markov decision processes: discrete stochastic dynamic programming, (2009), Wiley-Interscience
[48] Rabin, Michael O., Probabilistic automata, Inf. Control, 6, 3, 230-245, (1963) · Zbl 0182.33602
[49] Randour, M.; Raskin, J. F.; Sankur, O., Variations on the stochastic shortest path problem, (VMCAI, LNCS, vol. 8318, (2014), Springer), 1-18 · Zbl 1432.90155
[50] Randour, M.; Raskin, J. F.; Sankur, O., Percentile queries in multi-dimensional Markov decision processes, (CAV, LNCS, vol. 9206, (2015), Springer), 123-139 · Zbl 1381.68219
[51] Rockafellar, R. T., Convex analysis, (1997), Princeton University Press · Zbl 0932.90001
[52] Ross, S. M., Stochastic processes, vol. 2, (1996), John Wiley & Sons New York
[53] Sankur, O., Robustness in timed automata: analysis, synthesis, implementation, (2013), LSV, ENS Cachan France, Thèse de doctorat
[54] Segala, R., Modelling and verification of randomized distributed real time systems, (1995), Massachusetts Institute of Technology, PhD thesis
[55] Shapley, Lloyd S., Stochastic games, Proc. Natl. Acad. Sci. USA, 39, 10, 1095, (1953) · Zbl 0051.35805
[56] Shimkin, N.; Shwartz, A., Guaranteed performance regions in Markovian systems with competing decision makers, Autom. Control, 38, 1, 84-95, (1993) · Zbl 0779.90080
[57] Simaitis, A., Automatic verification of competitive stochastic systems, (2013), University of Oxford, PhD thesis · Zbl 1291.68252
[58] Sokolova, A.; de Vink, E. P., Probabilistic automata: system types, parallel composition and comparison, (VOSS, LNCS, vol. 2925, (2004), Springer), 1-43 · Zbl 1203.68089
[59] Svorenová, Mária; Kwiatkowska, Marta, Quantitative verification and strategy synthesis for stochastic games, Eur. J. Control, 30, 15-30, (2016), 15th European Control Conference, ECC16 · Zbl 1347.93240
[60] Velner, Y., Finite-memory strategy synthesis for robust multidimensional mean-payoff objectives, (LICS, (2014), ACM/IEEE), 79:1-79:10 · Zbl 1401.91035
[61] Velner, Yaron; Chatterjee, Krishnendu; Doyen, Laurent; Henzinger, Thomas A.; Rabinovich, Alexander Moshe; Raskin, Jean-François, The complexity of multi-mean-payoff and multi-energy games, Inf. Comput., 241, 177-196, (2015) · Zbl 1309.68082
[62] von Essen, C.; Jobstmann, B., Synthesizing efficient controllers, (VMCAI, LNCS, vol. 7148, (2012), Springer), 428-444 · Zbl 1326.68190
[63] White, D. J., Multi-objective infinite-horizon discounted Markov decision processes, J. Math. Anal. Appl., 89, 2, 639-647, (1982) · Zbl 0496.90083
[64] Wiltsche, C., Assume-guarantee strategy synthesis for stochastic games, (2016), University of Oxford, PhD thesis
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.