Published in Volume XXXII, Issue 2, 2022, pages 211-254, doi: 10.7561/SACS.2022.2.211
Authors: W. Du, Y. Deng, D. Gebler
Abstract
For the model of probabilistic labelled transition systems that allow for the co-existence of nondeterminism and probabilities, we present two notions of bisimulation metrics: one is state-based and the other is distribution-based. We provide a sound and complete modal characterisation for each of them, using real-valued modal logics based on Hennessy-Milner logic. The logic for characterising the state-based metric is much simpler than an earlier logic proposed by Desharnais et al. as it uses only two non-expansive operators rather than the general class of non-expansive operators. For the kernels of the two metrics, which correspond to two notions of bisimilarity, we give a comprehensive comparison with some typical distribution-based bisimilarities in the literature.
Full Text (PDF)References
[1] Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel. Computing probabilistic bisimilarity distances for probabilistic automata. Logical Methods in Computer Science, 17(1):9:1-9:36, 2021. doi:10.23638/LMCS-17(1:9)2021.
[2] Valentina Castiglioni, Daniel Gebler, and Simone Tini. Logical characterization of bisimulation metrics. In Mirco Tribastone and Herbert Wiklicky, editors, 14th International Workshop Quantitative Aspects of Programming Languages and Systems, QAPL 2016, volume 227 of Electronic Proceedings in Theoretical Computer Science, pages 44-62, 2016. doi:10.4204/EPTCS.227.4.
[3] Krishnendu Chatterjee, Luca De Alfaro, Rupak Majumdar, and Vishwanath Raman. Algorithms for game metrics. Logical Methods in Computer Science, 6(3), 2010. doi:10.2168/LMCS-6(3:13)2010.
[4] Rance Cleaveland, S. Purushothaman Iyer, and Murali Narasimha. Probabilistic temporal logics via the modal mu-calculus. Theoretical Computer Science, 342(2-3):316-350, 2005. doi:10.1016/j.tcs.2005.03.048.
[5] Pedro R. D’Argenio, Pedro Sánchez Terraf, and Nicolás Wolovick. Bisimulations for non-deterministic labelled Markov processes. Mathematical Structures in Computer Science, 22(1):43-68, 2012. doi:10.1017/S0960129511000454.
[6] Luca De Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching system metrics. IEEE Transactions on Software Engineering, 35(2):258-273, 2009. doi:10.1109/TSE.2008.106.
[7] Luca de Alfaro, Rupak Majumdar, Vishwanath Raman, and Mariëlle Stoelinga. Game relations and metrics. In 22nd IEEE Symposium on Logic in Computer Science, LICS 2007, pages 99-108. IEEE Computer Society, 2007. doi:10.1109/LICS.2007.22.
[8] Luca De Alfaro, Rupak Majumdar, Vishwanath Raman, and Mariëlle Stoelinga. Game refinement relations and metrics. Logical Methods in Computer Science, 4(3), 2008. doi:10.2168/LMCS-4(3:7)2008.
[9] Erik P. de Vink and Jan J. M. M. Rutten. Bisimulation for probabilistic transition systems: A coalgebraic approach. Theoretical Computer Science, 221(1-2):271-293, 1999. doi:10.1016/S0304-3975(99)00035-3.
[10] Jeremy Ian den Hartog. Probabilistic Extensions of Semantical Models. PhD thesis, Free University Amsterdam, 2002.
[11] Yuxin Deng. Semantics of Probabilistic Processes: An Operational Approach. Springer, 2014. doi:10.1007/978-3-662-45198-4.
[12] Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang. Metrics for action-labelled quantitative transition systems. Electronic Notes in Theoretical Computer Science, 153(2):79-96, 2006. doi:10.1016/j.entcs.2005.10.033.
[13] Yuxin Deng and Wenjie Du. Logical, metric, and algorithmic characterisations of probabilistic bisimulation. Technical Report CMU-CS-11-110, Carnegie Mellon University, 2011. arXiv:1103.4577.250
[14] Yuxin Deng, Yuan Feng, and Ugo Dal Lago. On coinduction and quantum lambda calculi. In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, volume 42 of LIPIcs, pages 427-440. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015. doi:10.4230/LIPIcs.CONCUR.2015.427.
[15] Yuxin Deng and Matthew Hennessy. On the semantics of Markov automata. Information and Computation, 222:139-168, 2013. doi:10.1016/j.ic.2012.10.010.
[16] Yuxin Deng, Rob J. van Glabbeek, Matthew Hennessy, and Carroll Morgan. Testing finitary probabilistic processes. In Mario Bravetti and Gianluigi Zavattaro, editors, 20th International Conference on Concurrency Theory, CONCUR 2009, volume 5710 of Lecture Notes in Computer Science, pages 274-288. Springer, 2009. doi:10.1007/978-3-642-04081-8_19.
[17] Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theoretical Computer Science, 318(3):323-354, 2004. doi:10.1016/j.tcs.2003.09.013.
[18] Josée Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In 17th IEEE Symposium on Logic in Computer Science, LICS 2002, pages 413-422. IEEE Computer Society, 2002. doi:10.1109/LICS.2002.1029849.
[19] Wenjie Du, Yuxin Deng, and Daniel Gebler. Behavioural pseudometrics for nondeterministic probabilistic systems. In Martin Fränzle, Deepak Kapur, and Naijun Zhan, editors, 2nd International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2016, volume 9984 of Lecture Notes in Computer Science, pages 67-84, 2016. doi:10.1007/978-3-319-47677-3_5.
[20] Christian Eisentraut, Jens Chr. Godskesen, Holger Hermanns, Lei Song, and Lijun Zhang. Probabilistic bisimulation for realistic schedulers. In Nikolaj S. Bjørner and Frank S. de Boer, editors, 20th International Symposium on Formal Methods, FM 2015, volume 9109 of Lecture Notes in Computer Science, pages 248-264. Springer, 2015. doi:10.1007/978-3-319-19249-9_16.
[21] Uli Fahrenberg and Axel Legay. The quantitative linear-time–branching-time spectrum. Theoretical Computer Science, 538:54-69, 2014. doi:10.1016/j.tcs.2013.07.030.
[22] Yuan Feng, Lei Song, and Lijun Zhang. Distribution-based bisimulation and bisimulation metric in probabilistic automata, 2015. arXiv:1512.05027.
[23] Yuan Feng and Mingsheng Ying. Toward automatic verification of quantum cryptographic protocols. In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, volume 42 of LIPIcs, pages 441-455. Schloss Dagstuhl- Leibniz-Zentrum für Informatik, 2015. doi:10.4230/LIPIcs.CONCUR.2015.441.
[24] Yuan Feng and Lijun Zhang. When equivalence and bisimulation join forces in probabilistic automata. In Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, editors, 19th International Symposium on Formal Methods, FM 2014, volume 8442 of Lecture Notes in Computer Science, pages 247-262. Springer, 2014. doi:10.1007/978-3-319-6410-9_18.
[25] Norm Ferns, Prakash Panangaden, and Doina Precup. Bisimulation metrics for continuous Markov decision processes. SIAM Journal on Computing, 40(6):1662-1714, 2011. doi:10.1137/10080484X.
[26] Norm Ferns, Doina Precup, and Sophia Knight. Bisimulation for Markov decision processes through families of functional expressions. In Franck van Breugel, Elham Kashefi, Catuscia Palamidessi, and Jan Rutten, editors, Horizons of the Mind. A Tribute to Prakash Panangaden, volume 8464 of Lecture Notes in Computer Science, pages 319-342. Springer, 2014. doi:10.1007/978-3-319-06880-0_17.
[27] Daniel Gebler, Kim Guldstrand Larsen, and Simone Tini. Compositional metric reasoning with probabilistic process calculi. In Andrew M. Pitts, editor, 18th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2015, volume 9034 of Lecture Notes in Computer Science, pages 230-245. Springer, 2015. doi:10.1007/978-3-662-46678-0_15.
[28] Alessandro Giacalone, Chi-Chang Jou, and Scott A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Manfred Broy and Cliff B. Jones, editors, IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, pages 443-458. North-Holland, 1990.
[29] Matthew Hennessy. Exploring probabilistic bisimulations, part I. Formal Aspects of Computing, 24(4-6):749-768, 2012. doi:10.1007/s00165-012-0242-7.
[30] Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32:137-161, 1985. doi:10.1145/2455.2460.
[31] Holger Hermanns, Jan Krcál, and Jan Kretı́nský. Probabilistic bisimulation: Naturally on distributions. In Paolo Baldan and Daniele Gorla, editors, 25th International Conference on Concurrency Theory, CONCUR 2014, volume 8704 of Lecture Notes in Computer Science, pages 249-265. Springer, 2014. doi:10.1007/978-3-662-44584-6_18.
[32] Michael Huth and Marta Z. Kwiatkowska. Quantitative analysis and model checking. In 12th Annual IEEE Symposium on Logic in Computer Science, pages 111-122. IEEE Computer Society, 1997. doi:10.1109/LICS.1997.614940.
[33] Bengt Jonsson and Wang Larsen, Kim G.and Yi. Probabilistic extensions of process algebras. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 685-710. Elsevier, 2001. doi:10.1016/b978-044482830-9/50029-1.
[34] Leonid Kantorovich and Gennady S. Rubinstein. On a space of totally additive functions. Vestnik Leningrad Universitet, 13:52-59, 1958.
[35] Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, 1983. doi:10.1016/0304-3975(82)90125-6.
[36] Marta Z. Kwiatkowska and Gethin Norman. Probabilistic metric semantics for a simple language with recursion. In Wojciech Penczek and Andrzej Szalas, editors, 21st International Symposium on Mathematical Foundations of Computer Science 1996, MFCS’96, volume 1113 of Lecture Notes in Computer Science, pages 419-430. Springer, 1996. doi:10.1007/3-540-61550-4_167.
[37] Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, 1991. doi:10.1016/0890-5401(91)90030-6.
[38] Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems – Specification. Springer, 1992. doi:10.1007/978-1-4612-0931-7.
[39] Gethin Norman. Metric Semantics for Reactive Probabilistic Systems. PhD thesis, University of Birmingham, 1997.
[40] Anna Philippou, Insup Lee, and Oleg Sokolsky. Weak bisimulation for probabilistic systems. In Catuscia Palamidessi, editor, 11th International Conference on Concurrency Theory, CONCUR 2000, volume 1877 of Lecture Notes in Computer Science, pages 334-349. Springer, 2000. doi:10.1007/3-540-44618-4_25.
[41] Vishwanath Raman. Game Relations, Metrics and Refinements. PhD thesis, University of California, 2010.
[42] Roberto Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, 1995.
[43] Roberto Segala and Nancy A. Lynch. Probabilistic simulations for probabilistic processes. In Bengt Jonsson and Joachim Parrow, editors, 5th International Conference on Concurrency Theory, CONCUR ’94, volume 836 of Lecture Notes in Computer Science, pages 481-496. Springer, 1994. doi:10.1007/978-3-540-48654-1_35.
[44] Lin Song, Yuxin Deng, and Xiaojuan Cai. Towards automatic measurement of probabilistic processes. In 7th International Conference on Quality Software, QSIC 2007, pages 50-59. IEEE Computer Society, 2007. doi:10.1109/QSIC.2007.65.
[45] Qiyi Tang and Franck van Breugel. Deciding probabilistic bisimilarity distance one for probabilistic automata. Journal of Computer and System Sciences, 111:57-84, 2020. doi:10.1016/j.jcss.2020.02.003.
[46] Hermann Thorisson. Coupling, Stationarity, and Regeneration. Probability and Its Applications. Springer, 2000.
[47] Franck van Breugel, Babita Sharma, and James Worrell. Approximating a behavioural pseudometric without discount for probabilistic systems. Logical Methods in Computer Science, 4(2), 2008. doi:10.2168/LMCS-4(2:2)2008.
[48] Franck van Breugel and James Worrell. An algorithm for quantitative verification of probabilistic transition systems. In Kim Guldstrand Larsen and Mogens Nielsen, editors, 12th International Conference on Concurrency Theory, CONCUR 2001, volume 2154 of Lecture Notes in Computer Science, pages 336-350. Springer, 2001. doi:10.1007/3-540-44685-0_23.
[49] Franck van Breugel and James Worrell. Towards quantitative verification of probabilistic transition systems. In Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors, 28th International Colloquium on Automata, Languages and Programming, volume 2076 of Lecture Notes in Computer Science, pages 421-432. Springer, 2001. doi:10.1007/3-540-48224-5_35.
[50] Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science, 331(1):115-142, 2005. doi:10.1016/j.tcs.2004.09.035.
[51] Mingsheng Ying. Bisimulation indexes and their applications. Theoretical Computer Science, 275(1-2):1-68, 2002. doi:10.1016/S0304-3975(01)00124-4.
Bibtex
@article{sacscuza:du22bpnps,
title={Behavioural Pseudometrics for Nondeterministic Probabilistic Systems},
author={W. Du, Y. Deng, D. Gebler},
journal={Scientific Annals of Computer Science},
volume={32},
number={2},
organization={Alexandru Ioan Cuza University, Ia\c si, Rom\^ania},
year={2022},
pages={211-254},
publisher={Alexandru Ioan Cuza University Press, Ia\c si},
doi={10.7561/SACS.2022.2.211}
}