research-article

Bisimulation for quantum processes

Authors:

Mingsheng YingAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 1

Pages 523 - 534

https://doi.org/10.1145/1925844.1926446

Published: 26 January 2011 Publication History

Abstract

Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the other hand, quantum protocol designers may commit much more faults than classical protocol designers since human intuition is much better adapted to the classical world than the quantum world. To offer formal techniques for modeling and verification of quantum protocols, several quantum extensions of process algebra have been proposed. One of the most serious issues in quantum process algebra is to discover a quantum generalization of the notion of bisimulation, which lies in a central position in process algebra, preserved by parallel composition in the presence of quantum entanglement, which has no counterpart in classical computation. Quite a few versions of bisimulation have been defined for quantum processes in the literature, but in the best case they are only proved to be preserved by parallel composition of purely quantum processes where no classical communications are involved.

Many quantum cryptographic protocols, however, employ the LOCC (Local Operations and Classical Communications) scheme, where classical communications must be explicitly specified. So, a notion of bisimulation preserved by parallel composition in the circumstance of both classical and quantum communications is crucial for process algebra approach to verification of quantum cryptographic protocols. In this paper we introduce a novel notion of bisimulation for quantum processes and prove that it is congruent with respect to various process algebra combinators including parallel composition even when both classical and quantum communications are present. We also establish some basic algebraic laws for this bisimulation. In particular, we prove uniqueness of the solutions to recursive equations of quantum processes, which provides a powerful proof technique for verifying complex quantum protocols.

Supplementary Material

MP4 File (48-mpeg-4.mp4)

Download
211.40 MB

References

[1]

M. Abadi and A. Gordon. A calculus for cryptographic protocols: the spi calculus, 1997.

[2]

C. Baier and M. Kwiatkowska. Domain equations for probabilistic processes. Mathematical Structure in Computer Science, 1999.

Digital Library

[3]

C. H. Bennett and S. J. Wiesner. Communication via one-and twoparticle operators on einstein-podolsky-rosen states. Physical Review Letters, 69(20):2881--2884, 1992.

[4]

C. H. Bennett, G. Brassard, C. Crepeau, R. Jozsa, A. Peres, and W.Wootters. Teleporting an unknown quantum state via dual classical and epr channels. Physical Review Letters, 70:1895--1899, 1993.

[5]

Y. Feng, R. Duan, Z. Ji, and M. Ying. Probabilistic bisimulations for quantum processes. Information and Computation, 205(11):1608--1639, 2007.

Digital Library

[6]

S. J. Gay and R. Nagarajan. Communicating quantum processes. In J. Palsberg and M. Abadi, editors, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 145--157, 2005.

Digital Library

[7]

L. K. Grover. Quantum mechanics helps in searching for a needle in a haystack. Physical Review Letters, 78(2):325, 1997.

[8]

M. Hennessy. A proof system for communicating processes with value-passing. Formal Aspects of Computer Science, 3:346--366, 1991.

Digital Library

[9]

M. Hennessy and A. Ingólfsdóttir. A theory of communicating processes value-passing. Information and Computation, 107(2):202--236, 1993.

Digital Library

[10]

P. Jorrand and M. Lalire. Toward a quantum process algebra. In P. Selinger, editor, Proceedings of the 2nd International Workshop on Quantum Programming Languages, 2004, page 111, 2004.

Digital Library

[11]

K. Kraus. States, Effects and Operations: Fundamental Notions of Quantum Theory. Springer, Berlin, 1983.

[12]

M. Lalire. Relations among quantum processes: Bisimilarity and congruence. Mathematical Structures in Computer Science, 16(3): 407--428, 2006.

Digital Library

[13]

R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts i and ii. Information and Computation, 100:1--77, 1992.

Digital Library

[14]

M. Nielsen and I. Chuang. Quantum computation and quantum information. Cambridge university press, 2000.

Digital Library

[15]

P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527--586, 2004.

Digital Library

[16]

P. W. Shor. Algorithms for quantum computation: discrete log and factoring. In Proceedings of the 35th IEEE FOCS, pages 124--134, 1994.

Digital Library

[17]

J. von Neumann. Mathematical Foundations of Quantum Mechanics. Princeton University Press, Princeton, NJ, 1955.

[18]

M. Ying, Y. Feng, R. Duan, and Z. Ji. An algebra of quantum processes. ACM Transactions on Computational Logic (TOCL), 10 :1--36, 2009.

Digital Library

Cited By

