{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T19:34:14Z","timestamp":1757619254033,"version":"3.44.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986789"},{"type":"electronic","value":"9783031986796"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Good-for-Games (GfG) automata require that their nondeterminism can be resolved on-the-fly, while unambiguous automata guarantee that no word has more than one accepting run. These two mutually exclusive ways of restricted nondeterminism play their roles independently in Markov chain model checking (MCMC) for almost a decade but synthesising them seems hopeless: an automaton that is both GfG and unambiguous is essentially deterministic. This work breaks this perception by combining the strengths of unambiguity with the GfG co-B\u00fcchi minimisation recently proposed by Abu Radi and Kupferman. More precisely, this combination allows us to turn unambiguous automata to certain types of probabilistic automata that can be used for MCMC. The resulting automata can be exponentially smaller, and we have provided a family of automata exemplifying this state space reduction, which translates into a significant acceleration of MCMC.\n<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_13","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:20:58Z","timestamp":1753089658000},"page":"276-298","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Accelerating Markov Chain Model Checking: Good-for-Games Meets Unambiguous Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7301-9234","authenticated-orcid":false,"given":"Yong","family":"Li","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7233-2018","authenticated-orcid":false,"given":"Soumyajit","family":"Paul","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9093-9518","authenticated-orcid":false,"given":"Sven","family":"Schewe","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9265-3011","authenticated-orcid":false,"given":"Qiyi","family":"Tang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Abu Radi, B., Kupferman, O.: Minimization and canonization of GFG transition-based automata. Log. Methods Comput. Sci. 18(3), 16:1\u201316:33 (2022). https:\/\/doi.org\/10.46298\/LMCS-18(3:16)2022","DOI":"10.46298\/LMCS-18(3:16)2022"},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-21690-4_31","volume-title":"Computer Aided Verification","author":"T Babiak","year":"2015","unstructured":"Babiak, T., et al.: The Hanoi omega-automata format. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification, pp. 479\u2013486. Springer, Cham (2015)"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Bertrand, N.: Probabilistic $$\\omega $$-automata. J. ACM 59(1), 1:1\u20131:52 (2012). https:\/\/doi.org\/10.1145\/2108242.2108243","DOI":"10.1145\/2108242.2108243"},{"key":"13_CR4","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Baier, C., Kiefer, S., Klein, J., M\u00fcller, D., Worrell, J.: Markov chains and unambiguous automata. J. Comput. Syst. Sci. 136, 113\u2013134 (2023). https:\/\/doi.org\/10.1016\/J.JCSS.2023.03.005","DOI":"10.1016\/J.JCSS.2023.03.005"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Boker, U., Kupferman, O., Skrzypczak, M.: How deterministic are good-for-games automata? In: Lokam, S.V., Ramanujam, R. (eds.) 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, Kanpur, India, 11\u201315 December 2017. LIPIcs, vol.\u00a093, pp. 18:1\u201318:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPICS.FSTTCS.2017.18","DOI":"10.4230\/LIPICS.FSTTCS.2017.18"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Bustan, D., Rubin, S., Vardi, M.Y.: Verifying omega-regular properties of Markov chains. In: Alur, R., Peled, D.A. (eds.) Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, 13\u201317 July 2004, Proceedings. LNCS, vol.\u00a03114, pp. 189\u2013201. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_15","DOI":"10.1007\/978-3-540-27813-9_15"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Carton, O., Michel, M.: Unambiguous B\u00fcchi automata. Theor. Comput. Sci. 297(1\u20133), 37\u201381 (2003). https:\/\/doi.org\/10.1016\/S0304-3975(02)00618-7","DOI":"10.1016\/S0304-3975(02)00618-7"},{"issue":"4","key":"13_CR9","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). https:\/\/doi.org\/10.1145\/210332.210339","journal-title":"J. ACM"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Couvreur, J., Saheb, N., Sutre, G.: An optimal automata approach to LTL model checking of probabilistic systems. In: Vardi, M.Y., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, 10th International Conference, LPAR 2003, Almaty, Kazakhstan, 22\u201326 September 2003, Proceedings. LNCS, vol.\u00a02850, pp. 361\u2013375. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-39813-4_26","DOI":"10.1007\/978-3-540-39813-4_26"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 - a framework for LTL and omega-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, 17\u201320 October 2016, Proceedings. LNCS, vol.\u00a09938, pp. 122\u2013129 (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From Spot 2.0 to Spot 2.10: what\u2019s new? In: Proceedings of the 34th International Conference on Computer Aided Verification (CAV 2022). LNCS, vol. 13372, pp. 174\u2013187. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Fu, C., et al.: EPMC gets knowledge in multi-agent systems. In: Finkbeiner, B., Wies, T. (eds.) Verification, Model Checking, and Abstract Interpretation - 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, 16\u201318 January 2022, Proceedings. LNCS, vol. 13182, pp. 93\u2013107. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_5","DOI":"10.1007\/978-3-030-94583-1_5"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Li, G., Schewe, S., Turrini, A., Zhang, L.: Lazy probabilistic model checking without determinisation. In: Aceto, L., de\u00a0Frutos-Escrig, D. (eds.) 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, 1\u20134 September 2015. LIPIcs, vol.\u00a042, pp. 354\u2013367. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2015.354","DOI":"10.4230\/LIPICS.CONCUR.2015.354"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: ISCASMC: a web-based probabilistic model checker. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014: Formal Methods - 19th International Symposium, Singapore, 12\u201316 May 2014. Proceedings. LNCS, vol.\u00a08442, pp. 312\u2013317. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_22","DOI":"10.1007\/978-3-319-06410-9_22"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., Wojtczak, D.: Good-for-MDPs automata for probabilistic analysis and reinforcement learning. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, 25\u201330 April 2020, Proceedings, Part I. LNCS, vol. 12078, pp. 306\u2013323. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_17","DOI":"10.1007\/978-3-030-45190-5_17"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Piterman, N.: Solving games without determinization. In: \u00c9sik, Z. (ed.) Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, 25\u201329 September 2006, Proceedings. LNCS, vol.\u00a04207, pp. 395\u2013410. Springer (2006). https:\/\/doi.org\/10.1007\/11874683_26","DOI":"10.1007\/11874683_26"},{"key":"13_CR18","unstructured":"Hoschek, W.: The Colt distribution: open source libraries for high performance scientific and technical computing in Java (2002). http:\/\/nicewww.cern.ch\/hoschek\/colt\/index.htm"},{"issue":"1\u20132","key":"13_CR19","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/S10703-021-00379-Z","volume":"58","author":"S Jantsch","year":"2021","unstructured":"Jantsch, S., M\u00fcller, D., Baier, C., Klein, J.: From LTL to unambiguous B\u00fcchi automata via disambiguation of alternating automata. Formal Methods Syst. Des. 58(1\u20132), 42\u201382 (2021). https:\/\/doi.org\/10.1007\/S10703-021-00379-Z","journal-title":"Formal Methods Syst. Des."},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Klein, J., M\u00fcller, D., Baier, C., Kl\u00fcppelholz, S.: Are good-for-games automata good for probabilistic model checking? In: Dediu, A., Mart\u00edn-Vide, C., Sierra-Rodr\u00edguez, J.L., Truthe, B. (eds.) Language and Automata Theory and Applications - 8th International Conference, LATA 2014, Madrid, Spain, 10\u201314 March 2014. Proceedings. LNCS, vol.\u00a08370, pp. 453\u2013465. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-04921-2_37","DOI":"10.1007\/978-3-319-04921-2_37"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Kuperberg, D., Skrzypczak, M.: On determinisation of good-for-games automata. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, 6\u201310 July 2015, Proceedings, Part II. LNCS, vol.\u00a09135, pp. 299\u2013310. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_24","DOI":"10.1007\/978-3-662-47666-6_24"},{"key":"13_CR22","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 the 23rd International Conference on Computer Aided Verification (CAV 2011). LNCS, vol.\u00a06806, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Li, Y., Schewe, S., Vardi, M.Y.: Singly exponential translation of alternating weak B\u00fcchi automata to unambiguous B\u00fcchi automata. Theor. Comput. Sci. 1006, 114650 (2024). https:\/\/doi.org\/10.1016\/J.TCS.2024.114650","DOI":"10.1016\/J.TCS.2024.114650"},{"key":"13_CR24","unstructured":"Rohde, G.S.: Alternating automata and the temporal logic of ordinals. Ph.D. thesis, University of Illinois at Urbana-Champaign (1997)"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Schewe, S., Tang, Q., Zhanabekova, T.: Deciding what is good-for-MDPs. In: P\u00e9rez, G.A., Raskin, J. (eds.) 34th International Conference on Concurrency Theory, CONCUR 2023, Antwerp, Belgium, 18\u201323 September 2023. LIPIcs, vol.\u00a0279, pp. 35:1\u201335:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2023.35","DOI":"10.4230\/LIPICS.CONCUR.2023.35"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Sickert, S., Esparza, J., Jaax, S., Kret\u00ednsk\u00fd, J.: Limit-deterministic B\u00fcchi automata for linear temporal logic. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, 17\u201323 July 2016, Proceedings, Part II. LNCS, vol.\u00a09780, pp. 312\u2013332. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_17","DOI":"10.1007\/978-3-319-41540-6_17"}],"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-98679-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T16:19:06Z","timestamp":1757261946000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}