Document Open Access Logo

Bisimulations for Probabilistic and Quantum Processes (Invited Paper)

Author Yuxin Deng

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.2.pdf
  • Filesize: 0.49 MB
  • 14 pages

Document Identifiers

Author Details

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

Funding

  • Deng, Yuxin: Supported by the National Natural Science Foundation of China (61672229) and Shanghai Municipal Natural Science Foundation (16ZR1409100).

Cite AsGet BibTex

Yuxin Deng. Bisimulations for Probabilistic and Quantum Processes (Invited Paper). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CONCUR.2018.2

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
  • Theory of computation → Operational semantics
  • Theory of computation → Modal and temporal logics
Keywords
  • Bisimulations
  • probabilistic processes
  • quantum processes

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  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. Google Scholar
  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. Google Scholar
  3. T.A.S. Davidson. Formal verification techniques using quantum process calculus. PhD thesis, University of Warwick, 2011. Google Scholar
  4. Yuxin Deng. Semantics of Probabilistic Processes: An Operational Approach. Springer, 2015. Google Scholar
  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. Google Scholar
  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. Google Scholar
  7. Yuxin Deng and Yuan Feng. Probabilistic bisimilarity as testing equivalence. Information and Computation, 257:58-64, 2017. Google Scholar
  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. Google Scholar
  9. Yuxin Deng and Matthew Hennessy. On the semantics of Markov automata. Information and Computation, 222:139-168, 2013. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. 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. Google Scholar
  13. Josée Desharnais. LabelledMarkovProcesses. PhD thesis, McGillUniversity, 1999. Google Scholar
  14. Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled Markov processes. Information and Computation, 179(2):163-193, 2002. Google Scholar
  15. Josée Desharnais, V. Gupta, R. Jagadeesan, and Prakash Panangaden. Approximating labelled Markov processes. Information and Computation, 184(1):160-200, 2003. Google Scholar
  16. 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. Google Scholar
  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. Google Scholar
  18. Y Feng, R Duan, Z Ji, and M Ying. Probabilistic bisimulations for quantum processes. Information and Computation, 205(11):1608-1639, 2007. Google Scholar
  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. Google Scholar
  20. Yuan Feng, Yuxin Deng, and Mingsheng Ying. Symbolic bisimulation for quantum processes. ACM Transactions on Computational Logic, 15(2):1-32, 2014. Google Scholar
  21. Yuan Feng, Runyao Duan, and Mingsheng Ying. Bisimulation for Quantum Processes. ACM Transactions on Programming Languages and Systems, 34(4):1-43, 2012. Google Scholar
  22. 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. Google Scholar
  23. 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. Google Scholar
  24. 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. Google Scholar
  25. M Hennessy and A. Ingólfsdóttir. A theory of communicating processes value-passing. Information and Computation, 107(2):202-236, 1993. Google Scholar
  26. Matthew Hennessy. Exploring probabilistic bisimulations, part I. Formal Aspects of Computing, 24(4-6):749-768, 2012. Google Scholar
  27. Matthew Hennessy and Huimin Lin. Symbolic bisimulations. Theoretical Computer Science, 138(2):353-389, 1995. Google Scholar
  28. Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, 1985. Google Scholar
  29. 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. Google Scholar
  30. Holger Hermanns, Augusto Parma, Roberto Segala, Björn Wachter, and Lijun Zhang. Probabilistic logical characterization. Information and Computation, 209(2):154-172, 2011. Google Scholar
  31. C. Jones. Probabilistic nondeterminism. PhD thesis, University of Edinburgh, 1990. Google Scholar
  32. Philippe Jorrand and Marie Lalire. Toward a quantum process algebra. In Proceedings of the First Conference on Computing Frontiers, pages 111-119. ACM, 2004. Google Scholar
  33. L. Kantorovich. On the transfer of masses (in Russian). Doklady Akademii Nauk, 37(2):227-229, 1942. Google Scholar
  34. 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. Google Scholar
  35. Marie Lalire. Relations among quantum processes: bisimilarity and congruence. Mathematical Structures in Computer Science, 16(3):407-428, 2006. Google Scholar
  36. Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94:1-28, 1991. Google Scholar
  37. Robin Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  38. Robin Milner. Communicating and mobile systems - the Pi-calculus. Cambridge University Press, 1999. Google Scholar
  39. David Park. Concurrency and automata on infinite sequences. In Proceedings of the 5th GI Conference, volume 104 of LNCS, pages 167-183. Springer, 1981. Google Scholar
  40. 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. Google Scholar
  41. 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. Google Scholar
  42. Davide Sangiorgi. A theory of bisimulation for the pi-calculus. Acta Informatica, 33(1):69-97, 1996. Google Scholar
  43. 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. Google Scholar
  44. 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. Google Scholar
  45. 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. Google Scholar
  46. 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. Google Scholar
  47. M Ying, Y Feng, R Duan, and Z Ji. An algebra of quantum processes. ACM Transactions on Computational Logic, 10(3):1-36, 2009. Google Scholar
  48. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact