Skip to main content
SpringerLink
Log in

Techniques for Formal Modelling and Analysis of Quantum Systems

  • Chapter
Book cover Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7860))

  • 1551 Accesses

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.

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. Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits. Physical Review A 70, 052328 (2004)

    Article  Google Scholar 

  2. 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)

    Google Scholar 

  3. 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)

    Google Scholar 

  4. 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

    Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. 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)

    Article  MATH  Google Scholar 

  7. 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)

    Google Scholar 

  8. 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)

    Article  MathSciNet  MATH  Google Scholar 

  9. 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)

    Google Scholar 

  10. 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)

    Google Scholar 

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

    Google Scholar 

  12. Emerson, E.A.: Temporal and modal logic, vol. B: Formal Models and Semantics, pp. 995–1072. MIT Press (1990)

    Google Scholar 

  13. Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. In: 38th ACM Symposium on Principles of Programming Languages, POPL. ACM (2011)

    Google Scholar 

  14. Feng, Y., Yu, N., Ying, M.: Model checking quantum Markov chains. arXiv:1205.2187 [quant-ph] (2012)

    Google Scholar 

  15. Feynman, R.P.: Simulating physics with computers. International Journal of Theoretical Physics 21(6-7), 467–488 (1982)

    Article  MathSciNet  Google Scholar 

  16. Gay, S.J., Mackie, I.C. (eds.): Semantic Techniques in Quantum Computation. Cambridge University Press (2010)

    Google Scholar 

  17. 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

    Google Scholar 

  18. Gay, S.J.: Stabilizer states as a basis for density matrices. arXiv:1112.2156 (2011)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  20. 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 

  21. Gay, S.J., Papanikolaou, N., Nagarajan, R.: Specification and verification of quantum protocols. In: Semantic Techniques in Quantum Computation. Cambridge University Press (2010)

    Google Scholar 

  22. Gottesman, D.: Class of quantum error-correcting codes saturating the quantum Hamming bound. Physical Review A 54, 1862 (1996)

    Article  MathSciNet  Google Scholar 

  23. 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)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  25. Mateus, P., Sernadas, A.: Weakly complete axiomatization of exogenous quantum propositional logic. Information and Computation 204(5), 771–794 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  26. Mayers, D.: Unconditional Security in Quantum Cryptography. Journal of the ACM 48(3), 351–406 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  27. Nagarajan, R., Gay, S.J.: Formal verification of quantum protocols. arXiv:quant-ph/0203086 (March 2002)

    Google Scholar 

  28. Papanikolaou, N.K.: Model Checking Quantum Protocols. PhD thesis, University of Warwick (2009)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  30. Shor, P.W.: Algorithms for quantum computation: discrete logarithms and factoring. In: 35th IEEE Symposium on Foundations of Computer Science, FOCS (1994)

    Google Scholar 

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

    Article  MATH  Google Scholar 

  32. Ying, M., Feng, Y., Duan, R., Ji, Z.: An algebra of quantum processes. ACM Transactions on Computational Logic 10(3), 19 (2009)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Simon J. Gay

  2. Department of Computer Science, School of Science and Technology, Middlesex University, London, UK

    Rajagopal Nagarajan

Authors
  1. Simon J. Gay
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rajagopal Nagarajan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Oxford, Parks Road, Wolfson Building, OX1 3QD, Oxford, UK

    Bob Coecke  & Luke Ong  & 

  2. Department of Computer Science, McGill University, 3480 Rue University, H3A 0E9, Montréal, QC, Canada

    Prakash Panangaden

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation