{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T13:51:19Z","timestamp":1750859479791},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496732"},{"type":"electronic","value":"9783662496749"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","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":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_35","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"560-566","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"given":"Clemens","family":"Wiltsche","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"issue":"1\u20132","key":"35_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P., Zaffanella, E.: The parma polyhedra library. Sci. Comput. Program. 72(1\u20132), 3\u201321 (2008)","journal-title":"Sci. Comput. Program."},{"key":"35_CR2","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/978-3-662-46681-0_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Nicolas Basset","year":"2015","unstructured":"Basset, N., Kwiatkowska, M., Topcu, U., Wiltsche, C.: Strategy synthesis for stochastic games with multiple long-run objectives. In: TACAS 2015, pp. 256\u2013271 (2015)"},{"key":"35_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-3-662-44584-6_13","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"N Basset","year":"2014","unstructured":"Basset, N., Kwiatkowska, M., Wiltsche, C.: Compositional controller synthesis for stochastic games. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 173\u2013187. Springer, Heidelberg (2014)"},{"key":"35_CR4","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Forejt, V., Ku\u010dera, A.: MultiGain: a controller synthesis tool for MDPs with multiple mean-payoff objectives. In: TACAS 2015","DOI":"10.1007\/978-3-662-46681-0_12"},{"key":"35_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)"},{"key":"35_CR6","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)"},{"issue":"1","key":"35_CR7","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":"35_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-40313-2_25","volume-title":"Mathematical Foundations of Computer Science 2013","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: On stochastic games with multiple objectives. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 266\u2013277. Springer, Heidelberg (2013)"},{"key":"35_CR9","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/978-3-642-40196-1_28","volume-title":"Quantitative Evaluation of Systems","author":"Taolue Chen","year":"2013","unstructured":"Chen, T., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: Synthesis for multi-objective stochastic games: an application to autonomous urban driving. In: QEST 2013 (2013)"},{"key":"35_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)"},{"key":"35_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/978-3-662-46681-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A David","year":"2015","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Miku\u010dionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206\u2013211. Springer, Heidelberg (2015)"},{"key":"35_CR12","doi-asserted-by":"crossref","unstructured":"Feng, L., Wiltsche, C., Humphrey, L., Topcu, U.: Controller synthesis for autonomous systems interacting with human operators. In: ICCPS (2015)","DOI":"10.1145\/2735960.2735973"},{"key":"35_CR13","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)"},{"key":"35_CR14","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, Heidelberg (2015)"},{"key":"35_CR15","unstructured":"Wiltsche, C.: Assume-Guarantee Strategy Synthesis for Stochastic Games. Ph.D. thesis, University of Oxford (2016, forthcoming)"},{"key":"35_CR16","unstructured":"PRISM-games website. \n                      www.prismmodelchecker.org\/games\/"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T01:15:13Z","timestamp":1585012513000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}