{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:51:17Z","timestamp":1762102277233,"version":"3.37.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319991535"},{"type":"electronic","value":"9783319991542"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99154-2_14","type":"book-chapter","created":{"date-parts":[[2018,8,14]],"date-time":"2018-08-14T14:14:35Z","timestamp":1534256075000},"page":"223-239","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Automated Verification of Concurrent 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":[[2018,8,15]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.: Concurrent omega-regular games. In: LICS 2000 (2000)","DOI":"10.1109\/LICS.2000.855763"},{"issue":"3","key":"14_CR2","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1016\/j.tcs.2007.07.008","volume":"386","author":"L Alfaro de","year":"2007","unstructured":"de Alfaro, L., Henzinger, T., Kupferman, O.: Concurrent reachability games. TCS 386(3), 188\u2013217 (2007)","journal-title":"TCS"},{"issue":"2","key":"14_CR3","first-page":"374","volume":"68","author":"L Alfaro de","year":"2004","unstructured":"de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. JCSS 68(2), 374\u2013397 (2004)","journal-title":"JCSS"},{"issue":"5","key":"14_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":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"890","DOI":"10.1007\/978-3-642-39799-8_63","volume-title":"Computer Aided Verification","author":"R Brenguier","year":"2013","unstructured":"Brenguier, R.: PRALINE: a tool for computing nash equilibria in concurrent games. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 890\u2013895. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_63"},{"issue":"5","key":"14_CR6","first-page":"640","volume":"79","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee, K., de Alfaro, L., Henzinger, T.: Strategy improvement for concurrent reachability and turn-based stochastic safety games. JCSS 79(5), 640\u2013657 (2013)","journal-title":"JCSS"},{"issue":"2","key":"14_CR7","first-page":"394","volume":"78","author":"K Chatterjee","year":"2012","unstructured":"Chatterjee, K., Henzinger, T.: A survey of stochastic $$\\omega $$-regular games. JCSS 78(2), 394\u2013413 (2012)","journal-title":"JCSS"},{"key":"14_CR8","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"},{"issue":"1","key":"14_CR9","first-page":"61","volume":"43","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. FMSD 43(1), 61\u201392 (2013)","journal-title":"FMSD"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-19835-9_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C-H Cheng","year":"2011","unstructured":"Cheng, C.-H., Knoll, A., Luttenberger, M., Buckl, C.: GAVS+: an open platform for the research of algorithmic game solving. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 258\u2013261. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_22"},{"key":"14_CR11","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"},{"key":"14_CR12","unstructured":"ILOG CPLEX. ibm.com\/products\/ilog-cplex-optimization-studio"},{"key":"14_CR13","series-title":"Graduate Texts in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains","author":"J Kemeny","year":"1976","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Graduate Texts in Mathematics, vol. 40. Springer, New York (1976). https:\/\/doi.org\/10.1007\/978-1-4684-9455-6"},{"key":"14_CR14","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":"14_CR15","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Parker, D., Simaitis, A.: Strategic analysis of trust models for user-centric networks. In: Proceedings of SR 2013. EPTCS, p. 112 (2013)","DOI":"10.4204\/EPTCS.112.10"},{"issue":"2","key":"14_CR16","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10009-017-0476-z","volume":"20","author":"M Kwiatkowska","year":"2018","unstructured":"Kwiatkowska, M., Parker, D., Wiltsche, C.: PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives. STTT 20(2), 195\u2013210 (2018)","journal-title":"STTT"},{"key":"14_CR17","unstructured":"LPSolve (version 5.5). lpsolve.sourceforge.net\/5.5\/"},{"issue":"4","key":"14_CR18","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"},{"issue":"1","key":"14_CR19","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/1182613.1182616","volume":"8","author":"A McIver","year":"2007","unstructured":"McIver, A., Morgan, C.: Results on the quantitative mu-calculus qMu. ACM Trans. Comput. Log. 8(1), 3 (2007)","journal-title":"ACM Trans. Comput. Log."},{"key":"14_CR20","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1073\/pnas.36.1.48","volume":"36","author":"J Nash","year":"1950","unstructured":"Nash, J.: Equilibrium points in $$n$$-person games. Proc. Natl. Acad. Sci 36, 48\u201349 (1950)","journal-title":"Proc. Natl. Acad. Sci"},{"key":"14_CR21","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/BF01448847","volume":"100","author":"J Neumann von","year":"1928","unstructured":"von Neumann, J.: Zur theorie der gesellschaftsspiele. Mathematische Annalen 100, 295\u2013320 (1928)","journal-title":"Mathematische Annalen"},{"key":"14_CR22","volume-title":"Theory of Games and Economic Behavior","author":"J Neumann von","year":"1944","unstructured":"von Neumann, J., Morgenstern, O., Kuhn, H., Rubinstein, A.: Theory of Games and Economic Behavior. Princeton University Press, Princeton (1944)"},{"issue":"6","key":"14_CR23","first-page":"437","volume":"35","author":"T Raghavan","year":"1991","unstructured":"Raghavan, T., Filar, J.: Algorithms for stochastic games \u2013 a survey. Zeitschrift f\u00fcr Oper. Res. 35(6), 437\u2013472 (1991)","journal-title":"Zeitschrift f\u00fcr Oper. Res."},{"key":"14_CR24","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.ejcon.2016.04.009","volume":"30","author":"M Svorenova","year":"2016","unstructured":"Svorenova, M., Kwiatkowska, M.: Quantitative verification and strategy synthesis for stochastic games. Eur. J. Control 30, 15\u201330 (2016)","journal-title":"Eur. J. Control"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/978-3-319-25150-9_34","volume-title":"Theoretical Aspects of Computing - ICTAC 2015","author":"A Toumi","year":"2015","unstructured":"Toumi, A., Gutierrez, J., Wooldridge, M.: A tool for the automated verification of nash equilibria in concurrent games. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 583\u2013594. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25150-9_34"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Zhu, Q., Ba\u015far, T.: Dynamic policy-based IDS configuration. In: CDC 2009 (2009)","DOI":"10.1109\/CDC.2009.5399894"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Zhu, Q., Li, H., Han, Z., Basar, T.: A stochastic game model for jamming in multi-channel cognitive radio systems. In: Proceedings of the ICC 2010. IEEE (2010)","DOI":"10.1109\/ICC.2010.5502451"},{"key":"14_CR28","unstructured":"Supporting material. www.prismmodelchecker.org\/files\/qest18\/"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99154-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,22]],"date-time":"2019-10-22T05:07:05Z","timestamp":1571720825000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99154-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319991535","9783319991542"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99154-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}