×

Probabilistic bisimulations for quantum processes. (English) Zbl 1130.68079

Summary: Modeling and reasoning about concurrent quantum systems is very important for both distributed quantum computing and quantum protocol verification. As a consequence, a general framework formally describing communication and concurrency in complex quantum systems is necessary. For this purpose, we propose a model named qCCS. It is a natural quantum extension of classical value-passing CCS which can deal with input and output of quantum states, and unitary transformations and measurements on quantum systems. The operational semantics of qCCS is given in terms of probabilistic labeled transition system. This semantics has many different features compared with the proposals in the available literature in order to describe the input and output of quantum systems which are possibly correlated with other components. Based on this operational semantics, the notions of strong probabilistic bisimulation and weak probabilistic bisimulation between quantum processes are introduced. Furthermore, some properties of these two probabilistic bisimulations, such as congruence under various combinators, are examined.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
81P68 Quantum computation

Software:

QPL; qGCL
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Bennett, C. H., Quantum cryptography using any two nonorthogonal states, Physical Review Letters, 68, 3121 (1992) · Zbl 0969.94501
[2] C.H. Bennett, G. Brassard, Quantum cryptography: Public-key distribution and coin tossing, in: Proceedings of the IEEE International Conference on Computer, Systems and Signal Processing, Bangalore, India, 1984, pp. 175-179.; C.H. Bennett, G. Brassard, Quantum cryptography: Public-key distribution and coin tossing, in: Proceedings of the IEEE International Conference on Computer, Systems and Signal Processing, Bangalore, India, 1984, pp. 175-179. · Zbl 1306.81030
[3] Bennett, C. H.; Brassard, G.; Crepeau, C.; Jozsa, R.; Peres, A.; Wootters, W., Teleporting an unknown quantum state via dual classical and epr channels, Physical Review Letters, 70, 1895-1899 (1993) · Zbl 1051.81505
[4] Bennett, C. H.; Wiesner, S. J., Communication via one- and two-particle operators on einstein-podolsky-rosen states, Physical Review Letters, 69, 20, 2881-2884 (1992) · Zbl 0968.81506
[5] Bettelli, S.; Calarco, T.; Serafini, L., Toward an architecture for quantum programming, European Physical Journal D, 25, 2, 181-200 (2003)
[6] Bussey, P. J., Communication and non-communication in einstein-rosen experiments, Physics Letters A, 123, 1-3 (1987)
[7] Ekert, A. K., Quantum cryptography based on bell’s theorem, Physical Review Letters, 67, 661 (1991) · Zbl 0990.94509
[8] Feynman, R., Simulating physics with computers, International Journal of Theoretical Physics, 21, 467-488 (1982)
[9] Gay, S. J., Quantum programming languages: survey and bibliography, Mathematical Structures in Computer Science, 16, 04, 581-600 (2006) · Zbl 1122.68021
[10] S.J. Gay, R. Nagarajan, Communicating quantum processes, in: J. Palsberg, M. Abadi (Eds.), Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2005, pp. 145-157.; S.J. Gay, R. Nagarajan, Communicating quantum processes, in: J. Palsberg, M. Abadi (Eds.), Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2005, pp. 145-157. · Zbl 1369.68207
[11] Ghirardi, G. C.; Weber, T., Quantum mechanics and faster-than-light communication methodological considerations, Nuovo Cimento B, 11, 78 B, 9-20 (1983)
[12] L.K. Grover, A fast quantum mechanical algorithm for database search, in: Proceedings of ACM STOC, 1996, pp. 212-219.; L.K. Grover, A fast quantum mechanical algorithm for database search, in: Proceedings of ACM STOC, 1996, pp. 212-219. · Zbl 0922.68044
[13] Grover, L. K., Quantum mechanics helps in searching for a needle in a haystack, Physical Review Letters, 78, 2, 325 (1997)
[14] Hennessy, M., A proof system for communicating processes with value-passing, Formal Aspects of Computer Science, 3, 346-366 (1991) · Zbl 0736.68057
[15] Hennessy, M.; Ingólfsdóttir, A., A theory of communicating processes value-passing, Information and Computation, 107, 2, 202-236 (1993) · Zbl 0794.68098
[16] P. Jorrand, M. Lalire, Toward a quantum process algebra, in: P. Selinger (Ed.), Proceedings of the 2nd International Workshop on Quantum Programming Languages, 2004, p. 111.; P. Jorrand, M. Lalire, Toward a quantum process algebra, in: P. Selinger (Ed.), Proceedings of the 2nd International Workshop on Quantum Programming Languages, 2004, p. 111.
[17] E.H. Knill, Conventions for quantum pseudocode, LANL report LAUR-96-2724, 1996.; E.H. Knill, Conventions for quantum pseudocode, LANL report LAUR-96-2724, 1996.
[18] Kraus, K., States, Effects and Operations: Fundamental Notions of Quantum Theory (1983), Springer: Springer Berlin
[19] Marie Lalire, A probabilistic branching bisimulation for quantum processes, 2005. arxiv:quant-ph/0508116v1; Marie Lalire, A probabilistic branching bisimulation for quantum processes, 2005. arxiv:quant-ph/0508116v1
[20] Lalire, Marie, Relations among quantum processes: Bisimilarity and congruence, Mathematical Structures in Computer Science, 16, 3, 407-428 (2006) · Zbl 1122.68060
[21] Larsen, K.; Skou, A., Bisimulation through probabilistic testing, Information and Computation, 94, 456-471 (1991) · Zbl 0756.68035
[22] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, parts i and ii, Information and Computation, 100, 1-77 (1992)
[23] Nielsen, M., Conditions for a class of entanglement transformations, Physical Review Letters, 83, 436-439 (1999)
[24] Nielsen, Michael; Chuang, Isaac, Quantum computation and quantum information (2000), Cambridge University Press · Zbl 1049.81015
[25] B. Ömer, A procedural formalism for quantum computing. Master thesis, Department of Theoretical Physics, Technical University of Vienna, 1998. <http://tph.tuwien.ac.at/oemer/qcl.html; B. Ömer, A procedural formalism for quantum computing. Master thesis, Department of Theoretical Physics, Technical University of Vienna, 1998. <http://tph.tuwien.ac.at/oemer/qcl.html
[26] B. Ömer, Structured Quantum Programming, Ph.D. thesis, Department of Theoretical Physics, Technical University of Vienna, 2003.; B. Ömer, Structured Quantum Programming, Ph.D. thesis, Department of Theoretical Physics, Technical University of Vienna, 2003.
[27] A. Poppe, A. Fedrizzi, T. Lorunser, O. Maurhardt, R. Ursin, H.R. Bohm, M. Peev, M. Suda, C. Kurtsiefer, H. Weinfurter, T. Jennewein, A. Zeilinger, Practical quantum key distribution with polarization entangled photons, 2004. arxiv:quant-ph/0404115; A. Poppe, A. Fedrizzi, T. Lorunser, O. Maurhardt, R. Ursin, H.R. Bohm, M. Peev, M. Suda, C. Kurtsiefer, H. Weinfurter, T. Jennewein, A. Zeilinger, Practical quantum key distribution with polarization entangled photons, 2004. arxiv:quant-ph/0404115
[28] Sanders, J. W.; Zuliani, P., Quantum programming, Mathematics of Program Construction, 1837, 80-99 (2000) · Zbl 0963.68037
[29] R. Segala, N. Lynch, Probabilistic simulations for probabilitsic processes, in: Proceedings of CONCUR’94, Theories of Concurrency Unification and Extension, Lecture Notes in Computer Science, vol. 836, 1994, pp. 481-496.; R. Segala, N. Lynch, Probabilistic simulations for probabilitsic processes, in: Proceedings of CONCUR’94, Theories of Concurrency Unification and Extension, Lecture Notes in Computer Science, vol. 836, 1994, pp. 481-496.
[30] Segala, R.; Lynch, N., Probabilistic simulations for probabilistic processes, Nordic Journal of Computing, 2, 2, 250-273 (1995) · Zbl 0839.68067
[31] Selinger, P., A brief survey of quantum programming languages, Functional and Logic Programming, 2998, 1-6 (2004) · Zbl 1122.68359
[32] Selinger, P., Towards a quantum programming language, Mathematical Structures in Computer Science, 14, 4, 527-586 (2004) · Zbl 1085.68014
[33] Peter W. Shor, Algorithms for quantum computation: discrete log and factoring, in: Proceedings of the 35th IEEE FOCS, 1994, pp. 124-134.; Peter W. Shor, Algorithms for quantum computation: discrete log and factoring, in: Proceedings of the 35th IEEE FOCS, 1994, pp. 124-134.
[34] von Neumann, J., Mathematical Foundations of Quantum Mechanics (1955), Princeton University Press: Princeton University Press Princeton, NJ
[35] Wootters, W. K.; Zurek, W. H., A single quantum cannot be cloned, Nature, 299, 5886, 802-803 (1982) · Zbl 1369.81022
[36] M.S. Ying, M. Wirsing, Approximate bisimilarity, in: T. Rus (Ed.), Algebraic Methodology and Software Technology, 8th International Conference, Lecture Notes in Computer Science, vol. 1816, Iowa City, USA, 2000, pp. 309-321.; M.S. Ying, M. Wirsing, Approximate bisimilarity, in: T. Rus (Ed.), Algebraic Methodology and Software Technology, 8th International Conference, Lecture Notes in Computer Science, vol. 1816, Iowa City, USA, 2000, pp. 309-321. · Zbl 0983.68131
[37] Ying, M. S., Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs (2001), Springer-Verlag: Springer-Verlag New York · Zbl 0971.68111
[38] Ying, M. S., Additive models of probabilistic processes, Theoretical Computer Science, 275, 481-519 (2002) · Zbl 1026.68100
[39] P. Zuliani, Quantum Programming, Ph.D. thesis, Oxford University, 2001.; P. Zuliani, Quantum Programming, Ph.D. thesis, Oxford University, 2001. · Zbl 1277.68061
[40] P. Zuliani, Quantum programming with mixed states, in: Proceedings of the 3rd International Workshop on Quantum Programming Languages, Chicago, 2005.; P. Zuliani, Quantum programming with mixed states, in: Proceedings of the 3rd International Workshop on Quantum Programming Languages, Chicago, 2005. · Zbl 1277.68061
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.