Bisimulations for probabilistic and quantum processes (invited paper). (English) Zbl 1520.68093
Schewe, Sven (ed.) et al., 29th international conference on concurrency theory. CONCUR 2018, Beijing, China, September 4–7, 2018. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 118, Article 2, 14 p. (2018).
Summary: Bisimulation is a fundamental concept in the classical concurrency theory for comparing the behaviour of nondeterministic processes. It admits elegant characterisations from various perspectives such as fixed point theory, modal logics, game theory, coalgebras etc. In this paper, we review some key ideas used in the formulations and characterisations of reasonable notions of bisimulations for both probabilistic and quantum processes. To some extent the transition from probabilistic to quantum concurrency theory is smooth and natural. However, new ideas need also to be introduced. We have not yet reached the stage of formally verifying quantum communication protocols and quantum algorithms using bisimulations implemented by automatic tools. We discuss some recent efforts in this direction.
For the entire collection see [Zbl 1402.68024].
For the entire collection see [Zbl 1402.68024].
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Software:
verifierReferences:
| [1] | Christel Baier, Bettina Engelen, and Mila E. Majster-Cederbaum. Deciding bisimilarity and similarity for probabilistic processes. Journal of Computer and System Sciences, 60(1):187-231, 2000. · Zbl 1073.68690 |
| [2] | C.H. Bennett and G. Brassard. Quantum cryptography: Public key distribution and coin tossing. In Proceedings of IEEE International Conference on Computers, Systems and Signal Processing, pages 175-179, 1984. |
| [3] | T.A.S. Davidson. Formal verification techniques using quantum process calculus. PhD thesis, University of Warwick, 2011. |
| [4] | Yuxin Deng. Semantics of Probabilistic Processes: An Operational Approach. Springer, 2015. · Zbl 1315.68002 |
| [5] | Yuxin Deng and Yuan Feng. Open bisimulation for quantum processes. In Proceedings of the 7th IFIP International Conference on Theoretical Computer Science, volume 7604 of LNCS, pages 119-133. Springer, 2012. · Zbl 1362.68210 |
| [6] | Yuxin Deng and Yuan Feng. Bisimulations for probabilistic linear lambda calculi. In Proceedings of the 11th IEEE International Symposium on Theoretical Aspects of Software Engineering, pages 1-8. IEEE Computer Society, 2017. |
| [7] | Yuxin Deng and Yuan Feng. Probabilistic bisimilarity as testing equivalence. Information and Computation, 257:58-64, 2017. · Zbl 1380.68293 |
| [8] | Yuxin Deng, Yuan Feng, and Ugo Dal Lago. On coinduction and quantum lambda calculi. In Proceedings of the 26th International Conference on Concurrency Theory, volume 42 of LIPIcs, pages 427-440. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2015. · Zbl 1374.68097 |
| [9] | Yuxin Deng and Matthew Hennessy. On the semantics of Markov automata. Information and Computation, 222:139-168, 2013. · Zbl 1286.68362 |
| [10] | Yuxin Deng and Rob van Glabbeek. Characterising probabilistic processes logically. In Proceedings of the 17th International Conference on Logic for Programming, Artificial In-telligence and Reasoning, volume 6397 of LNCS, pages 278-293. Springer, 2010. · Zbl 1306.68122 |
| [11] | Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan. Testing finit-ary probabilistic processes (extended abstract). In Proceedings of the 20th International Conference on Concurrency Theory, volume 5710 of LNCS, pages 274-288. Springer, 2009. · Zbl 1254.68166 |
| [12] | Yuxin Deng and Hengyang Wu. Modal characterisations of probabilistic and fuzzy bisimula-tions. In Proceedings of the 16th International Conference on Formal Engineering Methods, volume 8829 of LNCS, pages 123-138. Springer, 2014. |
| [13] | Josée Desharnais. LabelledMarkovProcesses. PhD thesis, McGillUniversity, 1999. |
| [14] | Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled Markov processes. Information and Computation, 179(2):163-193, 2002. · Zbl 1096.68103 |
| [15] | Josée Desharnais, V. Gupta, R. Jagadeesan, and Prakash Panangaden. Approximating labelled Markov processes. Information and Computation, 184(1):160-200, 2003. · Zbl 1028.68091 |
| [16] | Wenjie Du, Yuxin Deng, and Daniel Gebler. Behavioural pseudometrics for nondetermin-istic probabilistic systems. In Proceedings of the the 2nd International Symposium on De-pendable Software Engineering: Theories, Tools, and Applications, volume 9984 of LNCS, pages 67-84. Springer, 2016. · Zbl 1393.68114 |
| [17] | Christian Eisentraut, Jens Chr. Godskesen, Holger Hermanns, Lei Song, and Lijun Zhang. Probabilistic bisimulation for realistic schedulers. In Proceedings of the 20th International Symposium on Formal Methods, volume 9109 of LNCS, pages 248-264. Springer, 2015. · Zbl 1427.68193 |
| [18] | Y Feng, R Duan, Z Ji, and M Ying. Probabilistic bisimulations for quantum processes. Information and Computation, 205(11):1608-1639, 2007. · Zbl 1130.68079 |
| [19] | Y Feng, R Duan, and M Ying. Bisimulations for quantum processes. In Mooly Sagiv, editor, Proceedings of the 38th ACM Symposium on Principles of Programming Languages, pages 523-534, Austin, Texas, USA, 2011. · Zbl 1284.68425 |
| [20] | Y. Deng 2:13 |
| [21] | Yuan Feng, Yuxin Deng, and Mingsheng Ying. Symbolic bisimulation for quantum pro-cesses. ACM Transactions on Computational Logic, 15(2):1-32, 2014. · Zbl 1291.68237 |
| [22] | Yuan Feng, Runyao Duan, and Mingsheng Ying. Bisimulation for Quantum Processes. ACM Transactions on Programming Languages and Systems, 34(4):1-43, 2012. |
| [23] | Yuan Feng and Mingsheng Ying. Toward automatic verification of quantum cryptographic protocols. In 26th International Conference on Concurrency Theory, volume 42 of LIPIcs, pages 441-455. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2015. · Zbl 1374.68327 |
| [24] | Yuan Feng and Lijun Zhang. When equivalence and bisimulation join forces in probabilistic automata. In Proceedings of the 19th International Symposium on Formal Methods, volume 8442 of LNCS, pages 247-262. Springer, 2014. |
| [25] | Simon J. Gay and Rajagopal Nagarajan. Communicating quantum processes. In Pro-ceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 145-157. ACM, 2005. · Zbl 1369.68207 |
| [26] | M Hennessy and A. Ingólfsdóttir. A theory of communicating processes value-passing. Information and Computation, 107(2):202-236, 1993. · Zbl 0794.68098 |
| [27] | Matthew Hennessy. Exploring probabilistic bisimulations, part I. Formal Aspects of Com-puting, 24(4-6):749-768, 2012. · Zbl 1259.68153 |
| [28] | Matthew Hennessy and Huimin Lin. Symbolic bisimulations. Theoretical Computer Science, 138(2):353-389, 1995. · Zbl 0874.68187 |
| [29] | Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, 1985. · Zbl 0629.68021 |
| [30] | Holger Hermanns, Jan Krcál, and Jan Kretínský. Probabilistic bisimulation: Naturally on distributions. In Proceedings of the 25th International Conference on Concurrency Theory, volume 8704 of LNCS, pages 249-265. Springer, 2014. · Zbl 1417.68130 |
| [31] | Holger Hermanns, Augusto Parma, Roberto Segala, Björn Wachter, and Lijun Zhang. Prob-abilistic logical characterization. Information and Computation, 209(2):154-172, 2011. · Zbl 1210.68072 |
| [32] | C. Jones. Probabilistic nondeterminism. PhD thesis, University of Edinburgh, 1990. |
| [33] | Philippe Jorrand and Marie Lalire. Toward a quantum process algebra. In Proceedings of the First Conference on Computing Frontiers, pages 111-119. ACM, 2004. |
| [34] | L. Kantorovich. On the transfer of masses (in Russian). Doklady Akademii Nauk, 37(2):227-229, 1942. |
| [35] | Takahiro Kubota, Yoshihiko Kakutani, Go Kato, Yasuhito Kawano, and Hideki Sakurada. Semi-automated verification of security proofs of quantum cryptographic protocols. Journal of Symbolic Computation, 73:192-220, 2016. · Zbl 1336.68164 |
| [36] | Marie Lalire. Relations among quantum processes: bisimilarity and congruence. Mathem-atical Structures in Computer Science, 16(3):407-428, 2006. · Zbl 1122.68060 |
| [37] | Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94:1-28, 1991. · Zbl 0756.68035 |
| [38] | Robin Milner. Communication and Concurrency. Prentice Hall, 1989. · Zbl 0683.68008 |
| [39] | Robin Milner. Communicating and mobile systems -the Pi-calculus. Cambridge University Press, 1999. · Zbl 0942.68002 |
| [40] | David Park. Concurrency and automata on infinite sequences. In Proceedings of the 5th GI Conference, volume 104 of LNCS, pages 167-183. Springer, 1981. · Zbl 0457.68049 |
| [41] | Augusto Parma and Roberto Segala. Logical characterizations of bisimulations for discrete probabilistic systems. In Proceedings of the 10th International Conference on Foundations of Software Science and Computational Structures, volume 4423 of LNCS, pages 287-301. Springer, 2007. · Zbl 1195.68072 |
| [42] | J. Sack and Lijun Zhang. A general framework for probabilistic characterizing formulae. In Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation, volume 7148 of LNCS, pages 396-411. Springer, 2012. · Zbl 1326.68176 |
| [43] | Davide Sangiorgi. A theory of bisimulation for the pi-calculus. Acta Informatica, 33(1):69-97, 1996. · Zbl 0835.68072 |
| [44] | Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. In Proceedings of the 5th International Conference on Concurrency Theory, volume 836 of LNCS, pages 481-496. Springer, 1994. · Zbl 0839.68067 |
| [45] | Franck van Breugel, Michael W. Mislove, Joël Ouaknine, and James Worrell. Domain theory, testing and simulation for labelled Markov processes. Theoretical Computer Science, 333(1-2):171-197, 2005. · Zbl 1070.68108 |
| [46] | Franck van Breugel and James Worrell. An algorithm for quantitative verification of prob-abilistic transition systems. In Proceedings of the 12th International Conference on Con-currency Theory, volume 2154 of LNCS, pages 336-350. Springer, 2001. · Zbl 1006.68079 |
| [47] | Rob J. van Glabbeek, Scott A. Smolka, Bernhard Steffen, and Chris M. N. Tofts. Reactive, generative, and stratified models of probabilistic processes. In Proceedings of the 5th Annual Symposium on Logic in Computer Science, pages 130-141. IEEE Computer Society, 1990. |
| [48] | M Ying, Y Feng, R Duan, and Z Ji. An algebra of quantum processes. ACM Transactions on Computational Logic, 10(3):1-36, 2009. · Zbl 1351.68187 |
| [49] | Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, and David N. Jansen. Flow faster: Efficient decision algorithms for probabilistic simulations. Logical Methods in Computer Science, 4(4):1-43, 2008. · Zbl 1161.68473 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
