Bisimulations for Probabilistic and Quantum Processes (Invited Paper)
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.
Bisimulations
probabilistic processes
quantum processes
Theory of computation~Process calculi
Theory of computation~Operational semantics
Theory of computation~Modal and temporal logics
2:1-2:14
Invited Paper
Yuxin
Deng
Yuxin Deng
Shanghai Key Laboratory of Trustworthy Computing, MOE International Joint Lab of Trustworthy Software, and International Research Center of Trustworthy Software, East China Normal University, Shanghai, China
https://orcid.org/0000-0003-0753-418X
Supported by the National Natural Science Foundation of China (61672229) and Shanghai Municipal Natural Science Foundation (16ZR1409100).
10.4230/LIPIcs.CONCUR.2018.2
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.
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.
T.A.S. Davidson. Formal verification techniques using quantum process calculus. PhD thesis, University of Warwick, 2011.
Yuxin Deng. Semantics of Probabilistic Processes: An Operational Approach. Springer, 2015.
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.
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.
Yuxin Deng and Yuan Feng. Probabilistic bisimilarity as testing equivalence. Information and Computation, 257:58-64, 2017.
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.
Yuxin Deng and Matthew Hennessy. On the semantics of Markov automata. Information and Computation, 222:139-168, 2013.
Yuxin Deng and Rob van Glabbeek. Characterising probabilistic processes logically. In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 6397 of LNCS, pages 278-293. Springer, 2010.
Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan. Testing finitary probabilistic processes (extended abstract). In Proceedings of the 20th International Conference on Concurrency Theory, volume 5710 of LNCS, pages 274-288. Springer, 2009.
Yuxin Deng and Hengyang Wu. Modal characterisations of probabilistic and fuzzy bisimulations. In Proceedings of the 16th International Conference on Formal Engineering Methods, volume 8829 of LNCS, pages 123-138. Springer, 2014.
Josée Desharnais. LabelledMarkovProcesses. PhD thesis, McGillUniversity, 1999.
Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled Markov processes. Information and Computation, 179(2):163-193, 2002.
Josée Desharnais, V. Gupta, R. Jagadeesan, and Prakash Panangaden. Approximating labelled Markov processes. Information and Computation, 184(1):160-200, 2003.
Wenjie Du, Yuxin Deng, and Daniel Gebler. Behavioural pseudometrics for nondeterministic probabilistic systems. In Proceedings of the the 2nd International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, volume 9984 of LNCS, pages 67-84. Springer, 2016.
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.
Y Feng, R Duan, Z Ji, and M Ying. Probabilistic bisimulations for quantum processes. Information and Computation, 205(11):1608-1639, 2007.
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.
Yuan Feng, Yuxin Deng, and Mingsheng Ying. Symbolic bisimulation for quantum processes. ACM Transactions on Computational Logic, 15(2):1-32, 2014.
Yuan Feng, Runyao Duan, and Mingsheng Ying. Bisimulation for Quantum Processes. ACM Transactions on Programming Languages and Systems, 34(4):1-43, 2012.
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.
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.
Simon J. Gay and Rajagopal Nagarajan. Communicating quantum processes. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 145-157. ACM, 2005.
M Hennessy and A. Ingólfsdóttir. A theory of communicating processes value-passing. Information and Computation, 107(2):202-236, 1993.
Matthew Hennessy. Exploring probabilistic bisimulations, part I. Formal Aspects of Computing, 24(4-6):749-768, 2012.
Matthew Hennessy and Huimin Lin. Symbolic bisimulations. Theoretical Computer Science, 138(2):353-389, 1995.
Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, 1985.
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.
Holger Hermanns, Augusto Parma, Roberto Segala, Björn Wachter, and Lijun Zhang. Probabilistic logical characterization. Information and Computation, 209(2):154-172, 2011.
C. Jones. Probabilistic nondeterminism. PhD thesis, University of Edinburgh, 1990.
Philippe Jorrand and Marie Lalire. Toward a quantum process algebra. In Proceedings of the First Conference on Computing Frontiers, pages 111-119. ACM, 2004.
L. Kantorovich. On the transfer of masses (in Russian). Doklady Akademii Nauk, 37(2):227-229, 1942.
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.
Marie Lalire. Relations among quantum processes: bisimilarity and congruence. Mathematical Structures in Computer Science, 16(3):407-428, 2006.
Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94:1-28, 1991.
Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
Robin Milner. Communicating and mobile systems - the Pi-calculus. Cambridge University Press, 1999.
David Park. Concurrency and automata on infinite sequences. In Proceedings of the 5th GI Conference, volume 104 of LNCS, pages 167-183. Springer, 1981.
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.
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.
Davide Sangiorgi. A theory of bisimulation for the pi-calculus. Acta Informatica, 33(1):69-97, 1996.
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.
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.
Franck van Breugel and James Worrell. An algorithm for quantitative verification of probabilistic transition systems. In Proceedings of the 12th International Conference on Concurrency Theory, volume 2154 of LNCS, pages 336-350. Springer, 2001.
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.
M Ying, Y Feng, R Duan, and Z Ji. An algebra of quantum processes. ACM Transactions on Computational Logic, 10(3):1-36, 2009.
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.
Yuxin Deng
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode