{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:01:49Z","timestamp":1779087709538,"version":"3.51.4"},"reference-count":73,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,8,19]],"date-time":"2025-08-19T00:00:00Z","timestamp":1755561600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,8,19]],"date-time":"2025-08-19T00:00:00Z","timestamp":1755561600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100014690","name":"Ministerium f\u00fcr Kultur und Wissenschaft des Landes Nordrhein-Westfalen","doi-asserted-by":"publisher","award":["KI-Starter Project \"Verifying AI Systems under Partial Observability\""],"award-info":[{"award-number":["KI-Starter Project \"Verifying AI Systems under Partial Observability\""]}],"id":[{"id":"10.13039\/501100014690","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["RTG 2236 \"UnRAVeL\""],"award-info":[{"award-number":["RTG 2236 \"UnRAVeL\""]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100007210","name":"RWTH Aachen University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100007210","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We study the accurate and efficient computation of the expected number of times each state is visited in discrete- and continuous-time Markov chains. To obtain sound accuracy guarantees efficiently, we lift interval iteration, optimistic value iteration and topological approaches developed to compute reachability probabilities and expected rewards and prove all these algorithms to be correct. We further establish that expected visiting times are preserved under backward probabilistic bisimilarity. We study various applications of expected visiting times. The reachability probabilities of multiple bottom strongly connected components (BSCCs) can be obtained by solving a single linear equation system\u2014as opposed to solving an equation system per BSCC. Other applications include the sound computation of the stationary distribution as well as expected rewards conditioned on reaching multiple goal states. The implementation of our methods in the probabilistic model checker Storm scales to large systems with millions of states. Our experiments on the quantitative verification benchmark set show that the computation of stationary distributions via expected visiting times consistently outperforms existing approaches\u2014sometimes by several orders of magnitude.<\/jats:p>","DOI":"10.1007\/s10817-025-09736-7","type":"journal-article","created":{"date-parts":[[2025,8,19]],"date-time":"2025-08-19T09:01:18Z","timestamp":1755594078000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate"],"prefix":"10.1007","volume":"69","author":[{"given":"Hannah","family":"Mertens","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"Quatmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Winkler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,19]]},"reference":[{"key":"9736_CR1","doi-asserted-by":"crossref","unstructured":"Amparore, E. G., Balbo, G., Beccuti, M., et\u00a0al. 30 years of GreatSPN. In: Principles of Performance and Reliability Modeling and Evaluation. Springer, p 227\u2013254 (2016)","DOI":"10.1007\/978-3-319-30599-8_9"},{"key":"9736_CR2","doi-asserted-by":"publisher","unstructured":"Bacci, G., Bacci, G., Larsen, K.G., et al.: On the metric-based approximate minimization of Markov chains. J Log Algebraic Methods Program 100, 36\u201356 (2018). https:\/\/doi.org\/10.1016\/J.JLAMP.2018.05.006","DOI":"10.1016\/J.JLAMP.2018.05.006"},{"key":"9736_CR3","doi-asserted-by":"publisher","unstructured":"Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Larsen, K. G., et\u00a0al. Active learning of Markov decision processes using Baum-Welch algorithm. In: ICMLA. IEEE, pp 1203\u20131208, (2021). https:\/\/doi.org\/10.1109\/ICMLA52953.2021.00195","DOI":"10.1109\/ICMLA52953.2021.00195"},{"key":"9736_CR4","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"issue":"6","key":"9736_CR5","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., et al.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng. 29(6), 524\u2013541 (2003). https:\/\/doi.org\/10.1109\/TSE.2003.1205180","journal-title":"IEEE Trans. Software Eng."},{"key":"9736_CR6","doi-asserted-by":"publisher","unstructured":"Baier, C., Klein, J., Leuschner, L., et\u00a0al. Ensuring the reliability of your model checker: Interval iteration for Markov decision processes. In: CAV (1), Lecture Notes in Computer Science, vol 10426. Springer, pp 160\u2013180, (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"9736_CR7","doi-asserted-by":"publisher","unstructured":"Baier, C., Funke, F., Piribauer, J., et\u00a0al. On probability-raising causality in Markov decision processes. In: FoSSaCS, Lecture Notes in Computer Science, vol 13242. Springer, pp 40\u201360, (2022)https:\/\/doi.org\/10.1007\/978-3-030-99253-8_3","DOI":"10.1007\/978-3-030-99253-8_3"},{"issue":"5","key":"9736_CR8","first-page":"679","volume":"6","author":"R Bellman","year":"1957","unstructured":"Bellman, R.: A Markovian Decision Process. Journal of Mathematics and Mechanics 6(5), 679\u2013684 (1957)","journal-title":"Journal of Mathematics and Mechanics"},{"key":"9736_CR9","doi-asserted-by":"publisher","unstructured":"Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval Markov chains. In: TACAS, Lecture Notes in Computer Science, vol 7795. Springer, pp 32\u201346, (2013https:\/\/doi.org\/10.1007\/978-3-642-36742-7_3","DOI":"10.1007\/978-3-642-36742-7_3"},{"issue":"3","key":"9736_CR10","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1007\/S00224-019-09921-3","volume":"64","author":"M Bressan","year":"2020","unstructured":"Bressan, M., Peserico, E., Pretto, L.: On approximating the stationary distribution of time-reversible Markov chains. Theory Comput Syst 64(3), 444\u2013466 (2020). https:\/\/doi.org\/10.1007\/S00224-019-09921-3","journal-title":"Theory Comput Syst"},{"issue":"1\u20132","key":"9736_CR11","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/S0304-3975(98)00169-8","volume":"215","author":"P Buchholz","year":"1999","unstructured":"Buchholz, P.: Exact performance equivalence: An equivalence relation for stochastic automata. Theor. Comput. Sci. 215(1\u20132), 263\u2013287 (1999). https:\/\/doi.org\/10.1016\/S0304-3975(98)00169-8","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"9736_CR12","doi-asserted-by":"publisher","first-page":"1031","DOI":"10.1002\/NLA.824","volume":"18","author":"A Busic","year":"2011","unstructured":"Busic, A., Fourneau, J.: Iterative component-wise bounds for the steady-state distribution of a Markov chain. Numer Linear Algebra Appl 18(6), 1031\u20131049 (2011). https:\/\/doi.org\/10.1002\/NLA.824","journal-title":"Numer Linear Algebra Appl"},{"issue":"1","key":"9736_CR13","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/S11047-017-9667-5","volume":"17","author":"L Cardelli","year":"2018","unstructured":"Cardelli, L., Kwiatkowska, M., Laurenti, L.: Programming discrete distributions with chemical reaction networks. Nat. Comput. 17(1), 131\u2013145 (2018). https:\/\/doi.org\/10.1007\/S11047-017-9667-5","journal-title":"Nat. Comput."},{"key":"9736_CR14","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Majumdar, R., Henzinger, T. A.: Markov decision processes with multiple objectives. In: STACS, Lecture Notes in Computer Science, vol 3884. Springer, pp 325\u2013336, (2006). https:\/\/doi.org\/10.1007\/11672142_26","DOI":"10.1007\/11672142_26"},{"key":"9736_CR15","doi-asserted-by":"publisher","unstructured":"Ciesinski, F., Baier, C., Gr\u00f6\u00dfer, M., et\u00a0al. Reduction techniques for model checking Markov decision processes. In: QEST. IEEE Computer Society, pp 45\u201354, (2008)https:\/\/doi.org\/10.1109\/QEST.2008.45","DOI":"10.1109\/QEST.2008.45"},{"key":"9736_CR16","unstructured":"Dai, P., Goldsmith, J.: Topological value iteration algorithm for Markov decision processes. In: IJCAI, pp 1860\u20131865 (2007)"},{"key":"9736_CR17","first-page":"181","volume":"42","author":"P Dai","year":"2011","unstructured":"Dai, P., Mausam, W.D.S., et al.: Topological value iteration algorithms. J Artif Intell Res 42, 181\u2013209 (2011)","journal-title":"J Artif Intell Res"},{"key":"9736_CR18","doi-asserted-by":"publisher","unstructured":"Delgrange, F., Katoen, J., Quatmann, T., et\u00a0al. Simple Strategies in Multi-Objective MDPs. In: TACAS (1), Lecture Notes in Computer Science, vol 12078. Springer, pp 346\u2013364, (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_19","DOI":"10.1007\/978-3-030-45190-5_19"},{"key":"9736_CR19","doi-asserted-by":"publisher","unstructured":"Etessami, K., Kwiatkowska, M. Z., Vardi, M. Y., et\u00a0al. Multi-objective model checking of Markov decision processes. Log Methods Comput Sci 4(4), (2008)https:\/\/doi.org\/10.2168\/LMCS-4(4:8)2008","DOI":"10.2168\/LMCS-4(4:8)2008"},{"issue":"1","key":"9736_CR20","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1109\/TR.2013.2241131","volume":"62","author":"L Fiondella","year":"2013","unstructured":"Fiondella, L., Rajasekaran, S., Gokhale, S.S.: Efficient software reliability analysis with correlated component failures. IEEE Trans. Reliab. 62(1), 244\u2013255 (2013). https:\/\/doi.org\/10.1109\/TR.2013.2241131","journal-title":"IEEE Trans. Reliab."},{"key":"9736_CR21","doi-asserted-by":"publisher","unstructured":"Forejt, V., Kwiatkowska, M. Z., Norman, G., et\u00a0al. Quantitative multi-objective verification for probabilistic systems. In: TACAS, Lecture Notes in Computer Science, vol 6605. Springer, pp 112\u2013127, (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11","DOI":"10.1007\/978-3-642-19835-9_11"},{"key":"9736_CR22","doi-asserted-by":"publisher","unstructured":"Fourneau, J., Quessette, F.: Some improvements for the computation of the steady-state distribution of a Markov chain by monotone sequences of vectors. In: ASMTA, Lecture Notes in Computer Science, vol 7314. Springer, pp 178\u2013192, (2012)https:\/\/doi.org\/10.1007\/978-3-642-30782-9_13","DOI":"10.1007\/978-3-642-30782-9_13"},{"key":"9736_CR23","doi-asserted-by":"publisher","unstructured":"Funke, F., Jantsch, S., Baier, C.: Farkas certificates and minimal witnesses for probabilistic reachability constraints. In: TACAS (1), Lecture Notes in Computer Science, vol 12078. Springer, pp 324\u2013345, (2020)https:\/\/doi.org\/10.1007\/978-3-030-45190-5_18","DOI":"10.1007\/978-3-030-45190-5_18"},{"key":"9736_CR24","doi-asserted-by":"publisher","unstructured":"Gadot, U., Derman, E., Kumar, N., et\u00a0al. Solving non-rectangular reward-robust MDPs via frequency regularization. In: AAAI. AAAI Press, pp 21090\u201321098, (2024)https:\/\/doi.org\/10.1609\/AAAI.V38I19.30101","DOI":"10.1609\/AAAI.V38I19.30101"},{"key":"9736_CR25","doi-asserted-by":"publisher","unstructured":"Gokhale, S. S., Trivedi, K. S.: Reliability prediction and sensitivity analysis based on software architecture. In: ISSRE. IEEE Computer Society, pp 64\u201378, (2002). https:\/\/doi.org\/10.1109\/ISSRE.2002.1173214","DOI":"10.1109\/ISSRE.2002.1173214"},{"issue":"4","key":"9736_CR26","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1016\/J.PEVA.2004.04.003","volume":"58","author":"SS Gokhale","year":"2004","unstructured":"Gokhale, S.S., Wong, W.E., Horgan, J.R., et al.: An analytical approach to architecture-based software performance and reliability prediction. Perform Evaluation 58(4), 391\u2013412 (2004). https:\/\/doi.org\/10.1016\/J.PEVA.2004.04.003","journal-title":"Perform Evaluation"},{"key":"9736_CR27","unstructured":"Granlund, T.: the GMP\u00a0development team (2024) The GNU multiple precision arithmetic library. https:\/\/gmplib.org"},{"key":"9736_CR28","unstructured":"Guennebaud, G., Jacob, B.: Eigen v3. (2010). http:\/\/eigen.tuxfamily.org"},{"key":"9736_CR29","doi-asserted-by":"publisher","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: Refining convergence of value iteration. In: RP, Lecture Notes in Computer Science, vol 8762. Springer, pp 125\u2013137, (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_10","DOI":"10.1007\/978-3-319-11439-2_10"},{"key":"9736_CR30","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). https:\/\/doi.org\/10.1016\/J.TCS.2016.12.003","journal-title":"Theor. Comput. Sci."},{"key":"9736_CR31","doi-asserted-by":"publisher","unstructured":"Hartmanns, A.: Correct probabilistic model checking with floating-point arithmetic. In: TACAS (2), Lecture Notes in Computer Science, vol 13244. Springer, pp 41\u201359, (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_3","DOI":"10.1007\/978-3-030-99527-0_3"},{"key":"9736_CR32","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: The modest toolset: An integrated environment for quantitative modelling and verification. In: TACAS, Lecture Notes in Computer Science, vol 8413. Springer, pp 593\u2013598, (2014)https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"9736_CR33","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Kaminski, B. L.: Optimistic value iteration. In: CAV (2), Lecture Notes in Computer Science, vol 12225. Springer, pp 488\u2013511, (2020)https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26","DOI":"10.1007\/978-3-030-53291-8_26"},{"key":"9736_CR34","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Klauck, M., Parker, D., et\u00a0al. The quantitative verification benchmark set. In: TACAS (1), Lecture Notes in Computer Science, vol 11427. Springer, pp 344\u2013350, (2019)https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20","DOI":"10.1007\/978-3-030-17462-0_20"},{"issue":"4","key":"9736_CR35","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., et al.: 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","journal-title":"Int J Softw Tools Technol Transf"},{"key":"9736_CR36","doi-asserted-by":"publisher","unstructured":"Horn, R.A., Johnson, C.R.: Matrix Analysis, 2nd edn. Cambridge University Press, Xx (2012). https:\/\/doi.org\/10.1017\/CBO9781139020411","DOI":"10.1017\/CBO9781139020411"},{"key":"9736_CR37","doi-asserted-by":"publisher","unstructured":"Junges, S., Spaan, M. T. J.: Abstraction-refinement for hierarchical probabilistic models. In: CAV (1), Lecture Notes in Computer Science, vol 13371. Springer, pp 102\u2013123, (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_6","DOI":"10.1007\/978-3-031-13185-1_6"},{"key":"9736_CR38","doi-asserted-by":"publisher","unstructured":"Katoen, J.: The probabilistic model checking landscape. In: LICS. ACM, pp 31\u201345, (2016)https:\/\/doi.org\/10.1145\/2933575.2934574","DOI":"10.1145\/2933575.2934574"},{"issue":"2","key":"9736_CR39","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/175007.175019","volume":"4","author":"MS Keane","year":"1994","unstructured":"Keane, M.S., O\u2019Brien, G.L.: A bernoulli factory. ACM Trans. Model. Comput. Simul. 4(2), 213\u2013219 (1994)","journal-title":"ACM Trans. Model. Comput. Simul."},{"key":"9736_CR40","unstructured":"Kemeny, J., Snell, J.: Finite Markov Chains. Undergraduate texts in mathematics. Springer (1976)"},{"issue":"1","key":"9736_CR41","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1137\/1106012","volume":"6","author":"JG Kemeny","year":"1961","unstructured":"Kemeny, J.G., Snell, J.L.: Finite continuous time Markov chains. Theory of Probability & Its Applications 6(1), 101\u2013105 (1961). https:\/\/doi.org\/10.1137\/1106012","journal-title":"Theory of Probability & Its Applications"},{"key":"9736_CR42","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Of cores: A partial-exploration framework for Markov decision processes. In: CONCUR, LIPIcs, vol 140. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, pp 5:1\u20135:17, (2019). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2019.5","DOI":"10.4230\/LIPICS.CONCUR.2019.5"},{"key":"9736_CR43","doi-asserted-by":"publisher","unstructured":"Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman & Hall\/CRC Texts in Statistical Science, CRC Press, (2016). https:\/\/doi.org\/10.1201\/9781315367910","DOI":"10.1201\/9781315367910"},{"key":"9736_CR44","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M. Z., Norman, G., Parker, D.: Stochastic model checking. In: SFM, Lecture Notes in Computer Science, vol 4486. Springer, pp 220\u2013270, (2007). https:\/\/doi.org\/10.1007\/978-3-540-72522-0_6","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"9736_CR45","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M. Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: CAV, Lecture Notes in Computer Science, vol 6806. Springer, pp 585\u2013591, (2011)https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"issue":"1","key":"9736_CR46","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"KG Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1\u201328 (1991). https:\/\/doi.org\/10.1016\/0890-5401(91)90030-6","journal-title":"Inf. Comput."},{"key":"9736_CR47","unstructured":"Lumbroso, J. O.: Optimal discrete uniform generation from coin flips, and applications. (2013) CoRR abs\/1304.1916"},{"key":"9736_CR48","doi-asserted-by":"publisher","unstructured":"McMahan, H. B., Likhachev, M., Gordon, G. J.: Bounded real-time dynamic programming: RTDP with monotone upper bounds and performance guarantees. In: ICML, ACM International Conference Proceeding Series, vol 119. ACM, pp 569\u2013576, (2005). https:\/\/doi.org\/10.1145\/1102351.1102423","DOI":"10.1145\/1102351.1102423"},{"key":"9736_CR49","doi-asserted-by":"publisher","unstructured":"Meedeniya, I., Moser, I., Aleti, A., et\u00a0al. Architecture-based reliability evaluation under uncertainty. In: QoSA\/ISARCS. ACM, pp 85\u201394, (2011). https:\/\/doi.org\/10.1145\/2000259.2000275","DOI":"10.1145\/2000259.2000275"},{"key":"9736_CR50","doi-asserted-by":"publisher","unstructured":"Meggendorfer, T.: Correct approximation of stationary distributions. In: TACAS (1), Lecture Notes in Computer Science, vol 13993. Springer, pp 489\u2013507, (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_25","DOI":"10.1007\/978-3-031-30823-9_25"},{"key":"9736_CR51","doi-asserted-by":"publisher","unstructured":"Mertens, H., Katoen, J., Quatmann, T., et\u00a0al. Accurately computing expected visiting times and stationary distributions in Markov chains. In: TACAS (2), Lecture Notes in Computer Science, vol 14571. Springer, pp 237\u2013257, (2024a)https:\/\/doi.org\/10.1007\/978-3-031-57249-4_12","DOI":"10.1007\/978-3-031-57249-4_12"},{"key":"9736_CR52","doi-asserted-by":"publisher","unstructured":"Mertens, H., Katoen, J. P., Quatmann, T., et\u00a0al. Accurately computing expected visiting times and stationary distributions in Markov chains. (2024b)https:\/\/doi.org\/10.48550\/arXiv.2401.10638, arXiv:2401.10638","DOI":"10.48550\/arXiv.2401.10638"},{"key":"9736_CR53","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.13919107","author":"H Mertens","year":"2024","unstructured":"Mertens, H., Quatmann, T., Katoen, J.P., et al.: Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate (Artifact). (2024). https:\/\/doi.org\/10.5281\/zenodo.13919107","journal-title":"Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate (Artifact)."},{"key":"9736_CR54","unstructured":"Neumann, C.: Untersuchungen \u00fcber das logarithmische und Newton\u2019sche Potential. BG Teubner, (1877)"},{"key":"9736_CR55","unstructured":"Park, D.: Fixpoint induction and proofs of program properties. Machine Intelligence 5, (1969)"},{"key":"9736_CR56","doi-asserted-by":"publisher","unstructured":"Pietrantuono, R., Russo, S., Trivedi, K. S.: Online monitoring of software system reliability. In: EDCC. IEEE Computer Society, pp 209\u2013218, (2010). https:\/\/doi.org\/10.1109\/EDCC.2010.33","DOI":"10.1109\/EDCC.2010.33"},{"key":"9736_CR57","doi-asserted-by":"publisher","first-page":"69","DOI":"10.2307\/1425817","volume":"9","author":"J Pitman","year":"1977","unstructured":"Pitman, J.: Occupation measures for Markov chains. Adv. Appl. Probab. 9, 69\u201386 (1977). https:\/\/doi.org\/10.2307\/1425817","journal-title":"Adv. Appl. Probab."},{"issue":"1","key":"9736_CR58","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1137\/23M1572398","volume":"62","author":"AB Piunovskiy","year":"2024","unstructured":"Piunovskiy, A.B., Zhang, Y.: Extreme occupation measures in Markov decision processes with an absorbing state. SIAM J. Control. Optim. 62(1), 65\u201390 (2024). https:\/\/doi.org\/10.1137\/23M1572398","journal-title":"SIAM J. Control. Optim."},{"key":"9736_CR59","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":"9736_CR60","doi-asserted-by":"publisher","unstructured":"Quatmann, T., Katoen, J.: Sound value iteration. In: CAV (1), Lecture Notes in Computer Science, vol 10981. Springer, pp 643\u2013661, (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"9736_CR61","unstructured":"Renard, Y.: Gmm++. (2024). https:\/\/getfem.org\/gmm.html"},{"key":"9736_CR62","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898718003","author":"Y Saad","year":"2003","unstructured":"Saad, Y.: Iterative Methods for Sparse Linear Systems. SIAM (2003). https:\/\/doi.org\/10.1137\/1.9780898718003","journal-title":"SIAM"},{"key":"9736_CR63","doi-asserted-by":"publisher","unstructured":"Salmani, B., Katoen, J.: Bayesian inference by symbolic model checking. In: QEST, Lecture Notes in Computer Science, vol 12289. Springer, pp 115\u2013133, (2020). https:\/\/doi.org\/10.1007\/978-3-030-59854-9_9","DOI":"10.1007\/978-3-030-59854-9_9"},{"key":"9736_CR64","doi-asserted-by":"publisher","unstructured":"Salmani, B., Katoen, J.: Fine-tuning the odds in bayesian networks. In: ECSQARU, Lecture Notes in Computer Science, vol 12897. Springer, pp 268\u2013283, (2021)https:\/\/doi.org\/10.1007\/978-3-030-86772-0_20","DOI":"10.1007\/978-3-030-86772-0_20"},{"key":"9736_CR65","doi-asserted-by":"publisher","unstructured":"Sharma, V. S., Trivedi, K. S.: Reliability and performance of component based software systems with restarts, retries, reboots and repairs. In: ISSRE. IEEE Computer Society, pp 299\u2013310, (2006)https:\/\/doi.org\/10.1109\/ISSRE.2006.39","DOI":"10.1109\/ISSRE.2006.39"},{"key":"9736_CR66","doi-asserted-by":"publisher","unstructured":"Smolka, S., Kumar, P., Kahn, D. M., et\u00a0al. Scalable verification of probabilistic networks. In: PLDI. ACM, pp 190\u2013203, (2019). https:\/\/doi.org\/10.1145\/3314221.3314639","DOI":"10.1145\/3314221.3314639"},{"issue":"8","key":"9736_CR67","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1109\/TSE.2006.74","volume":"32","author":"J Sproston","year":"2006","unstructured":"Sproston, J., Donatelli, S.: Backward bisimulation in Markov chain model checking. IEEE Trans. Software Eng. 32(8), 531\u2013546 (2006). https:\/\/doi.org\/10.1109\/TSE.2006.74","journal-title":"IEEE Trans. Software Eng."},{"issue":"2","key":"9736_CR68","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"RE Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972). https:\/\/doi.org\/10.1137\/0201010","journal-title":"SIAM J. Comput."},{"key":"9736_CR69","doi-asserted-by":"publisher","DOI":"10.1002\/047001363X","author":"HC Tijms","year":"2003","unstructured":"Tijms, H.C.: A First Course in Stochastic Models. Wiley (2003). https:\/\/doi.org\/10.1002\/047001363X","journal-title":"Wiley"},{"key":"9736_CR70","volume-title":"Matrix Iterative Analysis","author":"RS Varga","year":"1999","unstructured":"Varga, R.S.: Matrix Iterative Analysis. Springer Series in Computational Mathematics. Springer, Berlin Heidelberg (1999)"},{"issue":"3","key":"9736_CR71","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1198\/TECH.2005.S293","volume":"47","author":"CA Volino","year":"2005","unstructured":"Volino, C.A.: A first course in stochastic models. Technometrics 47(3), 375 (2005). https:\/\/doi.org\/10.1198\/TECH.2005.S293","journal-title":"Technometrics"},{"key":"9736_CR72","doi-asserted-by":"publisher","unstructured":"Wimmer, R., Kortus, A., Herbstritt, M., et\u00a0al. Probabilistic model checking and reliability of results. In: DDECS. IEEE Computer Society, pp 207\u2013212, (2008). https:\/\/doi.org\/10.1109\/DDECS.2008.4538787","DOI":"10.1109\/DDECS.2008.4538787"},{"key":"9736_CR73","unstructured":"Zilken, D.: Distributional invariants for probabilistic program. Master\u2019s thesis, RWTH Aachen University, (2024)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09736-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09736-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09736-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T22:02:23Z","timestamp":1758664943000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09736-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,19]]},"references-count":73,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["9736"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09736-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,19]]},"assertion":[{"value":"13 October 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 July 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 August 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"23"}}