{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T21:00:38Z","timestamp":1757624438621,"version":"3.44.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031974380"},{"type":"electronic","value":"9783031974397"}],"license":[{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"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-031-97439-7_8","type":"book-chapter","created":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T11:03:54Z","timestamp":1756551834000},"page":"174-196","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Probabilistic Counterexamples Through the Ages"],"prefix":"10.1007","author":[{"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"first","affiliation":[]},{"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[]},{"given":"Simon","family":"Jantsch","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,8,30]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-319-07317-0_3","volume-title":"Formal Methods for Executable Software Models","author":"E \u00c1brah\u00e1m","year":"2014","unstructured":"\u00c1brah\u00e1m, E., Becker, B., Dehnert, C., Jansen, N., Katoen, J.-P., Wimmer, R.: Counterexample generation for discrete-time Markov models: an introductory survey. In: Bernardo, M., Damiani, F., H\u00e4hnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 65\u2013121. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07317-0_3"},{"key":"8_CR2","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"issue":"3","key":"8_CR3","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/s10589-016-9847-8","volume":"65","author":"P Belotti","year":"2016","unstructured":"Belotti, P., et al.: On handling indicator constraints in mixed integer programming. Comput. Optim. Appl. 65(3), 545\u2013566 (2016). https:\/\/doi.org\/10.1007\/s10589-016-9847-8","journal-title":"Comput. Optim. Appl."},{"issue":"1","key":"8_CR4","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10107-015-0891-4","volume":"151","author":"P Bonami","year":"2015","unstructured":"Bonami, P., Lodi, A., Tramontani, A., Wiese, S.: On mathematical programming with indicator constraints. Math. Program. 151(1), 191\u2013223 (2015). https:\/\/doi.org\/10.1007\/s10107-015-0891-4","journal-title":"Math. Program."},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-642-21461-5_5","volume-title":"Formal Techniques for Distributed Systems","author":"B Braitling","year":"2011","unstructured":"Braitling, B., Wimmer, R., Becker, B., Jansen, N., \u00c1brah\u00e1m, E.: Counterexample generation for Markov chains using SMT-based bounded model checking. In: Bruni, R., Dingel, J. (eds.) FMOODS\/FORTE -2011. LNCS, vol. 6722, pp. 75\u201389. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21461-5_5"},{"key":"8_CR6","unstructured":"Braitling, B., Wimmer, R., Becker, B., Jansen, N., \u00c1brah\u00e1m, E.: SMT-based counterexample generation for Markov chains. In: Proceedings of Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV 2011), pp. 19\u201328. OFFIS-Institut f\u00fcr Informatik (2011)"},{"key":"8_CR7","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. Log. Methods Comput. Sci. 10(1) (2014)","DOI":"10.2168\/LMCS-10(1:13)2014"},{"key":"8_CR8","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 (2025). https:\/\/arxiv.org\/abs\/2501.11467","DOI":"10.1007\/978-3-031-90653-4_7"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Damman, B., Han, T., Katoen, J.P.: Regular expressions for PCTL counterexamples. In: Proceedings of the 5th International Conference on Quantitative Evaluation of Systems (QEST 2008), pp. 179\u2013188 (2008)","DOI":"10.1109\/QEST.2008.11"},{"issue":"1","key":"8_CR10","first-page":"1","volume":"22","author":"N Dinh","year":"2014","unstructured":"Dinh, N., Jeyakumar, V.: Farkas\u2019 lemma: three decades of generalizations for mathematical optimization. Trans. Oper. Res. 22(1), 1\u201322 (2014)","journal-title":"Trans. Oper. Res."},{"issue":"124","key":"8_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1515\/crll.1902.124.1","volume":"1902","author":"J Farkas","year":"1902","unstructured":"Farkas, J.: Theorie der einfachen Ungleichungen. J. reine angewandte Math. (Crelles J.) 1902(124), 1\u201327 (1902)","journal-title":"J. reine angewandte Math. (Crelles J.)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-030-45190-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Funke","year":"2020","unstructured":"Funke, F., Jantsch, S., Baier, C.: Farkas certificates and minimal witnesses for probabilistic reachability constraints. In: TACAS 2020. LNCS, vol. 12078, pp. 324\u2013345. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_18"},{"issue":"2","key":"8_CR13","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. Softw. Eng. 35(2), 241\u2013257 (2009)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR14","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":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-642-24372-1_33","volume-title":"Automated Technology for Verification and Analysis","author":"N Jansen","year":"2011","unstructured":"Jansen, N., \u00c1brah\u00e1m, E., Katelaan, J., Wimmer, R., Katoen, J.-P., Becker, B.: Hierarchical counterexamples for discrete-time Markov chains. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 443\u2013452. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_33"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-642-33386-6_27","volume-title":"Automated Technology for Verification and Analysis","author":"N Jansen","year":"2012","unstructured":"Jansen, N., \u00c1brah\u00e1m, E., Volk, M., Wimmer, R., Katoen, J.-P., Becker, B.: The COMICS tool \u2013 computing minimal counterexamples for DTMCs. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 349\u2013353. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_27"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-642-35861-6_9","volume-title":"Formal Aspects of Component Software","author":"N Jansen","year":"2013","unstructured":"Jansen, N., et al.: Symbolic counterexample generation for discrete-time Markov chains. In: P\u0103s\u0103reanu, C.S., Sala\u00fcn, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 134\u2013151. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35861-6_9"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Jansen, N., Wimmer, R., \u00c1brah\u00e1m, E., Zajzon, B., Katoen, J.P., Becker, B.: Symbolic counterexample generation for large discrete-time Markov chains. Sci. Comput. Program. 91(A), 90\u2013114 (2014)","DOI":"10.1016\/j.scico.2014.02.001"},{"key":"8_CR19","unstructured":"Jantsch, S.: Certificates and witnesses for probabilistic model checking. Ph.D. thesis, Dresden University of Technology, Germany (2022)"},{"key":"8_CR20","unstructured":"Jantsch, S., Harder, H., Funke, F., Baier, C.: SWITSS: computing small witnessing subsystems. In: Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design (FMCAD 2020), vol.\u00a01, pp. 236\u2013244. TU Wien Academic Press (2020)"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Jantsch, S., Piribauer, J., Baier, C.: Witnessing subsystems for probabilistic systems with low tree width. In: Proceedings of the 12th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2021). Electronic Proceedings in Theoretical Computer Science, vol.\u00a0346, pp. 35\u201351. Open Publishing Association (2021)","DOI":"10.4204\/EPTCS.346.3"},{"key":"8_CR22","unstructured":"Kallenberg, L.: Linear programming and finite Markovian control problems. Mathematical Centre, Amsterdam (1983)"},{"issue":"2","key":"8_CR23","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"RM McConnell","year":"2011","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119\u2013161 (2011)","journal-title":"Comput. Sci. Rev."},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-319-19249-9_27","volume-title":"FM 2015: Formal Methods","author":"T Quatmann","year":"2015","unstructured":"Quatmann, T., et al.: Counterexamples for expected rewards. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 435\u2013452. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_27"},{"key":"8_CR25","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley-Interscience Series in Discrete Mathematics and Optimization. Wiley (1999)"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of the 26th Annual Symposium on Foundations of Computer Science (FOCS 1985), pp. 327\u2013338. IEEE (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"8_CR27","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Katoen, J.P., Becker, B.: Minimal counterexamples for refuting $$\\omega $$-regular properties of Markov decision processes. Reports of SFB\/TR 14 AVACS\u00a088 (2012)"},{"key":"8_CR28","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Katoen, J.P., Becker, B.: Minimal critical subsystems as counterexamples for $$\\omega $$-regular DTMC properties. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV 2012), pp. 169\u2013180. Verlag Dr. Kova\u010d (2012)"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-28756-5_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Wimmer","year":"2012","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Becker, B., Katoen, J.-P.: Minimal critical subsystems for discrete-time Markov models. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 299\u2013314. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_21"},{"key":"8_CR30","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.tcs.2014.06.020","volume":"549","author":"R Wimmer","year":"2014","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Katoen, J.P., Becker, B.: Minimal counterexamples for linear-time probabilistic verification. Theoret. Comput. Sci. 549, 61\u2013100 (2014)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-40196-1_4","volume-title":"Quantitative Evaluation of Systems","author":"R Wimmer","year":"2013","unstructured":"Wimmer, R., Jansen, N., Vorpahl, A., \u00c1brah\u00e1m, E., Katoen, J.-P., Becker, B.: High-level counterexamples for probabilistic automata. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 39\u201354. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40196-1_4"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Jansen, N., Vorpahl, A., \u00c1brah\u00e1m, E., Katoen, J., Becker, B.: High-level counterexamples for probabilistic automata. Log. Methods Comput. Sci. 11(1) (2015)","DOI":"10.2168\/LMCS-11(1:15)2015"}],"container-title":["Lecture Notes in Computer Science","Principles of Formal Quantitative Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-97439-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T13:24:07Z","timestamp":1757424247000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-97439-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,30]]},"ISBN":["9783031974380","9783031974397"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-97439-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,8,30]]},"assertion":[{"value":"30 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}