{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,1]],"date-time":"2026-03-01T14:21:03Z","timestamp":1772374863367,"version":"3.50.1"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,11,29]],"date-time":"2017-11-29T00:00:00Z","timestamp":1511913600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000855","name":"University of Birmingham","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000855","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2018,4]]},"DOI":"10.1007\/s10009-017-0476-z","type":"journal-article","created":{"date-parts":[[2017,11,29]],"date-time":"2017-11-29T07:33:44Z","timestamp":1511940824000},"page":"195-210","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":33,"title":["PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives"],"prefix":"10.1007","volume":"20","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":[[2017,11,29]]},"reference":[{"key":"476_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.: Reactive modules. In: Proceedings of 11th Annual IEEE Symposium on Logic in Computer Science (LICS\u201996), pp. 207\u2013218. IEEE Computer Society Press, July 1996","DOI":"10.1109\/LICS.1996.561320"},{"issue":"5","key":"476_CR2","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"476_CR3","doi-asserted-by":"crossref","unstructured":"Aslanyan, Z., Nielson, F., Parker, D.: Quantitative verification and synthesis of attack\u2013defence scenarios. In: Proceedings of 29th IEEE Computer Security Foundations Symposium (CSF\u201916), pp. 105\u2013119. IEEE (2016)","DOI":"10.1109\/CSF.2016.15"},{"issue":"1\u20132","key":"476_CR4","doi-asserted-by":"crossref","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":"476_CR5","doi-asserted-by":"crossref","unstructured":"Basset, N., Kwiatkowska, M., Topcu, U., Wiltsche, C.: Strategy synthesis for stochastic games with multiple long-run objectives. In: Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915), volume 9035 of LNCS, pp. 256\u2013271. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_22"},{"key":"476_CR6","doi-asserted-by":"crossref","unstructured":"Basset, N., Kwiatkowska, M., Wiltsche, C.: Compositional controller synthesis for stochastic games. In: Proceedings of 25th International Conference on Concurrency Theory (CONCUR\u201914), volume 8704 of LNCS, pp. 173\u2013187. Springer (2014)","DOI":"10.1007\/978-3-662-44584-6_13"},{"key":"476_CR7","doi-asserted-by":"crossref","unstructured":"Basset, N., Kwiatkowska, M., Wiltsche, C.: Compositional strategy synthesis for stochastic games with multiple objectives. Inf. Comput. (2017). https:\/\/doi.org\/10.1016\/j.ic.2017.09.010","DOI":"10.1016\/j.ic.2017.09.010"},{"key":"476_CR8","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: Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915), volume 9035 of LNCS, pp. 181\u2013187. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_12"},{"key":"476_CR9","doi-asserted-by":"crossref","unstructured":"Brenguier, R.: PRALINE: a tool for computing Nash equilibria in concurrent games. In: Proceedings of 25th International Conference on Computer Aided Verification (CAV\u201913), volume 8044 of LNCS, pp. 890\u2013895. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_63"},{"key":"476_CR10","doi-asserted-by":"crossref","unstructured":"C\u00e1mara, J., Moreno, G.A. Garlan, D.: Stochastic game analysis and latency awareness for proactive self-adaptation. In: Proceedings of Software Engineering for Adaptive and Self-Managing Systems (SEAMS\u201914), pp. 155\u2013164 (2014)","DOI":"10.1145\/2593929.2593933"},{"key":"476_CR11","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T. Jobstmann, B., Radhakrishna, A.: Gist: a solver for probabilistic games. In: Proceedings of 22nd International Conference on Computer Aided Verification (CAV\u201910), LNCS, pp. 665\u2013669. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_57"},{"issue":"1","key":"476_CR12","doi-asserted-by":"crossref","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. Form. Methods Syst. Des. 43(1), 61\u201392 (2013)","journal-title":"Form. Methods Syst. Des."},{"key":"476_CR13","doi-asserted-by":"crossref","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: PRISM-games: a model checker for stochastic multi-player games. In: Proc. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201913), volume 7795 of LNCS, pp. 185\u2013191. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_13"},{"key":"476_CR14","doi-asserted-by":"crossref","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: On stochastic games with multiple objectives. In: Proceedings of 38th International Symposium on Mathematical Foundations of Computer Science (MFCS\u201913), volume 8087 of LNCS, pp. 266\u2013277. Springer (2013)","DOI":"10.1007\/978-3-642-40313-2_25"},{"key":"476_CR15","doi-asserted-by":"crossref","unstructured":"Chen, T., Kwiatkowska, M., Parker, D., Simaitis, A.: Verifying team formation protocols with probabilistic model checking. In: Proceedings of 12th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA XII 2011), volume 6814 of LNCS, pp. 190\u2013297. Springer (2011)","DOI":"10.1007\/978-3-642-22359-4_14"},{"key":"476_CR16","doi-asserted-by":"crossref","unstructured":"Chen, T., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: Synthesis for multi-objective stochastic games: an application to autonomous urban driving. In: Proceedings of 10th International Conference on Quantitative Evaluation of Systems (QEST\u201913), volume 8054 of LNCS, pp. 322\u2013337. Springer (2013)","DOI":"10.1007\/978-3-642-40196-1_28"},{"key":"476_CR17","doi-asserted-by":"crossref","unstructured":"Cheng, C., Knoll, A., Luttenberger, M., Buckl, C.: GAVS+: an open platform for the research of algorithmic game solving. In: Proceedings of 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201911), pp. 258\u2013261. Springer (2011)","DOI":"10.1007\/978-3-642-19835-9_22"},{"key":"476_CR18","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1090\/dimacs\/013\/04","volume":"13","author":"A Condon","year":"1993","unstructured":"Condon, A.: On algorithms for simple stochastic games. Adv. Comput. Complex. Theory DIMACS Ser. Discrete Math. Theor. Comput. Sci. 13, 51\u201373 (1993)","journal-title":"Adv. Comput. Complex. Theory DIMACS Ser. Discrete Math. Theor. Comput. Sci."},{"key":"476_CR19","doi-asserted-by":"crossref","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Mikucionis, M., Taankvist, J.H.: Uppaal stratego. In: Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915), volume 9035 of LNCS, pp. 206\u2013211. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_16"},{"key":"476_CR20","unstructured":"de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University (1997)"},{"key":"476_CR21","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Proceedings of 29th International Conference on Computer Aided Verification (CAV\u201917) (2017)","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"476_CR22","doi-asserted-by":"crossref","unstructured":"Deshpande, T., Katsaros, P., Smolka, S., Stoller, S.: Stochastic game-based analysis of the DNS bandwidth amplification attack using probabilistic model checking. In: Proceedings of European Dependable Computing Conference (EDCC\u201914), pp. 226\u2013237 (2014)","DOI":"10.1109\/EDCC.2014.37"},{"issue":"4","key":"476_CR23","first-page":"1","volume":"4","author":"K Etessami","year":"2008","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Logical Methods Comput. Sci. 4(4), 1\u201321 (2008)","journal-title":"Logical Methods Comput. Sci."},{"key":"476_CR24","doi-asserted-by":"crossref","unstructured":"Feng, L., Wiltsche, C., Humphrey, L., Topcu, U.: Controller synthesis for autonomous systems interacting with human operators. In: Proceedings of IEEE\/ACM International Conference on Cyber-Physical Systems (ICCPS\u201915), pp. 70\u201379 (2015)","DOI":"10.1145\/2735960.2735973"},{"key":"476_CR25","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems (SFM\u201911), Volume 6659 of LNCS","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) Formal Methods for Eternal Networked Software Systems (SFM\u201911), Volume 6659 of LNCS, pp. 53\u2013113. Springer, Berlin (2011)"},{"key":"476_CR26","doi-asserted-by":"crossref","unstructured":"Glazier, T., Camara, J., Schmerl, B., Garlan, D.: Analyzing resilience properties of different topologies of collective adaptive systems. In: Proceedings of Self-Adaptive and Self-Organizing Systems Workshops (SASOW\u201915), pp. 55\u201360 (2015)","DOI":"10.1109\/SASOW.2015.14"},{"key":"476_CR27","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Proceedings of 19th International Symposium on Formal Methods (FM\u201914), pp. 312\u2013317 (2014)","DOI":"10.1007\/978-3-319-06410-9_22"},{"issue":"5","key":"476_CR28","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512\u2013535 (1994)","journal-title":"Form. Asp. Comput."},{"key":"476_CR29","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: Proceedings of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914), volume 8413 of LNCS, pp. 593\u2013598. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"476_CR30","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/s100970050003","volume":"2","author":"B Huber","year":"1999","unstructured":"Huber, B., Rambau, J., Santos, F.: The Cayley trick, lifting subdivisions and the Bohne-Dress theorem on zonotopal tilings. JEMS 2, 179\u2013198 (1999)","journal-title":"JEMS"},{"issue":"2","key":"476_CR31","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J-P Katoen","year":"2011","unstructured":"Katoen, J.-P., Zapreev, I., Hahn, E.M., Hermanns, H., Jansen, D.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"key":"476_CR32","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proceedings of 23rd International Conference on Computer Aided Verification (CAV\u201911), volume 6806 of LNCS, pp, 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"476_CR33","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1016\/j.ic.2013.10.001","volume":"232","author":"M Kwiatkowska","year":"2013","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Compositional probabilistic verification through multi-objective model checking. Inf. Comput. 232, 38\u201365 (2013)","journal-title":"Inf. Comput."},{"key":"476_CR34","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Parker, D., Wiltsche, C.: PRISM-games 2.0: a tool for multi-objective strategy synthesis for stochastic games. In: Proceedings of 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201916), LNCS. Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_35"},{"issue":"1","key":"476_CR35","doi-asserted-by":"crossref","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. Logic 8(1), 3 (2007)","journal-title":"ACM Trans. Comput. Logic"},{"key":"476_CR36","unstructured":"Segala, R.: Modelling and verification of randomized distributed real time systems. Ph.D. thesis, Massachusetts Institute of Technology (1995)"},{"issue":"10","key":"476_CR37","doi-asserted-by":"crossref","first-page":"1095","DOI":"10.1073\/pnas.39.10.1953","volume":"39","author":"LS Shapley","year":"1953","unstructured":"Shapley, L.S.: Stochastic games. PNAS 39(10), 1095 (1953)","journal-title":"PNAS"},{"key":"476_CR38","unstructured":"Simaitis, A.: Automatic verification of competitive stochastic systems. Ph.D. thesis, Department of Computer Science, University of Oxford (2014)"},{"key":"476_CR39","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang. J.: PAT: towards flexible verification under fairness. In: Proceedings of 21st International Conference on Computer Aided Verification (CAV\u201909), volume 5643 of LNCS, pp. 709\u2013714. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"476_CR40","doi-asserted-by":"crossref","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":"476_CR41","doi-asserted-by":"crossref","unstructured":"Toumi, A., Gutierrez, J., Wooldridge, M.: A tool for the automated verification of Nash equilibria in concurrent games. In: Proceedings of 12th International Colloquium on Theoretical Aspects of Computing (ICTAC\u201915), volume 9399 of LNCS, pp. 583\u2013594. Springer (2015)","DOI":"10.1007\/978-3-319-25150-9_34"},{"key":"476_CR42","unstructured":"Ujma, M.: On verification and controller synthesis for probabilistic systems at runtime. Ph.D. thesis, University of Oxford (2015)"},{"key":"476_CR43","unstructured":"Weibel, C.: Minkowski sums of polytopes: combinatorics and computation. Ph.D. thesis, \u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne (2007)"},{"key":"476_CR44","unstructured":"Wiltsche, C.: Assume-guarantee strategy synthesis for stochastic games. Ph.D. thesis, University of Oxford (2015)"},{"key":"476_CR45","unstructured":"PRISM-games website. www.prismmodelchecker.org\/games\/"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-017-0476-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0476-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0476-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T22:44:00Z","timestamp":1570401840000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-017-0476-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,29]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,4]]}},"alternative-id":["476"],"URL":"https:\/\/doi.org\/10.1007\/s10009-017-0476-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,11,29]]}}}