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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
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)
Davidson, T.A.S.: Formal Verification Techniques using Quantum Process Calculus. Ph.D thesis, University of Warwick (2011)
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)
Feng, Y., Duan, R., Ji, Z., Ying, M.: Probabilistic bisimilarities between quantum processes (2006). arXiv:cs.LO/0601014
Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. In: ACM Symposium on Principles of Programming Languages, pp. 523–534. ACM (2011)
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)
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)
Gay, S., Nagarajan, R.: Communicating Quantum Processes. In: ACM Symposium on Principles of Programming Languages, pp. 145–157. ACM (2005)
Gay, S.J., Nagarajan, R.: Types and Typechecking for Communicating Quantum Processes. Mathematical Structures in Computer Science 16(3), 375–406 (2006)
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)
Hillery, M., Buzek, V., Berthiaume, A.: Quantum secret sharing. Phys. Rev. A 59, 1829–1834 (1999)
Mayers, D.: Unconditional security in quantum cryptography. Journal of the ACM 48(3), 351–406 (2001)
Milner, R.: Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press (1999)
Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press (2000)
Puthoor, I.V.: Theory and applications of quantum process calculus. Ph.D thesis, University of Glasgow (2015)
Trčka, N., Georgievska, S.: Branching bisimulation congruence for probabilistic systems. Electronic Notes in Theoretical Computer Science 220(3), 129–143 (2008)
Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)
Zhou, X., Leung, D.W., Chuang, I.L.: Methodology for quantum logic gate construction. Phys. Rev. A 62 (2000)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)