Skip to main content
SpringerLink
Log in

Equational Reasoning About Quantum Protocols

  • Conference paper
  • First Online:
Reversible Computation (RC 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9138))

Included in the following conference series:

  • 761 Accesses

Abstract

Communicating Quantum Processes (CQP) is a quantum process calculus that applies formal techniques from classical computer science to concurrent and communicating systems that combine quantum and classical computation. By employing the theory of behavioural equivalence between processes, it is possible to verify the correctness of a system in CQP. The equational theory of CQP helps us to analyse quantum systems by reducing the need to explicitly construct bisimulation relations. We add three new equational axioms to the existing equational theory of CQP, which helps us to analyse various quantum protocols by proving that the implementation and specification are equivalent. We summarise the necessary theory and demonstrate its application in the analysis of quantum secret sharing. Also, we illustrate the approach by verifying other interesting and important practical quantum protocols such as superdense coding, quantum error correction and remote CNOT.

Supported by a Lord Kelvin/Adam Smith Scholarship from the University of Glasgow.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Verification of concurrent quantum protocols by equivalence checking. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 500–514. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  2. Davidson, T.A.S.: Formal Verification Techniques using Quantum Process Calculus. Ph.D thesis, University of Warwick (2011)

    Google Scholar 

  3. Davidson, T.A.S., Gay, S.J., Nagarajan, R., Puthoor, I.V.: Analysis of a quantum error correcting code using quantum process calculus. In: Proceedings of the International Workshop on QPL, vol. 95, pp. 67–80. EPTCS (2011)

    Google Scholar 

  4. Feng, Y., Duan, R., Ji, Z., Ying, M.: Probabilistic bisimilarities between quantum processes (2006). arXiv:cs.LO/0601014

  5. Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. In: ACM Symposium on Principles of Programming Languages, pp. 523–534. ACM (2011)

    Google Scholar 

  6. Franke-Arnold, S., Gay, S.J., Puthoor, I.V.: Quantum process calculus for linear optical quantum computing. In: Dueck, G.W., Miller, D.M. (eds.) RC 2013. LNCS, vol. 7948, pp. 234–246. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  7. Franke-Arnold, S., Gay, S.J., Puthoor, I.V.: Verification of linear optical quantum computing using quantum process calculus. In: Proceedings of the Combined International Workshop on Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS), vol. 160, pp. 111–129. EPTCS (2014)

    Google Scholar 

  8. Gay, S., Nagarajan, R.: Communicating Quantum Processes. In: ACM Symposium on Principles of Programming Languages, pp. 145–157. ACM (2005)

    Google Scholar 

  9. Gay, S.J., Nagarajan, R.: Types and Typechecking for Communicating Quantum Processes. Mathematical Structures in Computer Science 16(3), 375–406 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  10. Gay, S.J., Nagarajan, R., Papanikolaou, N.: QMC: a model checker for quantum systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 543–547. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Hillery, M., Buzek, V., Berthiaume, A.: Quantum secret sharing. Phys. Rev. A 59, 1829–1834 (1999)

    Article  MathSciNet  Google Scholar 

  12. IDQ. http://www.idquantique.com/company/presentation.html

  13. MagiQ. http://www.magiqtech.com/magiq/home.html

  14. Mayers, D.: Unconditional security in quantum cryptography. Journal of the ACM 48(3), 351–406 (2001)

    Article  MathSciNet  Google Scholar 

  15. Milner, R.: Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press (1999)

    Google Scholar 

  16. Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press (2000)

    Google Scholar 

  17. Puthoor, I.V.: Theory and applications of quantum process calculus. Ph.D thesis, University of Glasgow (2015)

    Google Scholar 

  18. Trčka, N., Georgievska, S.: Branching bisimulation congruence for probabilistic systems. Electronic Notes in Theoretical Computer Science 220(3), 129–143 (2008)

    Article  Google Scholar 

  19. Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  20. Zhou, X., Leung, D.W., Chuang, I.L.: Methodology for quantum logic gate construction. Phys. Rev. A 62 (2000)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computing Science, University of Glasgow, Glasgow, UK

    Simon J. Gay & Ittoop V. Puthoor

  2. School of Physics and Astronomy, University of Glasgow, Glasgow, UK

    Ittoop V. Puthoor

Authors
  1. Simon J. Gay
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ittoop V. Puthoor
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ittoop V. Puthoor .

Editor information

Editors and Affiliations

  1. CNRS and Université Paris Diderot, Paris, France

    Jean Krivine

  2. Inria, St. Ismier Cedex, France

    Jean-Bernard Stefani

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Gay, S.J., Puthoor, I.V. (2015). Equational Reasoning About Quantum Protocols. In: Krivine, J., Stefani, JB. (eds) Reversible Computation. RC 2015. Lecture Notes in Computer Science(), vol 9138. Springer, Cham. https://doi.org/10.1007/978-3-319-20860-2_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-20860-2_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-20859-6

  • Online ISBN: 978-3-319-20860-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation