{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:59:31Z","timestamp":1779087571072,"version":"3.51.4"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032104434","type":"print"},{"value":"9783032104441","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-10444-1_8","type":"book-chapter","created":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T06:58:53Z","timestamp":1762844333000},"page":"129-147","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Certificates and\u00a0Witnesses for\u00a0Multi-objective $$\\omega $$-Regular Queries in\u00a0Markov Decision Processes"],"prefix":"10.1007","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Calvin","family":"Chau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Volodymyr","family":"Drobitko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Jantsch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sascha","family":"Kl\u00fcppelholz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,12]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A., Giacobbe, M., Roy, D.: Quantitative Supermartingale Certificates. In: CAV. LNCS, vol. 15932, pp. 3\u201328. Springer Nature Switzerland, Cham (2025)","DOI":"10.1007\/978-3-031-98679-6_1"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., et al.: From Spot 2.0 to Spot 2.10: What\u2019s New? In: CAV. LNCS, vol. 13372, pp. 174\u2013187. Springer (2022)","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Aljazzar, H., Leue, S.: Generation of counterexamples for model checking of Markov decision processes. In: QEST, pp. 197\u2013206 (2009)","DOI":"10.1109\/QEST.2009.10"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Baier, C., Chau, C., Drobitko, V., Jantsch, S., Kl\u00fcppelholz, S.: Artefact for SEFM 2025 (2025). https:\/\/doi.org\/10.5281\/zenodo.15680332","DOI":"10.5281\/zenodo.15680332"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Baier, C., Chau, C., Drobitko, V., Jantsch, S., Kl\u00fcppelholz, S.: Certificates and witnesses for multi-objective $$\\omega $$-regular queries in Markov decision processes (2025). https:\/\/doi.org\/10.48550\/arXiv.2508.17859","DOI":"10.48550\/arXiv.2508.17859"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Baier, C., Chau, C., Kl\u00fcppelholz, S.: Certificates and witnesses for multi-objective queries in Markov decision processes. In: QEST+FORMATS. LNCS, vol. 14996, pp. 1\u201318. Springer Nature Switzerland, Cham (2024)","DOI":"10.1007\/978-3-031-68416-6_1"},{"key":"8_CR7","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)"},{"key":"8_CR8","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.jcss.2023.03.005","volume":"136","author":"C Baier","year":"2023","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)","journal-title":"J. Comput. Syst. Sci."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Brozek, V., Chatterjee, K., Forejt, V., Kucera, A.: Two views on multiple mean-payoff objectives in Markov decision processes. In: Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science, pp. 33\u201342. LICS \u201911, IEEE Computer Society, USA (2011)","DOI":"10.1109\/LICS.2011.10"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: CAV. LNCS, vol.\u00a08044, pp. 511\u2013526. Springer, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Quatmann, T., Sch\u00e4ffeler, M., Weininger, M., Winkler, T., Zilken, D.: Fixed point certificates for reachability and expected rewards in MDPs. In: TACAS. LNCS, vol. 15697, pp. 130\u2013151. Springer Nature Switzerland, Cham (2025)","DOI":"10.1007\/978-3-031-90653-4_7"},{"key":"8_CR12","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. Ph.D. thesis, Stanford University, Stanford, CA, USA (1997)"},{"issue":"4","key":"8_CR13","doi-asserted-by":"publisher","first-page":"990","DOI":"10.2168\/LMCS-4(4:8)2008","volume":"4","author":"K Etessami","year":"2008","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Logical Methods Comput. Sci. 4(4), 990 (2008)","journal-title":"Logical Methods Comput. Sci."},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: TACAS. LNCS, vol. 6605, pp. 112\u2013127. Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-19835-9_11"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: ATVA. LNCS, vol.\u00a07561, pp. 317\u2013332. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-33386-6_25"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Funke, F., Jantsch, S., Baier, C.: Farkas certificates and minimal witnesses for probabilistic reachability constraints. In: TACAS. LNCS, vol. 12078, pp. 324\u2013345. Springer International Publishing, Cham (2020)","DOI":"10.1007\/978-3-030-45190-5_18"},{"key":"8_CR17","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2024)"},{"issue":"2","key":"8_CR18","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1109\/TSE.2009.5","volume":"35","author":"T Han","year":"2009","unstructured":"Han, T., Katoen, J.P., Damman, B.: Counterexample generation in probabilistic model checking. IEEE Trans. Software Eng. 35(2), 241\u2013257 (2009)","journal-title":"IEEE Trans. Software Eng."},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: TACAS. LNCS, vol. 11427, pp. 344\u2013350. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-17462-0_20"},{"issue":"4","key":"8_CR20","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-021-00633-z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transfer 24(4), 589\u2013610 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Mallik, K., Sadeghi, P., \u017dikeli\u0107, \u0110.: Supermartingale certificates for\u00a0quantitative omega-regular verification and\u00a0control. In: CAV. LNCS, vol. 15932, pp. 29\u201355. Springer Nature Switzerland, Cham (2025)","DOI":"10.1007\/978-3-031-98679-6_2"},{"issue":"2","key":"8_CR22","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/0020-0190(90)90107-9","volume":"35","author":"T Herman","year":"1990","unstructured":"Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63\u201367 (1990)","journal-title":"Inf. Process. Lett."},{"key":"8_CR23","unstructured":"Jansen, N.: Counterexamples in Probabilistic Verification. Ph.D. thesis, RWTH Aachen University, Germany (2015)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Jansen, N., \u00c1brah\u00e1m, E., Katelaan, J., Wimmer, R., Katoen, J.P., Becker, B.: Hierarchical counterexamples for discrete-time Markov chains. In: ATVA. LNCS, vol.\u00a06996, pp. 443\u2013452. Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-24372-1_33"},{"key":"8_CR25","unstructured":"Jantsch, S.: Certificates and Witnesses for Probabilistic Model Checking. Ph.D. thesis, Technische Universit\u00e4t Dresden, Dresden (2022)"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Kuntz, M., Leitner-Fischer, F., Leue, S.: From probabilistic counterexamples via causality to fault trees. In: Computer Safety, Reliability, and Security. LNCS, vol. 6894, pp. 71\u201384. Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-24270-0_6"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Kwiatkowsa, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: QEST, pp. 203\u2013204 (2012)","DOI":"10.1109\/QEST.2012.14"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: CAV. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"issue":"2","key":"8_CR29","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"R McConnell","year":"2011","unstructured":"McConnell, R., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119\u2013161 (2011)","journal-title":"Comput. Sci. Rev."},{"key":"8_CR30","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming, 1st edn. John Wiley & Sons Inc, USA (1994)","edition":"1"},{"key":"8_CR31","unstructured":"Quatmann, T.: Verification of Multi-Objective Markov Models. Ph.D. thesis, RWTH Aachen University (2023)"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Randour, M., Raskin, J.F., Sankur, O.: Percentile queries in multi-dimensional Markov decision processes. In: CAV. LNCS, vol.\u00a09206, pp. 123\u2013139. Springer International Publishing, Cham (2015)","DOI":"10.1007\/978-3-319-21690-4_8"},{"issue":"12","key":"8_CR33","first-page":"15073","volume":"37","author":"M Sch\u00e4ffeler","year":"2023","unstructured":"Sch\u00e4ffeler, M., Abdulaziz, M.: Formally verified solution methods for Markov decision processes. Proc. AAAI Conf. Artif. Intell. 37(12), 15073\u201315081 (2023)","journal-title":"Proc. AAAI Conf. Artif. Intell."},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Sickert, S., K\u0159et\u00ednsk\u00fd, J.: MoChiBA: probabilistic LTL model checking using limit-deterministic B\u00fcchi automata. In: ATVA. LNCS, vol.\u00a09938, pp. 130\u2013137. Springer International Publishing, Cham (2016)","DOI":"10.1007\/978-3-319-46520-3_9"},{"issue":"2","key":"8_CR35","doi-asserted-by":"publisher","first-page":"5:1","DOI":"10.1145\/3450967","volume":"43","author":"T Takisaka","year":"2021","unstructured":"Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartingales for reachability in randomized programs. ACM Trans. Program. Lang. Syst. 43(2), 5:1-5:46 (2021)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Becker, B., Katoen, J.P.: Minimal critical subsystems for discrete-time Markov models. In: TACAS. LNCS, vol. 7214, pp. 299\u2013314. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28756-5_21"},{"key":"8_CR37","unstructured":"Wimmer, R., Kortus, A., Herbstritt, M., Becker, B.: The demand for reliability in probabilistic verification. In: MBMV, pp. 99\u2013108 (2008)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10444-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T14:06:58Z","timestamp":1770905218000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10444-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,12]]},"ISBN":["9783032104434","9783032104441"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10444-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,12]]},"assertion":[{"value":"12 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toledo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","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":"10 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}