{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:17Z","timestamp":1776333497463,"version":"3.51.2"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986789","type":"print"},{"value":"9783031986796","type":"electronic"}],"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>Despite its prevalence, probabilistic bisimilarity suffers from a lack of robustness under minuscule perturbations of the transition probabilities. This can lead to discontinuities in the probabilistic bisimilarity distance function, undermining its reliability in practical applications where transition probabilities are often approximations derived from experimental data. Motivated by this limitation, we introduce the notion of robust probabilistic bisimilarity for labelled Markov chains, which ensures the continuity of the probabilistic bisimilarity distance function. We also propose an efficient algorithm for computing robust probabilistic bisimilarity and show that it performs well in practice, as evidenced by our experimental results.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_12","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:21:19Z","timestamp":1753089679000},"page":"254-275","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Robust Probabilistic Bisimilarity for\u00a0Labelled Markov Chains"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7899-8665","authenticated-orcid":false,"given":"Syyeda Zainab","family":"Fatmi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4173-6877","authenticated-orcid":false,"given":"Stefan","family":"Kiefer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4137-8862","authenticated-orcid":false,"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0002-7320-1527","authenticated-orcid":false,"given":"Franck","family":"van Breugel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"de\u00a0Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. In: Vitter, J.S., Spirakis, P.G., Yannakakis, M. (eds.) Proceedings of the 33rd Annual Symposium on Theory of Computing, Heraklion, Crete, Greece, pp. 675\u2013683. ACM (2001)","DOI":"10.1145\/380752.380871"},{"key":"12_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"van Breugel, F., Worrell, J.: Towards quantitative verification of probabilistic transition systems. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) Proceedings of the 28th International Colloquium on Automata, Languages and Programming, Crete, Greece. LNCS, vol.\u00a02076, pp. 421\u2013432. Springer (2001)","DOI":"10.1007\/3-540-48224-5_35"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Cai, X., Gu, Y.: Measuring anonymity. In: Bao, F., Li, H., Wang, G. (eds.) Proceedings of the 5th International Conference on Information Security Practice and Experience, Xi\u2019an, China. LNCS, vol.\u00a05451, pp. 183\u2013194. Springer (2009)","DOI":"10.1007\/978-3-642-00843-6_17"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., de\u00a0Alfaro, L., Majumdar, R., Raman, V.: Algorithms for game metrics (full version). Log. Methods Comput. Sci. 6(3) (2010)","DOI":"10.2168\/LMCS-6(3:13)2010"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Chen, D., van Breugel, F., Worrell, J.: On the complexity of computing probabilistic bisimilarity. In: Birkedal, L. (ed.) Proceedings of the 15th International Conference on Foundations of Software Science and Computational Structures, Tallinn, Estonia. LNCS, vol.\u00a07213, pp. 437\u2013451. Springer (2012)","DOI":"10.1007\/978-3-642-28729-9_29"},{"key":"12_CR7","series-title":"Graduate Texts in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-87859-1","volume-title":"Probability and Stochastics","author":"E \u00c7\u0131nlar","year":"2011","unstructured":"\u00c7\u0131nlar, E.: Probability and Stochastics. Graduate Texts in Mathematics, vol. 261. Springer, New York (2011)"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Comanici, G., Precup, D.: Basis function discovery using spectral clustering and bisimulation metrics. In: Burgard, W., Roth, D. (eds.) Proceedings of the 25th AAAI Conference on Artificial Intelligence, San Francisco, California, USA, pp. 325\u2013330. AAAI Press (2011)","DOI":"10.1609\/aaai.v25i1.7918"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Derisavi, S.: Signature-based symbolic algorithm for optimal Markov chain lumping. In: Proceedings of the 4th International Conference on the Quantitative Evaluation of Systems, Edinburgh, Scotland, UK, pp. 141\u2013150. IEEE Computer Society (2007)","DOI":"10.1109\/QEST.2007.27"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labeled Markov systems. In: Baeten, J.C.M., Mauw, S. (eds.) Proceedings of the 10th International Conference on Concurrency Theory, Eindhoven, The Netherlands. LNCS, vol.\u00a01664, pp. 258\u2013273. Springer (1999)","DOI":"10.1007\/3-540-48320-9_19"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theoret. Comput. Sci. 318(3), 323\u2013354 (2004)","DOI":"10.1016\/j.tcs.2003.09.013"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: logic, simulation and games. In: Proceedings of the 5th International Conference on the Quantitative Evaluation of Systems, Saint-Malo, France, pp. 264\u2013273. IEEE Computer Society (2008)","DOI":"10.1109\/QEST.2008.42"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Eastman, J.R., He, J.: A regression-based procedure for Markov transition probability estimation in land change modeling. Land 9(11) (2020)","DOI":"10.3390\/land9110407"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Fatmi, S.Z., Chen, X., Dhamija, Y., Wildes, M., Tang, Q., van Breugel, F.: Probabilistic model checking of randomized Java code. In: Laarman, A., Sokolova, A. (eds.) Proceedings of the 27th International Symposium on Model Checking Software, SPIN. LNCS, vol. 12864, pp. 157\u2013174. Springer (2021)","DOI":"10.1007\/978-3-030-84629-9_9"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Fatmi, S.Z., Kiefer, S., Parker, D., van Breugel, F.: Robust probabilistic bisimilarity for labelled Markov chains. CoRR (2025). https:\/\/doi.org\/10.48550\/arXiv.2505.15290","DOI":"10.48550\/arXiv.2505.15290"},{"key":"12_CR16","unstructured":"Giacalone, A., Jou, C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Broy, M., Jones, C.B. (eds.) Proceedings of the Working Conference on Programming Concepts and Methods, North-Holland, Sea of Galilee, Israel, pp. 443\u2013458 (1990)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Prague, Czech Republic. LNCS, vol. 11427, pp. 344\u2013350. Springer (2019)","DOI":"10.1007\/978-3-030-17462-0_20"},{"issue":"4","key":"12_CR18","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., 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":"12_CR19","doi-asserted-by":"crossref","unstructured":"Jaeger, M., Mao, H., Larsen, K.G., Mardare, R.: Continuity properties of distances for Markov processes. In: Norman, G., Sanders, W.H. (eds.) Proceedings of the 11th International Conference on Quantitative Evaluation of Systems, Florence, Italy. LNCS, vol.\u00a08657, pp. 297\u2013312. Springer (2014)","DOI":"10.1007\/978-3-319-10696-0_24"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.: Specification and refinement of probabilistic processes. In: Proceedings of the 6th Annual Symposium on Logic in Computer Science, Amsterdam, The Netherlands, pp. 266\u2013277. IEEE (1991)","DOI":"10.1109\/LICS.1991.151651"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Katoen, J., Kemna, T., Zapreev, I.S., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol.\u00a04424, pp. 87\u2013101. Springer (2007)","DOI":"10.1007\/978-3-540-71209-1_9"},{"key":"12_CR22","volume-title":"Finite Markov Chains","author":"JG Kemeny","year":"1960","unstructured":"Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Springer, Heidelberg (1960)"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Kozen, D.: A probabilistic PDL. In: Johnson, D.S., et al. (eds.) Proceedings of the 15th Annual Symposium on Theory of Computing, Boston, Massachusetts, USA, pp. 291\u2013297. ACM (1983)","DOI":"10.1145\/800061.808758"},{"key":"12_CR24","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, Snowbird, Utah, USA. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Larsen, K., Skou, A.: Bisimulation through probabilistic testing. In: Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages, Austin, TX, USA, pp. 344\u2013352. ACM (1989)","DOI":"10.1145\/75277.75307"},{"key":"12_CR26","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer (2004)"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Mizutani, D., Lethanh, N., Adey, B.T., Kaito, K.: Improving the estimation of Markov transition probabilities using mechanistic-empirical models. Front. Built Environ. 3, 58 (2017)","DOI":"10.3389\/fbuil.2017.00058"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Olariu, E., Cadwell, K.K., Hancock, E., Trueman, D., Chevrou-Severac, H.: Current recommendations on the estimation of transition probabilities in Markov cohort models for use in health care decision-making: a targeted literature review. ClinicoEcon. Outcomes Res. 9, 537\u2013546 (2017)","DOI":"10.2147\/CEOR.S135445"},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"Spitzer, F.: Principles of Random Walk. Graduate Texts in Mathematics. Springer, New York (1964)","DOI":"10.1007\/978-1-4757-4229-9"},{"issue":"8","key":"12_CR30","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1007\/s40273-021-01034-5","volume":"39","author":"T Srivastava","year":"2021","unstructured":"Srivastava, T., Latimer, N.R., Tappenden, P.: Estimation of transition probabilities for state-transition models: a review of NICE appraisals. Pharmacoeconomics 39(8), 869\u2013878 (2021)","journal-title":"Pharmacoeconomics"},{"key":"12_CR31","unstructured":"Tang, Q., van Breugel, F.: Algorithms to compute probabilistic bisimilarity distances for labelled Markov chains. In: Meyer, R., Nestmann, U. (eds.) Proceedings of the 28th International Conference on Concurrency Theory, Berlin, Germany. LIPIcs, vol.\u00a085, pp. 27:1\u201327:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017)"},{"key":"12_CR32","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1049\/iet-syb.2009.0039","volume":"4","author":"D Thorsley","year":"2010","unstructured":"Thorsley, D., Klavins, E.: Approximating stochastic biochemical processes with Wasserstein pseudometrics. IET Syst. Biol. 4, 193\u2013211 (2010)","journal-title":"IET Syst. Biol."},{"issue":"2","key":"12_CR33","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."}],"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_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T16:18:06Z","timestamp":1757261886000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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"}}]}}