Qin XDeng YDu W(2020)Verifying Quantum Communication Protocols with Ground BisimulationTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-45237-7_2(21-38)Online publication date: 17-Apr-2020
https://doi.org/10.1007/978-3-030-45237-7_2
Díaz-Caro A(2017)A Lambda Calculus for Density Matrices with Classical and Probabilistic ControlsProgramming Languages and Systems10.1007/978-3-319-71237-6_22(448-467)Online publication date: 19-Nov-2017
https://doi.org/10.1007/978-3-319-71237-6_22
Kubota TKakutani YKato GKawano YSakurada H(2016)Semi-automated verification of security proofs of quantum cryptographic protocolsJournal of Symbolic Computation10.1016/j.jsc.2015.05.00173:C(192-220)Online publication date: 1-Mar-2016
https://dl.acm.org/doi/10.1016/j.jsc.2015.05.001
Show More Cited By

Index Terms

Bisimulation for quantum processes
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation

Recommendations

Bisimulation for Quantum Processes

Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the ...
An algebra of quantum processes

We introduce an algebra qCCS of pure quantum processes in which communications by moving quantum states physically are allowed and computations are modeled by super-operators, but no classical data is explicitly involved. An operational semantics of ...
Bisimulation for quantum processes
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 46, Issue 1

POPL '11

January 2011

624 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1925844

Issue’s Table of Contents

POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2011
652 pages
ISBN:9781450304900
DOI:10.1145/1926385
General Chair:
Thomas Ball
Microsoft Research, USA
,
Program Chair:
Mooly Sagiv
Tel Aviv University, Israel

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 January 2011

Published in SIGPLAN Volume 46, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

36
Total Citations
View Citations
636
Total Downloads

Downloads (Last 12 months)15
Downloads (Last 6 weeks)6

Reflects downloads up to 25 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Qin XDeng YDu W(2020)Verifying Quantum Communication Protocols with Ground BisimulationTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-45237-7_2(21-38)Online publication date: 17-Apr-2020
https://doi.org/10.1007/978-3-030-45237-7_2
Díaz-Caro A(2017)A Lambda Calculus for Density Matrices with Classical and Probabilistic ControlsProgramming Languages and Systems10.1007/978-3-319-71237-6_22(448-467)Online publication date: 19-Nov-2017
https://doi.org/10.1007/978-3-319-71237-6_22
Kubota TKakutani YKato GKawano YSakurada H(2016)Semi-automated verification of security proofs of quantum cryptographic protocolsJournal of Symbolic Computation10.1016/j.jsc.2015.05.00173:C(192-220)Online publication date: 1-Mar-2016
https://dl.acm.org/doi/10.1016/j.jsc.2015.05.001
Gay SPuthoor I(2015)Equational Reasoning About Quantum ProtocolsReversible Computation10.1007/978-3-319-20860-2_10(155-170)Online publication date: 20-Jun-2015
https://doi.org/10.1007/978-3-319-20860-2_10
Deng YFeng Y(2012)Open bisimulation for quantum processesProceedings of the 7th IFIP TC 1/WG 202 international conference on Theoretical Computer Science10.1007/978-3-642-33475-7_9(119-133)Online publication date: 26-Sep-2012
https://dl.acm.org/doi/10.1007/978-3-642-33475-7_9
Wu HYang QLong H(2024)Branching bisimulation semantics for quantum processesInformation Processing Letters10.1016/j.ipl.2024.106492186:COnline publication date: 1-Aug-2024
https://dl.acm.org/doi/10.1016/j.ipl.2024.106492
Mousavi MPeters KSchmitt A(2024)Towards a Formal Testing Theory for Quantum ProcessesLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_8(111-131)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-73709-1_8
Dai G(2019)Formal Verification for KMB09 ProtocolInternational Journal of Theoretical Physics10.1007/s10773-019-04232-258:11(3651-3657)Online publication date: 5-Aug-2019
https://doi.org/10.1007/s10773-019-04232-2
Wang Y(2019)Entanglement in Quantum Process AlgebraInternational Journal of Theoretical Physics10.1007/s10773-019-04226-058:11(3611-3626)Online publication date: 13-Aug-2019
https://doi.org/10.1007/s10773-019-04226-0
Wang Y(2019)Probabilistic Process Algebra to Unifying Quantum and Classical Computing in Closed SystemsInternational Journal of Theoretical Physics10.1007/s10773-019-04216-258:10(3436-3509)Online publication date: 5-Sep-2019
https://doi.org/10.1007/s10773-019-04216-2
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents