{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T19:32:20Z","timestamp":1757619140871,"version":"3.44.0"},"publisher-location":"Cham","reference-count":64,"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>We introduce <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$(\\varepsilon , \\delta )$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mo>(<\/mml:mo>\n                    <mml:mi>\u03b5<\/mml:mi>\n                    <mml:mo>,<\/mml:mo>\n                    <mml:mi>\u03b4<\/mml:mi>\n                    <mml:mo>)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$(\\varepsilon , \\delta )$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mo>(<\/mml:mo>\n                    <mml:mi>\u03b5<\/mml:mi>\n                    <mml:mo>,<\/mml:mo>\n                    <mml:mi>\u03b4<\/mml:mi>\n                    <mml:mo>)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-bisimulation allows the use of different tolerances for the transition probabilities (<jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\varepsilon $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03b5<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>, additive) and total exit rates (<jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\delta $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03b4<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>, multiplicative) of states. Fundamental properties of the notion, as well as bounds on the absolute difference of time- and reward-bounded reachability probabilities for <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$(\\varepsilon ,\\delta )$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mo>(<\/mml:mo>\n                    <mml:mi>\u03b5<\/mml:mi>\n                    <mml:mo>,<\/mml:mo>\n                    <mml:mi>\u03b4<\/mml:mi>\n                    <mml:mo>)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-bisimilar states, are established.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_3","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:18:42Z","timestamp":1753089522000},"page":"56-81","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Approximate Probabilistic Bisimulation for\u00a0Continuous-Time Markov Chains"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-4461-0667","authenticated-orcid":false,"given":"Timm","family":"Spork","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5321-9343","authenticated-orcid":false,"given":"Christel","family":"Baier","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1724-2586","authenticated-orcid":false,"given":"Sascha","family":"Kl\u00fcppelholz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4829-0476","authenticated-orcid":false,"given":"Jakob","family":"Piribauer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Abate, A.: Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey. In: Proceedings of the First Workshop on Hybrid Autonomous Systems. Electronic Notes in Theoretical Computer Science, vol. 297, pp. 3\u201325 (2013). https:\/\/doi.org\/10.1016\/j.entcs.2013.12.002","DOI":"10.1016\/j.entcs.2013.12.002"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Abate, A., Brim, L., \u010ce\u0161ka, M., Kwiatkowska, M.: Adaptive aggregation of Markov chains: quantitative analysis of chemical reaction networks. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification. Lecture Notes in Computer Science (LNCS), vol.\u00a09206, pp. 195\u2013213. Springer International Publishing, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_12","DOI":"10.1007\/978-3-319-21690-4_12"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Abate, A., Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking of labelled Markov processes via finite approximate bisimulations. In: van Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J. (eds.) Horizons of the Mind. A Tribute to Prakash Panangaden: Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday, Lecture Notes in Computer Science (LNCS), vol.\u00a08464, pp. 40\u201358. Springer International Publishing, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06880-0_2","DOI":"10.1007\/978-3-319-06880-0_2"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"\u010ce\u0161ka, M., \u0160afr\u00e1nek, D., Dra\u017ean, S., Brim, L.: Robustness analysis of stochastic biochemical systems. PLoS ONE 9(4), e94553 (2014). https:\/\/doi.org\/10.1371\/journal.pone.0094553","DOI":"10.1371\/journal.pone.0094553"},{"key":"3_CR5","unstructured":"Aldini, A.: A Note on the Approximation of Weak Probabilistic Bisimulation (2009)"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Amparore, E.G., Beccuti, M., Donatelli, S.: (Stochastic) model checking in GreatSPN. In: Petri Nets. Lecture Notes in Computer Science (LNCS), vol.\u00a08489, pp. 354\u2013363. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-07734-5_19","DOI":"10.1007\/978-3-319-07734-5_19"},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.peva.2018.03.002","volume":"123\u2013124","author":"EG Amparore","year":"2018","unstructured":"Amparore, E.G., Donatelli, S.: Efficient model checking of the stochastic logic CSL$$ ^{\\text{ TA }}$$. Perform. Eval. 123\u2013124, 1\u201334 (2018). https:\/\/doi.org\/10.1016\/j.peva.2018.03.002","journal-title":"Perform. Eval."},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Arnold, F., Belinfante, A., van\u00a0der Berg, F.I., Guck, D., Stoelinga, M.: DFTCalc: a tool for efficient fault tree analysis. In: SAFECOMP. Lecture Notes in Computer Science (LNCS), vol.\u00a08153, pp. 293\u2013301. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-40793-2_27","DOI":"10.1007\/978-3-642-40793-2_27"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic 1(1), 162\u2013170 (2000). https:\/\/doi.org\/10.1145\/343369.343402","DOI":"10.1145\/343369.343402"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Baier, C.: Polynomial time algorithms for testing probabilistic bisimulation and simulation. In: Alur, R., Henzinger, T.A. (eds.) Computer Aided Verification. Lecture Notes in Computer Science (LNCS), vol.\u00a01102, pp. 50\u201361. Springer, Berlin, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_57","DOI":"10.1007\/3-540-61474-5_57"},{"issue":"4","key":"3_CR11","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1109\/TSE.2007.36","volume":"33","author":"C Baier","year":"2007","unstructured":"Baier, C., Cloth, L., Haverkort, B.R., Kuntz, M., Siegle, M.: Model checking Markov chains with actions and state labels. IEEE Trans. Software Eng. 33(4), 209\u2013224 (2007). https:\/\/doi.org\/10.1109\/TSE.2007.36","journal-title":"IEEE Trans. Software Eng."},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: On the logical characterisation of performability properties. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds.) Automata, Languages and Programming (ICALP 2000). Lecture Notes in Computer Science (LNCS), vol.\u00a01853, pp. 780\u2013792. Springer Berlin Heidelberg, Berlin, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-45022-X_65","DOI":"10.1007\/3-540-45022-X_65"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013 541 (2003). https:\/\/doi.org\/10.1109\/TSE.2003.1205180","DOI":"10.1109\/TSE.2003.1205180"},{"key":"3_CR14","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)"},{"issue":"2","key":"3_CR15","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.ic.2005.03.001","volume":"200","author":"C Baier","year":"2005","unstructured":"Baier, C., Katoen, J.P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Inf. Comput. 200(2), 149\u2013214 (2005). https:\/\/doi.org\/10.1016\/j.ic.2005.03.001","journal-title":"Inf. Comput."},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Bartoletti, M., Murgia, M., Zunino, R.: Sound approximate and asymptotic probabilistic bisimulations for PCTL. Log. Meth. Comput. Sci. 19(1) (2023). https:\/\/doi.org\/10.46298\/lmcs-19(1:22)2023","DOI":"10.46298\/lmcs-19(1:22)2023"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Beaudry, M.D.: Performance-related reliability measures for computing systems. IEEE Trans. Comput. C-27(6), 540\u2013547 (1978). https:\/\/doi.org\/10.1109\/TC.1978.1675145","DOI":"10.1109\/TC.1978.1675145"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Bian, G., Abate, A.: On the relationship between bisimulation and trace equivalence in an approximate probabilistic context. In: Esparza, J., Murawski, A.S. (eds.) Foundations of Software Science and Computation Structures (FoSSaCS). Lecture Notes in Computer Science (LNCS), vol. 10203, pp. 321\u2013337. Springer, Berlin, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54458-7_19","DOI":"10.1007\/978-3-662-54458-7_19"},{"issue":"1","key":"3_CR19","doi-asserted-by":"publisher","first-page":"59","DOI":"10.2307\/3215235","volume":"31","author":"P Buchholz","year":"1994","unstructured":"Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. J. Appl. Probab. 31(1), 59\u201375 (1994). https:\/\/doi.org\/10.2307\/3215235","journal-title":"J. Appl. Probab."},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Cardelli, L., Grosu, R., Larsen, K.G., Tribastone, M., Tschaikowski, M., Vandin, A.: Lumpability for uncertain continuous-time Markov chains. In: Abate, A., Marin, A. (eds.) Quantitative Evaluation of Systems (QEST 2021), Lecture Notes in Computer Science (LNCS), vol. 12846, pp. 391\u2013409. Springer International Publishing, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85172-9_21","DOI":"10.1007\/978-3-030-85172-9_21"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Cardelli, L., Grosu, R., Larsen, K.G., Tribastone, M., Tschaikowski, M., Vandin, A.: Algorithmic minimization of uncertain continuous-time markov chains. IEEE Trans. Autom. Control 68(11), 6557\u20136572 (2023). https:\/\/doi.org\/10.1109\/TAC.2023.3244093","DOI":"10.1109\/TAC.2023.3244093"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"Chen, T., Han, T., Katoen, J.P., Mereacre, A.: Quantitative model checking of continuous-time Markov chains against timed automata specifications. In: 24th IEEE Symposium on Logic In Computer Science (LICS), pp. 309\u2013318. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/LICS.2009.21","DOI":"10.1109\/LICS.2009.21"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Desharnais, J., Edalat, A., Panangaden, P.: A logical characterization of bisimulation for labeled Markov processes. In: Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LiCS), pp. 478\u2013487 (1998). https:\/\/doi.org\/10.1109\/LICS.1998.705681","DOI":"10.1109\/LICS.1998.705681"},{"issue":"2","key":"3_CR24","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1006\/inco.2001.2962","volume":"179","author":"J Desharnais","year":"2002","unstructured":"Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Inf. Comput. 179(2), 163\u2013193 (2002). https:\/\/doi.org\/10.1006\/inco.2001.2962","journal-title":"Inf. Comput."},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: logic, simulation and games. In: Fifth International Conference on Quantitative Evaluation of Systems (QEST 2008), pp. 264\u2013273 (2008). https:\/\/doi.org\/10.1109\/QEST.2008.42","DOI":"10.1109\/QEST.2008.42"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Dey, P., Kannan, R., Ryder, N., Srivastava, N.: Bit complexity of Jordan normal form and polynomial spectral factorization. In: Tauman\u00a0Kalai, Y. (ed.) 14th Innovations in Theoretical Computer Science Conference (ITCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0251, pp. 42:1\u201342:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ITCS.2023.42","DOI":"10.4230\/LIPIcs.ITCS.2023.42"},{"key":"3_CR27","doi-asserted-by":"publisher","unstructured":"D\u2019Innocenzo, A., Abate, A., Katoen, J.P.: Robust PCTL model checking. In: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2012), pp. 275\u2013286. Association for Computing Machinery, New York, NY, USA (2012). https:\/\/doi.org\/10.1145\/2185632.2185673","DOI":"10.1145\/2185632.2185673"},{"key":"3_CR28","unstructured":"Erlang, A.K.: Solution to some problems of the theory of probabilities of significance in automatic telephone exchange. Post Office Electric. Eng. J., 189\u2013197 (1917)"},{"issue":"1","key":"3_CR29","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0166-5316(94)90015-9","volume":"20","author":"G Franceschinis","year":"1994","unstructured":"Franceschinis, G., Muntz, R.R.: Bounds for quasi-lumpable Markov chains. Perform. Eval. 20(1), 223\u2013243 (1994). https:\/\/doi.org\/10.1016\/0166-5316(94)90015-9","journal-title":"Perform. Eval."},{"issue":"7","key":"3_CR30","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1109\/32.297940","volume":"20","author":"G Franceschinis","year":"1994","unstructured":"Franceschinis, G., Muntz, R.R.: Computing bounds for the performance indices of quasi-lumpable stochastic well-formed nets. IEEE Trans. Softw. Eng. 20(7), 516\u2013525 (1994). https:\/\/doi.org\/10.1109\/32.297940","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR31","doi-asserted-by":"publisher","unstructured":"Gouberman, A., Siegle, M.: Markov reward models and Markov decision processes in discrete and continuous time: performance evaluation and optimization. In: Remke, A., Stoelinga, M. (eds.) Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems: International Autumn School (ROCKS 2012). Lecture Notes in Computer Science (LNCS), vol.\u00a08453, pp. 156\u2013241. Springer Berlin Heidelberg, Berlin, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-45489-3_6","DOI":"10.1007\/978-3-662-45489-3_6"},{"issue":"1","key":"3_CR32","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0305-0548(77)90007-7","volume":"4","author":"WK Grassmann","year":"1977","unstructured":"Grassmann, W.K.: Transient solutions in Markovian queueing systems. Computers & Operations Research 4(1), 47\u201353 (1977). https:\/\/doi.org\/10.1016\/0305-0548(77)90007-7","journal-title":"Computers & Operations Research"},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"Haesaert, S., Nilsson, P., Soudjani, S.: Formal multi-objective synthesis of continuous-state MDPs. In: 2021 American Control Conference (ACC), pp. 3428\u20133433 (2021). https:\/\/doi.org\/10.23919\/ACC50511.2021.9482873","DOI":"10.23919\/ACC50511.2021.9482873"},{"key":"3_CR34","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. Trans. (STTT) 24, 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/s10009-021-00633-z","DOI":"10.1007\/s10009-021-00633-z"},{"issue":"sup1","key":"3_CR35","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1080\/03461238.1953.10419459","volume":"1953","author":"A Jensen","year":"1953","unstructured":"Jensen, A.: Markoff chains as an aid in the study of Markoff processes. Scand. Actuar. J. 1953(sup1), 87\u201391 (1953). https:\/\/doi.org\/10.1080\/03461238.1953.10419459","journal-title":"Scand. Actuar. J."},{"key":"3_CR36","volume-title":"Finite Markov Chains","author":"JG Kemeny","year":"1976","unstructured":"Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Undergraduate Texts in Mathematics (UTM), Springer, New York (1976)"},{"key":"3_CR37","doi-asserted-by":"publisher","unstructured":"Kiefer, S., Tang, Q.: Approximate bisimulation minimisation. In: Boja\u0144czy, M., Chekuri, C. (eds.) 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0213, pp. 48:1\u201348:16. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2021.48","DOI":"10.4230\/LIPIcs.FSTTCS.2021.48"},{"key":"3_CR38","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/BF01457949","volume":"104","author":"AN Kolmogorov","year":"1931","unstructured":"Kolmogorov, A.N.: \u00dcber die analytischen methoden in der wahrscheinlichkeitsrechnung. Math. Ann. 104, 415\u2013458 (1931). https:\/\/doi.org\/10.1007\/BF01457949","journal-title":"Math. Ann."},{"key":"3_CR39","doi-asserted-by":"publisher","unstructured":"Kulkarni, V.G.: Introduction to Modeling and Analysis of Stochastic Systems. Springer Texts in Statistics (STS), Springer New York (2010). https:\/\/doi.org\/10.1007\/978-1-4419-1772-0","DOI":"10.1007\/978-1-4419-1772-0"},{"key":"3_CR40","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proc. 23rd International Conference on Computer Aided Verification (CAV\u201911). Lecture Notes in Computer Science (LNCS), vol.\u00a06806, pp. 585\u2013591. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"3_CR41","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Thachuk, C.: Probabilistic model checking for biology. In: Software Systems Safety, NATO Science for Peace and Security Series, D: Information and Communication Security, vol.\u00a036, pp. 165\u2013189. IOS Press (2014). https:\/\/doi.org\/10.3233\/978-1-61499-385-8-165","DOI":"10.3233\/978-1-61499-385-8-165"},{"issue":"1","key":"3_CR42","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."},{"issue":"4","key":"3_CR43","doi-asserted-by":"publisher","first-page":"1278","DOI":"10.1017\/jpr.2024.20","volume":"61","author":"N Lin","year":"2024","unstructured":"Lin, N., Liu, Y.: Perturbation analysis for continuous-time Markov chains in a weak sense. J. Appl. Probab. 61(4), 1278\u20131300 (2024). https:\/\/doi.org\/10.1017\/jpr.2024.20","journal-title":"J. Appl. Probab."},{"issue":"12","key":"3_CR44","doi-asserted-by":"publisher","first-page":"2633","DOI":"10.1007\/s11425-015-5019-z","volume":"58","author":"YY Liu","year":"2015","unstructured":"Liu, Y.Y.: Perturbation analysis for continuous-time Markov chains. Sci. China Math. 58(12), 2633\u20132642 (2015). https:\/\/doi.org\/10.1007\/s11425-015-5019-z","journal-title":"Sci. China Math."},{"issue":"2","key":"3_CR45","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1017\/apr.2018.28","volume":"50","author":"Y Liu","year":"2018","unstructured":"Liu, Y., Li, W.: Error bounds for augmented truncation approximations of Markov chains via the perturbation method. Adv. Appl. Probab. 50(2), 645\u2013669 (2018). https:\/\/doi.org\/10.1017\/apr.2018.28","journal-title":"Adv. Appl. Probab."},{"key":"3_CR46","doi-asserted-by":"publisher","unstructured":"Madsen, C., Zhang, Z., Roehner, N., Winstead, C., Myers, C.J.: Stochastic model checking of genetic circuits. ACM J. Emerg. Technol. Comput. Syst. 11(3), 23:1\u201323:21 (2014). https:\/\/doi.org\/10.1145\/2644817","DOI":"10.1145\/2644817"},{"issue":"3","key":"3_CR47","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/0166-5316(87)90039-3","volume":"7","author":"RA Maire","year":"1987","unstructured":"Maire, R.A., Reibman, A.L., Trivedi, K.S.: Transient analysis of acyclic Markov chains. Perform. Eval. 7(3), 175\u2013194 (1987). https:\/\/doi.org\/10.1016\/0166-5316(87)90039-3","journal-title":"Perform. Eval."},{"key":"3_CR48","doi-asserted-by":"publisher","unstructured":"Marin, A., Piazza, C., Rossi, S.: Proportional lumpability. In: Andr\u00e9, \u00c9., Stoelinga, M. (eds.) Formal Modeling and Analysis of Timed Systems (FORMATS) 2019. Lecture Notes in Computer Science (LNCS), vol. 11750, pp. 265\u2013281. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29662-9_16","DOI":"10.1007\/978-3-030-29662-9_16"},{"key":"3_CR49","doi-asserted-by":"publisher","unstructured":"Marin, A., Piazza, C., Rossi, S.: Proportional lumpability and proportional bisimilarity. Acta Inf. 59(2\u20133), 211\u2013244 (2022). https:\/\/doi.org\/10.1007\/s00236-021-00404-y","DOI":"10.1007\/s00236-021-00404-y"},{"key":"3_CR50","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719512","volume-title":"Matrix Analysis and Applied Linear Algebra","author":"CD Meyer","year":"2000","unstructured":"Meyer, C.D.: Matrix Analysis and Applied Linear Algebra. Society for Industrial and Applied Mathematics, Philadelphia, PA (2000)"},{"key":"3_CR51","doi-asserted-by":"publisher","unstructured":"Mitrophanov, A.Y.: Sensitivity and convergence of uniformly ergodic Markov chains. J. Appl. Probab. 42(4), 1003\u20131014 (2005). https:\/\/doi.org\/10.1239\/jap\/1134587812","DOI":"10.1239\/jap\/1134587812"},{"key":"3_CR52","doi-asserted-by":"publisher","unstructured":"Mitrophanov, A.Y.: The arsenal of perturbation bounds for finite continuous-time Markov chains: a perspective. Mathematics 12(11) (2024). https:\/\/doi.org\/10.3390\/math12111608","DOI":"10.3390\/math12111608"},{"key":"3_CR53","doi-asserted-by":"publisher","unstructured":"Moler, C., Van Loan, C.: Nineteen dubious ways to compute the exponential of a matrix. twenty-five years later. SIAM Rev. 45(1), 3\u201349 (2003). https:\/\/doi.org\/10.1137\/S00361445024180","DOI":"10.1137\/S00361445024180"},{"key":"3_CR54","doi-asserted-by":"publisher","unstructured":"Pan, V.Y., Chen, Z.Q.: The complexity of the matrix eigenproblem. In: Proceedings of the thirty-first Annual ACM Symposium on Theory of Computing, pp. 507\u2013516. ACM, Atlanta Georgia USA (1999). https:\/\/doi.org\/10.1145\/301250.301389","DOI":"10.1145\/301250.301389"},{"key":"3_CR55","doi-asserted-by":"publisher","unstructured":"Piazza, C., Rossi, S.: Reasoning about proportional lumpability. In: Abate, A., Marin, A. (eds.) Quantitative Evaluation of Systems (QEST 2021). Lecture Notes in Computer Science (LNCS), vol. 12846, pp. 372\u2013390. Springer International Publishing, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85172-9_20","DOI":"10.1007\/978-3-030-85172-9_20"},{"key":"3_CR56","doi-asserted-by":"publisher","unstructured":"Piazza, C., Rossi, S., Smuseva, D.: Efficient algorithm for proportional lumpability and its application to selfish mining in public blockchains. Algorithms 17(4) (2024). https:\/\/doi.org\/10.3390\/a17040159","DOI":"10.3390\/a17040159"},{"key":"3_CR57","doi-asserted-by":"publisher","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR \u201994: Concurrency Theory. Lecture Notes in Computer Science (LNCS), vol.\u00a0836, pp. 481\u2013496. Springer, Berlin, Heidelberg (1994). https:\/\/doi.org\/10.1007\/978-3-540-48654-1_35","DOI":"10.1007\/978-3-540-48654-1_35"},{"issue":"4","key":"3_CR58","doi-asserted-by":"publisher","first-page":"1120","DOI":"10.1137\/S0036142998337235","volume":"37","author":"T Shardlow","year":"2000","unstructured":"Shardlow, T., Stuart, A.M.: A perturbation theory for ergodic Markov chains and application to numerical approximations. SIAM J. Numer. Anal. 37(4), 1120\u20131137 (2000). https:\/\/doi.org\/10.1137\/S0036142998337235","journal-title":"SIAM J. Numer. Anal."},{"key":"3_CR59","doi-asserted-by":"publisher","unstructured":"Spork, T., Baier, C., Katoen, J.P., Kl\u00fcppelholz, S., Piribauer, J.: Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains (2025). https:\/\/doi.org\/10.48550\/arXiv.2505.15587","DOI":"10.48550\/arXiv.2505.15587"},{"key":"3_CR60","doi-asserted-by":"publisher","unstructured":"Spork, T., Baier, C., Katoen, J.P., Piribauer, J., Quatmann, T.: A spectrum of approximate probabilistic bisimulations. In: Majumdar, R., Silva, A. (eds.) 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0311, pp. 37:1\u201337:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2024). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2024.37","DOI":"10.4230\/LIPIcs.CONCUR.2024.37"},{"key":"3_CR61","doi-asserted-by":"publisher","unstructured":"Tracol, M., Desharnais, J., Zhioua, A.: Computing distances between probabilistic automata. In: Massink, M., Norman, G. (eds.) Proceedings of the Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), Saarbr\u00fccken, Germany, April 1-3, 2011. EPTCS, vol.\u00a057, pp. 148\u2013162 (2011). https:\/\/doi.org\/10.4204\/eptcs.57.11","DOI":"10.4204\/eptcs.57.11"},{"issue":"1","key":"3_CR62","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1109\/TII.2017.2710316","volume":"14","author":"M Volk","year":"2018","unstructured":"Volk, M., Junges, S., Katoen, J.P.: Fast dynamic fault tree analysis by model checking techniques. IEEE Trans. Ind. Info. 14(1), 370\u2013379 (2018). https:\/\/doi.org\/10.1109\/TII.2017.2710316","journal-title":"IEEE Trans. Ind. Info."},{"key":"3_CR63","doi-asserted-by":"publisher","unstructured":"Watterson, G.A.: Markov chains with absorbing states: a genetic example. Ann. Math. Stat. 32(3), 716\u2013729 (1961). https:\/\/doi.org\/10.1214\/aoms\/1177704967","DOI":"10.1214\/aoms\/1177704967"},{"key":"3_CR64","doi-asserted-by":"publisher","unstructured":"Zhang, L., Jansen, D.N., Nielson, F., Hermanns, H.: Automata-based CSL model checking. Log. Meth. Comput. Sci. 8(2) (2011). https:\/\/doi.org\/10.1007\/978-3-642-22012-8_21","DOI":"10.1007\/978-3-642-22012-8_21"}],"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_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T16:17:54Z","timestamp":1757261874000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_3","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 to declare that are relevant to the content of this article.","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"}}]}}