{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T01:00:54Z","timestamp":1773104454611,"version":"3.50.1"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656323","type":"print"},{"value":"9783031656330","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present version 2.0 of the<jats:italic>Partial Exploration Tool<\/jats:italic>(<jats:sc>Pet<\/jats:sc>), a tool for verification of probabilistic systems. We extend the previous version by adding support for<jats:italic>stochastic games<\/jats:italic>, based on a recent unified framework for sound value iteration algorithms. Thereby,<jats:sc>Pet2<\/jats:sc>is the first tool implementing a sound and efficient approach for solving stochastic games with objectives of the type reachability\/safety and mean payoff. We complement this approach by developing and implementing a partial-exploration based variant for all three objectives. Our experimental evaluation shows that<jats:sc>Pet2<\/jats:sc>offers the most efficient partial-exploration based algorithm and is the most viable tool on SGs, even outperforming unsound tools.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_16","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"359-372","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Playing Games with\u00a0Your PET: Extending the\u00a0Partial Exploration Tool to\u00a0Stochastic Games"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1712-2165","authenticated-orcid":false,"given":"Tobias","family":"Meggendorfer","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1825-0097","authenticated-orcid":false,"given":"Maximilian","family":"Weininger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"16_CR1","series-title":"NATO Science Series","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-94-010-0189-2_30","volume-title":"Stochastic Games and Applications","author":"R Amir","year":"2003","unstructured":"Amir, R.: Stochastic games in economics and related fields: an overview. In: Neyman, A., Sorin, S. (eds.) Stochastic Games and Applications. NATO Science Series, vol. 570, pp. 455\u2013470. Springer, Dordrecht (2003). https:\/\/doi.org\/10.1007\/978-94-010-0189-2_30"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-10631-6_13","volume-title":"Algorithms and Computation","author":"D Andersson","year":"2009","unstructured":"Andersson, D., Miltersen, P.B.: The complexity of solving stochastic games on graphs. In: Dong, Y., Du, D.-Z., Ibarra, O. (eds.) ISAAC 2009. LNCS, vol. 5878, pp. 112\u2013121. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10631-6_13"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Andriushchenko, R., et al.: Tools at the frontiers of quantitative verification: QComp 2023 competition report. TOOLympics (to appear)","DOI":"10.1007\/978-3-031-67695-6_4"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-63387-9_10","volume-title":"Computer Aided Verification","author":"P Ashok","year":"2017","unstructured":"Ashok, P., Chatterjee, K., Daca, P., K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T.: Value iteration for long-run average reward in Markov decision processes. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 201\u2013221. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_10"},{"key":"16_CR5","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-031-19992-9_18","volume-title":"ATVA 2022","author":"M Azeem","year":"2022","unstructured":"Azeem, M., Evangelidis, A., Kret\u00ednsk\u00fd, J., Slivinskiy, A., Weininger, M.: Optimistic and topological value iteration for simple stochastic games. In: Bouajjani, A., Hol\u00edk, L., Wu, Z. (eds.) ATVA 2022. LNCS, vol. 13505, pp. 285\u2013302. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_18"},{"key":"16_CR6","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"4","key":"16_CR7","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.plrev.2008.07.001","volume":"5","author":"N Bellomo","year":"2008","unstructured":"Bellomo, N., Delitala, M.: From the mathematical kinetic, and stochastic game theory to modelling mutations, onset, progression and immune competition of cancer cells. Phys. Life Rev. 5(4), 183\u2013206 (2008). https:\/\/doi.org\/10.1016\/j.plrev.2008.07.001","journal-title":"Phys. Life Rev."},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., et al.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"},{"key":"16_CR9","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":"16_CR10","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Meggendorfer, T., Saona, R., Svoboda, J.: Faster algorithm for turn-based stochastic games with bounded treewidth. In: SODA, pp. 4590\u20134605. SIAM (2023). https:\/\/doi.org\/10.1137\/1.9781611977554.CH173","DOI":"10.1137\/1.9781611977554.CH173"},{"issue":"1","key":"16_CR11","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.Z., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods Syst. Des. 43(1), 61\u201392 (2013). https:\/\/doi.org\/10.1007\/s10703-013-0183-7","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR12","unstructured":"Condon, A.: On algorithms for simple stochastic games. In: Advances In Computational Complexity Theory. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a013, pp. 51\u201371. DIMACS\/AMS (1990)"},{"issue":"4","key":"16_CR13","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"16_CR14","unstructured":"De\u00a0Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University (1997)"},{"issue":"Part","key":"16_CR15","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2022.104886","volume":"285","author":"J Eisentraut","year":"2022","unstructured":"Eisentraut, J., Kelmendi, E., Kret\u00ednsk\u00fd, J., Weininger, M.: Value iteration for simple stochastic games: stopping criterion and learning algorithm. Inf. Comput. 285(Part), 104886 (2022). https:\/\/doi.org\/10.1016\/j.ic.2022.104886","journal-title":"Inf. Comput."},{"key":"16_CR16","first-page":"179","volume":"3","author":"D Gillette","year":"1957","unstructured":"Gillette, D.: Stochastic games with zero stop probabilities. Contrib. Theory Games 3, 179\u2013187 (1957)","journal-title":"Contrib. Theory Games"},{"key":"16_CR17","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.tcs.2016.12.003","volume":"735","author":"S Haddad","year":"2018","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111\u2013131 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR18","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-031-30823-9_24","volume-title":"TACAS 2023","author":"A Hartmanns","year":"2023","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner\u2019s guide to MDP model checking algorithms. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13993, pp. 469\u2013488. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_24"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-030-53291-8_26","volume-title":"Computer Aided Verification","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 488\u2013511. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-030-17462-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2019","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 344\u2013350. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/S10009-021-00633-Z","DOI":"10.1007\/S10009-021-00633-Z"},{"issue":"2","key":"16_CR22","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1145\/1240233.1240247","volume":"3","author":"DS Johnson","year":"2007","unstructured":"Johnson, D.S.: The NP-completeness column: finding needles in haystacks. ACM Trans. Algorithms 3(2), 24 (2007). https:\/\/doi.org\/10.1145\/1240233.1240247","journal-title":"ACM Trans. Algorithms"},{"key":"16_CR23","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Of cores: a partial-exploration framework for Markov decision processes. Log. Methods Comput. Sci. 16(4) (2020). https:\/\/lmcs.episciences.org\/6833"},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Weininger, M.: Stopping criteria for value iteration on stochastic games with quantitative objectives. In: LICS, pp. 1\u201314 (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175771","DOI":"10.1109\/LICS56636.2023.10175771"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Weininger, M.: Stopping criteria for value iteration on stochastic games with quantitative objectives. CoRR abs\/2304.09930 (2023)","DOI":"10.1109\/LICS56636.2023.10175771"},{"issue":"Part","key":"16_CR26","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2022.104885","volume":"289","author":"J Kret\u00ednsk\u00fd","year":"2022","unstructured":"Kret\u00ednsk\u00fd, J., Ramneantu, E., Slivinskiy, A., Weininger, M.: Comparison of algorithms for simple stochastic games. Inf. Comput. 289(Part), 104885 (2022). https:\/\/doi.org\/10.1016\/j.ic.2022.104885","journal-title":"Inf. Comput."},{"key":"16_CR27","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"},{"issue":"11","key":"16_CR28","first-page":"1547","volume":"46","author":"D Lemire","year":"2016","unstructured":"Lemire, D., Kai, G.S.Y., Kaser, O.: Consistently faster and smaller compressed bitmaps with roaring. SPE 46(11), 1547\u20131569 (2016)","journal-title":"SPE"},{"key":"16_CR29","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-031-19992-9_20","volume-title":"ATVA 2022","author":"T Meggendorfer","year":"2022","unstructured":"Meggendorfer, T.: PET - a partial exploration tool for probabilistic verification. In: Bouajjani, A., Hol\u00edk, L., Wu, Z. (eds.) ATVA 2022. LNCS, vol. 13505, pp. 320\u2013326. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_20"},{"key":"16_CR30","unstructured":"Meggendorfer, T., Weininger, M.: Partial exploration tool gitlab. https:\/\/gitlab.lrz.de\/i7\/partial-exploration"},{"key":"16_CR31","doi-asserted-by":"publisher","unstructured":"Meggendorfer, T., Weininger, M.: Artifact for \u201cPartial Exploration Tool 2.0\u201d (2024). https:\/\/doi.org\/10.5281\/zenodo.10927672","DOI":"10.5281\/zenodo.10927672"},{"key":"16_CR32","doi-asserted-by":"publisher","unstructured":"Meggendorfer, T., Weininger, M.: Playing games with your pet: extending the partial exploration tool to stochastic games. CoRR abs\/2405.03885 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2405.03885","DOI":"10.48550\/ARXIV.2405.03885"},{"key":"16_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-030-88885-5_15","volume-title":"Automated Technology for Verification and Analysis","author":"S Pranger","year":"2021","unstructured":"Pranger, S., K\u00f6nighofer, B., Posch, L., Bloem, R.: TEMPEST - synthesis tool for reactive systems and shields in probabilistic environments. In: Hou, Z., Ganesh, V. (eds.) ATVA 2021. LNCS, vol. 12971, pp. 222\u2013228. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88885-5_15"},{"key":"16_CR34","doi-asserted-by":"publisher","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley (1994). https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"key":"16_CR35","doi-asserted-by":"publisher","unstructured":"Roy, S., Ellis, C., Shiva, S.G., Dasgupta, D., Shandilya, V., Wu, Q.: A survey of game theory as applied to network security. In: HICSS, pp. 1\u201310. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/HICSS.2010.35","DOI":"10.1109\/HICSS.2010.35"},{"key":"16_CR36","unstructured":"Weininger, M.: Solving Stochastic Games Reliably. Ph.D. thesis, Technical University of Munich, Germany (2022). https:\/\/mediatum.ub.tum.de\/node?id=1661588"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65633-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T20:14:57Z","timestamp":1732479297000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}