Abstract
Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods such as formal logics for specification, formal modelling languages, separation of levels of abstraction, and compositional analysis. We argue that these techniques will be necessary for the analysis of large-scale systems that combine quantum and classical components. We summarize the results of our investigation using different approaches: behavioural equivalence in process calculus, model-checking and equivalence checking. Quantum teleportation is used as an example to illustrate our techniques.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits. Physical Review A 70, 052328 (2004)
Abramsky, S., Gay, S.J., Nagarajan, R.: Interaction categories and the foundations of typed concurrent programming. In: Broy, M. (ed.) Deductive Program Design: Proceedings of the 1994 Marktoberdorf International Summer School. NATO ASI Series F: Computer and Systems Sciences. Springer (1995)
Abramsky, S.: Interaction Categories (Extended Abstract). In: Burn, G.L., Gay, S.J., Ryan, M.D. (eds.) Theory and Formal Methods 1993: Proceedings of the First Imperial College Department of Computing Workshop on Theory and Formal Methods. Workshops in Computer Science, pp. 57–70. Springer (1993)
Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004), pp. 415–425. IEEE Computer Society (2004); Also arXiv:quant-ph/0402130
Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Equivalence checking of quantum protocols. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 478–492. Springer, Heidelberg (2013)
Baltazar, P., Chadha, R., Mateus, P.: Quantum computation tree logic – model checking and complete calculus. International Journal of Quantum Information 6(2), 219–236 (2008)
Baltazar, P., Chadha, R., Mateus, P., Sernadas, A.: Towards model-checking quantum security protocols. In: First International Conference on Quantum, Nano, and Micro Technologies, ICQNM. IEEE Computer Society (2007)
Bennett, C.H., Brassard, G., Crépeau, C., Jozsa, R., Peres, A., Wootters, W.K.: Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Physical Review Letters 70, 1895–1899 (1993)
Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: 42nd IEEE Symposium on Foundations of Computer Science, FOCS, pp. 136–145. IEEE Computer Society (2001)
Davidson, T., Gay, S.J., Mlnařík, H., Nagarajan, R., Papanikolaou, N.: Model checking for Communicating Quantum Processes. International Journal of Unconventional Computing 8(1), 73–98 (2012)
Davidson, T.A.S.: Formal Verification Techniques using Quantum Process Calculus. PhD thesis, University of Warwick (2011)
Emerson, E.A.: Temporal and modal logic, vol. B: Formal Models and Semantics, pp. 995–1072. MIT Press (1990)
Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. In: 38th ACM Symposium on Principles of Programming Languages, POPL. ACM (2011)
Feng, Y., Yu, N., Ying, M.: Model checking quantum Markov chains. arXiv:1205.2187 [quant-ph] (2012)
Feynman, R.P.: Simulating physics with computers. International Journal of Theoretical Physics 21(6-7), 467–488 (1982)
Gay, S.J., Mackie, I.C. (eds.): Semantic Techniques in Quantum Computation. Cambridge University Press (2010)
Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: 32nd ACM Symposium on Principles of Programming Languages, POPL, pp. 145–157 (2005); Also arXiv:quant-ph/0409052
Gay, S.J.: Stabilizer states as a basis for density matrices. arXiv:1112.2156 (2011)
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)
Gay, S.J., Papanikolaou, N., Nagarajan, R.: Specification and verification of quantum protocols. In: Semantic Techniques in Quantum Computation. Cambridge University Press (2010)
Gottesman, D.: Class of quantum error-correcting codes saturating the quantum Hamming bound. Physical Review A 54, 1862 (1996)
Grover, L.: A fast quantum mechanical algorithm for database search. In: 28th ACM Symposium on the Theory of Computation, STOC, pp. 212–219. ACM Press (1996)
Lalire, M.: Relations among quantum processes: bisimilarity and congruence. Mathematical Structures in Computer Science 16(3), 407–428 (2006)
Mateus, P., Sernadas, A.: Weakly complete axiomatization of exogenous quantum propositional logic. Information and Computation 204(5), 771–794 (2006)
Mayers, D.: Unconditional Security in Quantum Cryptography. Journal of the ACM 48(3), 351–406 (2001)
Nagarajan, R., Gay, S.J.: Formal verification of quantum protocols. arXiv:quant-ph/0203086 (March 2002)
Papanikolaou, N.K.: Model Checking Quantum Protocols. PhD thesis, University of Warwick (2009)
Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 14(4), 527–586 (2004)
Shor, P.W.: Algorithms for quantum computation: discrete logarithms and factoring. In: 35th IEEE Symposium on Foundations of Computer Science, FOCS (1994)
Trčka, N., Georgievska, S.: Branching bisimulation congruence for probabilistic systems. Electronic Notes in Theoretical Computer Science 220(3), 129–143 (2008)
Ying, M., Feng, Y., Duan, R., Ji, Z.: An algebra of quantum processes. ACM Transactions on Computational Logic 10(3), 19 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Gay, S.J., Nagarajan, R. (2013). Techniques for Formal Modelling and Analysis of Quantum Systems. In: Coecke, B., Ong, L., Panangaden, P. (eds) Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky. Lecture Notes in Computer Science, vol 7860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38164-5_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-38164-5_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38163-8
Online ISBN: 978-3-642-38164-5
eBook Packages: Computer ScienceComputer Science (R0)