Symbolic Bisimulation for Quantum Processes

Abstract

With the previous notions of bisimulation presented in the literature, to check if two quantum processes are bisimilar, we have to instantiate their free quantum variables with arbitrary quantum states, and verify the bisimilarity of the resulting configurations. This makes checking bisimilarity infeasible from an algorithmic point of view, because quantum states constitute a continuum. In this article, we introduce a symbolic operational semantics for quantum processes directly at the quantum operation level, which allows us to describe the bisimulation between quantum processes without resorting to quantum states. We show that the symbolic bisimulation defined here is equivalent to the open bisimulation for quantum processes in previous work, when strong bisimulations are considered. An algorithm for checking symbolic ground bisimilarity is presented. We also give a modal characterisation for quantum bisimilarity based on an extension of Hennessy-Milner logic to quantum processes.

References

1. C. H. Bennett and G. Brassard. 1984. Quantum cryptography: Public-key distribution and coin tossing. In Proceedings of the IEEE International Conference on Computer, Systems and Signal Processing. 175--179.
2. C. H. Bennett, G. Brassard, C. Crepeau, R. Jozsa, A. Peres, and W. Wootters. 1993. Teleporting an unknown quantum state via dual classical and EPR channels. Phys. Rev. Lett. 70, 1895--1899.
3. C. H. Bennett and S. J. Wiesner. 1992. Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states. Phys. Rev. Lett. 69, 20, 2881--2884.
4. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. 1992. Symbolic model checking: 1020 states and beyond. Inf. Comput. 98, 2, 142--170.
5. J. Cheriyan, T. Hagerup, and K. Mehlhorn. 1990. Can a maximum flow be computed in o(nm) time? In Automata, Languages and Programming, M. Paterson, Ed., Lecture Notes in Computer Science, vol. 443, Springer, 235--248.
6. T. A. S. Davidson. 2011. Formal verification techniques using quantum process calculus. PhD thesis, University of Warwick.
7. Y. Deng and W. Du. 2011. Logical, metric, and algorithmic characterisations of probabilistic bisimulation. arXiv:1103.4577v1 {cs.LO}. Tech. rep. CMU-CS-11-110, Carnegie Mellon University.
8. Y. Deng and Y. Feng. 2012. Open bisimulation for quantum processes. In Theoiretical Computer Science, Lecture Notes in Computer Science, vol. 7604, Springer, 119--133. (Full version available at http://arxiv.org/abs/1202.3484).
9. Y. Feng, R. Duan, Z. Ji, and M. Ying. 2007. Probabilistic bisimulations for quantum processes. Inf. Comput. 205, 11, 1608--1639.
10. Y. Feng, R. Duan, and M. Ying. 2011. Bisimulation for quantum processes. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 523--534.
11. Y. Feng, R. Duan, and M. Ying. 2012. Bisimulation for quantum processes. ACM Trans. Program. Lang. Syst. 34, 4, 1--43.
12. Y. Feng, N. Yu, and M. Ying. 2013. Model checking quantum Markov chains. J. Comput. Syst. Sci. 79, 7, 1181--1198.
13. S. Gay, R. Nagarajan, and N. Papanikolaou. 2006. Probabilistic model-checking of quantum protocols. In Proceedings of the 2nd International Workshop on Developments in Computational Models.
14. S. Gay, R. Nagarajan, and N. Papanikolaou. 2008. QMC: A model checker for quantum systems. In Proceedings of the International Conference on Computer Aided Verification. Springer, 543--547.
15. S. Gay and R. Nagarajan. 2005. Communicating quantum processes. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. J. Palsberg and M. Abadi, Eds., 145--157.
16. M. Hennessy and A. Ingolfsdotir. 1993. A theory of communicating processes value-passing. Inf. Comput. 107, 2, 202--236.
17. M. Hennessy and H. Lin. 1995. Symbolic bisimulations. Theor. Comput. Sci. 138, 2, 353--389.
18. P. Jorrand and M. Lalire. 2004. Toward a quantum process algebra. In Proceedings of the 2nd International Workshop on Quantum Programming Languages. P. Selinger, Ed., 111.
19. K. Kraus. 1983. States, Effects and Operations: Fundamental Notions of Quantum Theory. Springer.
20. T. Kubota, Y. Kakutani, G. Kato, Y. Kawano, and H. Sakurada. 2012. Application of a process calculus to security proofs of quantum protocols. In Proceedings of the International Conference on Foundations of Computer Science (FCS'12).
21. M. Lalire. 2006. Relations among quantum processes: Bisimilarity and congruence. Math. Structures Comput. Sci. 16, 3, 407--428.
22. R. Milner. 1989. Communication and Concurrency. Prentice Hall, Englewood Cliffs, NJ.
23. M. Nielsen and I. Chuang. 2000. Quantum Computation and Quantum Information. Cambridge University Press.
24. N. K. Papanikolaou. 2008. Model checking quantum protocols. Ph.D. thesis, University of Warwick.
25. D. Sangiorgi. 1996. A theory of bisimulation for the pi-calculus. Acta Informatica 33, 1, 69--97.
26. Neumann, J. 1955. States, Effects and Operations: Fundamental Notions of Quantum Theory. Princeton University Press.
27. M. Ying, Y. Feng, R. Duan, and Z. Ji. 2009. An algebra of quantum processes. ACM Trans. Comput. Log. 10, 3, 1--36.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

• Theory of computation

  • Formal languages and automata theory

  • Logic

  • Semantics and reasoning

    • Program reasoning