{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:26:20Z","timestamp":1750843580889,"version":"3.40.3"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031223365"},{"type":"electronic","value":"9783031223372"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_19","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"388-406","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Symbolic Verification and Strategy Synthesis for Turn-Based Stochastic Games"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"given":"Gabriel","family":"Santos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,29]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Alfaro","year":"2000","unstructured":"de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 395\u2013410. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46419-0_27"},{"issue":"1","key":"19_CR2","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.: Reactive modules. Formal Methods Syst. Des. 15(1), 7\u201348 (1999)","journal-title":"Formal Methods Syst. Des."},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: modularity in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 521\u2013525. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028774"},{"issue":"5","key":"19_CR4","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-030-90870-6_9","volume-title":"Formal Methods","author":"G Amram","year":"2021","unstructured":"Amram, G., Maoz, S., Pistiner, O., Ringert, J.O.: Efficient algorithms for omega-regular energy games. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 163\u2013181. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_9"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Aslanyan, Z., Nielson, F., Parker, D.: Quantitative verification and synthesis of attack-defence scenarios. In: Proceedings of the 29th IEEE Computer Security Foundations Symposium (CSF 2016), pp. 105\u2013119. IEEE (2016)","DOI":"10.1109\/CSF.2016.15"},{"issue":"2\/3","key":"19_CR7","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"I Bahar","year":"1997","unstructured":"Bahar, I., et al.: Algebraic decision diagrams and their applications. Formal Methods Syst. Des. 10(2\/3), 171\u2013206 (1997)","journal-title":"Formal Methods Syst. Des."},{"key":"19_CR8","unstructured":"Baier, C.: On algorithmic verification methods for probabilistic systems. Habilitation thesis. Fakult\u00e4t f\u00fcr Mathematik & Informatik, Universit\u00e4t Mannheim (1998)"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/3-540-63165-8_199","volume-title":"Automata, Languages and Programming","author":"C Baier","year":"1997","unstructured":"Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 430\u2013440. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63165-8_199"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-030-53291-8_27","volume-title":"Computer Aided Verification","author":"K Batz","year":"2020","unstructured":"Batz, K., Junges, S., Kaminski, B.L., Katoen, J.-P., Matheja, C., Schr\u00f6er, P.: PrIC3: property directed reachability for MDPs. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 512\u2013538. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_27"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-319-21690-4_10","volume-title":"Computer Aided Verification","author":"T Br\u00e1zdil","year":"2015","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmel\u00edk, M., Fellner, A., K\u0159et\u00ednsk\u00fd, J.: Counterexample explanation by learning small strategies in Markov decision processes. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 158\u2013177. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_10"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C 35(8), 677\u2013691 (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"19_CR13","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, J.: Symbolic model checking: $$10^{20}$$ states and beyond. In: Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (LICS 1990), pp. 428\u2013439. IEEE Computer Society Press (1990)"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Ca\u00e1mara, J., Garlan, D., Schmerl, B., Pandey, A.: Optimal planning for architecture-based self-adaptation via model checking of stochastic games. In: Proceedings of the 30th ACM Symposium on Applied Computing (SAC 2015) (2015)","DOI":"10.1145\/2695664.2695680"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-69850-0_7","volume-title":"25 Years of Model Checking","author":"K Chatterjee","year":"2008","unstructured":"Chatterjee, K., Henzinger, T.A.: Value iteration. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 107\u2013138. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69850-0_7"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1007\/978-3-642-14295-6_57","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Radhakrishna, A.: Gist: a solver for probabilistic games. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 665\u2013669. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_57"},{"key":"19_CR17","unstructured":"Chatterjee, K., Jurdzinski, M., Henzinger, T.: Quantitative stochastic parity games. In: Munro, J.I. (ed.) Proceedings of the 15th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA 2004), pp. 121\u2013130. SIAM (2004)"},{"issue":"2","key":"19_CR18","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1016\/j.jcss.2011.05.002","volume":"78","author":"K Chatterjee","year":"2012","unstructured":"Chatterjee, K., Henzinger, T.A.: A survey of stochastic $$\\omega $$-regular games. J. Comput. Syst. Sci. 78(2), 394\u2013413 (2012)","journal-title":"J. Comput. Syst. Sci."},{"issue":"6","key":"19_CR19","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1016\/j.ic.2009.07.004","volume":"208","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., Henzingera, T.A., Piterman, N.: Strategy logic. Inf. Comput. 208(6), 677\u2013693 (2010)","journal-title":"Inf. Comput."},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-030-53291-8_21","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2020","unstructured":"Chatterjee, K., Katoen, J.-P., Weininger, M., Winkler, T.: Stochastic games with lexicographic reachability-safety objectives. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 398\u2013420. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_21"},{"issue":"1","key":"19_CR21","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10703-013-0183-7","volume":"43","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods Syst. Des. 43(1), 61\u201392 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Clarke, E., Fujita, M., McGeer, P., McMillan, K., Yang, J., Zhao, X.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. In: Proceedings of the International Workshop on Logic Synthesis (IWLS 1993), pp. 1\u201315 (1993). Also available in Formal Methods Syst. Des. 10(2\/3), 149\u2013169 (1997)","DOI":"10.1023\/A:1008647823331"},{"key":"19_CR23","unstructured":"Clarke, E., McMillan, K., Zhao, X., Fujita, M., Yang, J.: Spectral transforms for large Boolean functions with applications to technology mapping. In: Proceedings of the 30th Design Automation Conference (DAC 1993), pp. 54\u201360. ACM Press (1993). Also available in Formal Methods Syst. Des. 10(2\/3), 137\u2013148 (1997)"},{"issue":"2","key":"19_CR24","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A Condon","year":"1992","unstructured":"Condon, A.: The complexity of stochastic games. Inf. Comput. 96(2), 203\u2013224 (1992)","journal-title":"Inf. Comput."},{"issue":"2","key":"19_CR25","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1016\/j.jcss.2003.07.009","volume":"68","author":"L de Alfaro","year":"2004","unstructured":"de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374\u2013397 (2004)","journal-title":"J. Comput. Syst. Sci."},{"key":"19_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"issue":"2","key":"19_CR27","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1109\/TASE.2016.2530623","volume":"13","author":"L Feng","year":"2016","unstructured":"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\u2013462 (2016)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"key":"19_CR28","doi-asserted-by":"publisher","unstructured":"Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, New York (1997). https:\/\/doi.org\/10.1007\/978-1-4612-4054-9","DOI":"10.1007\/978-1-4612-4054-9"},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-319-99154-2_13","volume-title":"Quantitative Evaluation of Systems","author":"S Junges","year":"2018","unstructured":"Junges, S., Jansen, N., Katoen, J.-P., Topcu, U., Zhang, R., Hayhoe, M.: Model checking for safe navigation among humans. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 207\u2013222. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99154-2_13"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1007\/978-3-319-96145-3_36","volume-title":"Computer Aided Verification","author":"E Kelmendi","year":"2018","unstructured":"Kelmendi, E., Kr\u00e4mer, J., K\u0159et\u00ednsk\u00fd, J., Weininger, M.: Value iteration for simple stochastic games: stopping criterion and learning algorithm. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 623\u2013642. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_36"},{"key":"19_CR31","doi-asserted-by":"publisher","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer, New York (1976). https:\/\/doi.org\/10.1007\/978-1-4684-9455-6","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"19_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-662-49674-9_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Klein","year":"2016","unstructured":"Klein, J., et al.: Advances in symbolic probabilistic model checking with PRISM. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 349\u2013366. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_20"},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"Kret\u00ednsk\u00fd, J., Ramneantu, E., Slivinskiy, A., Weininger, M.: Comparison of algorithms for simple stochastic games. In: Proceedings of the 11th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2020), pp. 131\u2013148. EPTCS (2020)","DOI":"10.4204\/EPTCS.326.9"},{"key":"19_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: Proceedings of the 9th International Conference on Quantitative Evaluation of SysTems (QEST 2012), pp. 203\u2013204. IEEE CS Press (2012). https:\/\/www.prismmodelchecker.org\/benchmarks\/","DOI":"10.1109\/QEST.2012.14"},{"key":"19_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-030-31175-9_22","volume-title":"The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy","author":"M Kwiatkowska","year":"2019","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Verification and control of turn-based probabilistic real-time games. In: Alvim, M.S., Chatzikokolakis, K., Olarte, C., Valencia, F. (eds.) The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy. LNCS, vol. 11760, pp. 379\u2013396. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31175-9_22"},{"key":"19_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-030-59854-9_7","volume-title":"Quantitative Evaluation of Systems","author":"M Kwiatkowska","year":"2020","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Multi-player equilibria verification for concurrent stochastic games. In: Gribaudo, M., Jansen, D.N., Remke, A. (eds.) QEST 2020. LNCS, vol. 12289, pp. 74\u201395. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59854-9_7"},{"key":"19_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-030-53291-8_25","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2020","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: PRISM-games 3.0: stochastic game verification with concurrency, equilibria and time. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 475\u2013487. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_25"},{"key":"19_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-020-00356-y","volume":"58","author":"M Kwiatkowska","year":"2021","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Automatic verification of concurrent stochastic systems. Formal Methods Syst. Des. 58, 1\u201363 (2021)","journal-title":"Formal Methods Syst. Des."},{"key":"19_CR40","doi-asserted-by":"crossref","unstructured":"Littman, M., Cassandra, A., Kaelbling, L.: Learning policies for partially observable environments: scaling up. In: Proceedings of the 12th International Conference on Machine Learning (ICML 1995), pp. 362\u2013370 (1995)","DOI":"10.1016\/B978-1-55860-377-6.50052-9"},{"key":"19_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1007\/978-3-642-02658-4_55","volume-title":"Computer Aided Verification","author":"A Lomuscio","year":"2009","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: a model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682\u2013688. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_55"},{"issue":"5","key":"19_CR42","first-page":"127","volume":"54","author":"R Majumdar","year":"2021","unstructured":"Majumdar, R., Mallik, K., Schmuck, A.K., Soudjani, S.: Symbolic qualitative control for stochastic systems via finite parity games. IFAC 54(5), 127\u2013132 (2021)","journal-title":"IFAC"},{"issue":"4","key":"19_CR43","doi-asserted-by":"publisher","first-page":"1565","DOI":"10.2307\/2586667","volume":"63","author":"D Martin","year":"1998","unstructured":"Martin, D.: The determinacy of Blackwell games. J. Symb. Log. 63(4), 1565\u20131581 (1998)","journal-title":"J. Symb. Log."},{"key":"19_CR44","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Results on the quantitative mu-calculus qMu. ACM Trans. Comput. Log. 8(1), 3-es (2007)","DOI":"10.1145\/1182613.1182616"},{"key":"19_CR45","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Amsterdam (1993)"},{"key":"19_CR46","volume-title":"Theory of Games and Economic Behavior","author":"J von Neumann","year":"1944","unstructured":"von Neumann, J., Morgenstern, O., Kuhn, H., Rubinstein, A.: Theory of Games and Economic Behavior. Princeton University Press, Princeton (1944)"},{"key":"19_CR47","volume-title":"An Introduction to Game Theory","author":"M Osborne","year":"2004","unstructured":"Osborne, M., Rubinstein, A.: An Introduction to Game Theory. Oxford University Press, Oxford (2004)"},{"key":"19_CR48","unstructured":"Parker, D.: Implementation of symbolic model checking for probabilistic systems. Ph.D. thesis. University of Birmingham (2002)"},{"key":"19_CR49","doi-asserted-by":"crossref","unstructured":"Shapley, L.: Stochastic games. In: Proceedings of the National Academy of Science, vol. 39, pp. 1095\u20131100 (1953)","DOI":"10.1073\/pnas.39.10.1953"},{"key":"19_CR50","doi-asserted-by":"crossref","unstructured":"Zamani, Z., Sanner, S., Fang, C.: Symbolic dynamic programming for continuous state and action MDPs. In: Proceedings of the AAAI 2012, pp. 1839\u20131845. AAAI Press (2012)","DOI":"10.1609\/aaai.v26i1.8372"},{"key":"19_CR51","unstructured":"Supporting material. https:\/\/www.prismmodelchecker.org\/files\/pgsym\/"}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T00:09:38Z","timestamp":1672358978000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}