Skip to main content Accessibility help

We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.

Close cookie message
×
Hostname: page-component-745bb68f8f-5r2nc Total loading time: 0 Render date: 2025-02-06T19:10:39.428Z Has data issue: false hasContentIssue false

11 - Specification and Verification of Quantum Protocols

Published online by Cambridge University Press:  05 July 2014

By
Simon J. Gay ,
Rajagopal Nagarajan  and
Nikolaos Papanikolaou
Edited by
Simon Gay  and
Ian Mackie
Simon J. Gay
Affiliation:
University of Glasgow
Rajagopal Nagarajan
Affiliation:
University of Warwick
Nikolaos Papanikolaou
Affiliation:
University of Warwick
Simon Gay
Affiliation:
University of Glasgow
Ian Mackie
Affiliation:
Imperial College London
Get access

Summary

Abstract

We describe model-checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of a practical model checker, QMC, for quantum protocols. In our framework, we assume that the quantum operations performed in a protocol are restricted to those within the stabilizer formalism; while this particular set of operations is not universal for quantum computation, it allows us to develop models of several useful protocols as well as of systems involving both classical and quantum information processing. We discuss the modeling language of QMC, the logic used for verification, and the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to a number of case studies, including quantum teleportation and the BB84 quantum coin-flipping protocol.

11.1 Introduction

Model-checking is a method of computer-aided verification used widely in both academia and industry for the analysis of software and communication systems. The method essentially consists of three phases: (1) modeling the system of interest at a suitable level of abstraction, usually by describing it in a formal specification language; (2) specifying the properties that the system must satisfy – these properties are typically expressed with reference to the system model, using a logic designed specially for this purpose (e.g., linear or branching time temporal logic); and (3) supplying the model and the properties to a model-checking tool, which automatically constructs the state space of the model and checks whether or not the given properties are satisfied (and if not, usually providing a counterexample).

Type
Chapter
Information
Semantic Techniques in Quantum Computation , pp. 414 - 472
Publisher: Cambridge University Press
Print publication year: 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aaronson, S. (2004) The complexity zoo. http://qwiki.caltech.edu/wiki/Complexity_Zoo.Google Scholar
Aaronson, S., and Gottesman, D. (2004) Improved simulation of stabilizer circuits. Physical Review A 70:52328.CrossRefGoogle Scholar
Abramsky, S. (2004) High-level methods for quantum computation and information. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society.Google Scholar
Abramsky, S., and Coecke, B. (2003) Physical traces: Quantum vs. classical information processing. Electronic Notes in Theoretical Computer Science 69:1–22. Also arXiv:cs/0207057v2 [cs.CG].CrossRefGoogle Scholar
Abramsky, S., and Coecke, B. (2004) A categorical semantics of quantum protocols. In Proceedings ofthe 19th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society. Also arXiv:quant-ph/0402130v5.Google Scholar
Abramsky, S., and Coecke, B. (2005) Abstract physical traces. Theory and Applications of Categories 14(6):111–124.Google Scholar
Audenaert, K. M. R., and Plenio, M. B. (2005) Entanglement on mixed stabiliser states: Normal forms and reduction procedures. New Journal of Physics 7:170.CrossRefGoogle Scholar
Bacon, D. (2006) Stabilizer quantum error correcting codes. Lecture Notes for course CSE 599d (Quantum Computing), University of Washington.Google Scholar
Baltazar, P, Chadha, R., and Mateus, P. (2008) Quantum computation tree logic - model checking and complete calculus. International Journal of Quantum Information 6(2):219–236.CrossRefGoogle Scholar
Bennett, C. H., and Brassard, G. (1984) Quantum cryptography: Public key distribution and coin tossing. In Proceedings of International Conference on Computers, Systems and Signal Processing.Google Scholar
Bennett, C. H., Brassard, G., Crepeau, C., Jozsa, R., Peres, A., and Wootters, W. K. (1993) Tele-porting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Physical Review Letters 70:1895–1899.CrossRefGoogle ScholarPubMed
Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., and McKenzie, P. (1999) Systems and Software Verification: Model-Checking Techniques and Tools. Springer.Google Scholar
Bouwmeester, D., Ekert, A., and Zeilinger, A., editors (2000) The Physics of Quantum Information. Springer.CrossRefGoogle Scholar
Cardelli, L. (2004) Type systems. In CRC Handbook of Computer Science and Engineering, chapter 97. CRC Press, second edition.Google Scholar
Cleaveland, R., Parrow, J., and Steffen, B. (1993) The concurrency workbench: A semantics-based tool for the verification of finite-state systems.Google Scholar
Coecke, B. (2004a) The logic of entanglement. arXiv:quant-ph/0402014v2.Google Scholar
Coecke, B. (2004b) Quantum information-flow, concretely, abstractly. In Selinger, P., editor, Proceedings of the 2nd International Workshop on Quantum Programming Languages. Turku Centre for Computer Science.Google Scholar
Danos, V, and D'Hondt, E. (2008) Classical knowledge for quantum cryptographic reasoning. Electronic Notes in Theoretical Computer Science 192(3):39–58.CrossRefGoogle Scholar
D'Hondt, E., and Panangaden, P. (2005) Reasoning about quantum knowledge. In Ramanujam, R., and Sen, S., editors, Proceedings of the 25th Conference on Foundations of Software Technology and Theoretical Computer Science, volume 3821 of Lecture Notes in Computer Science, pages 553–564. Springer.Google Scholar
Dijkstra, E. W. (1976) A Discipline of Programming. Prentice-Hall.Google Scholar
Ekert, A. (1991) Quantum cryptography based on Bell's theorem. Physical Review Letters 67(6):661–663.CrossRefGoogle ScholarPubMed
Emerson, E. A. (1990) Temporal and modal logic. In Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics, pages 995–1072. MIT Press.Google Scholar
Gagnon, E. (1998) SableCC, An Object-Oriented Compiler Framework. Master's thesis, School of Computer Science, McGill University, Montreal.CrossRefGoogle Scholar
Gansner, E. R., and North, S. C. (2000) An open graph visualization system and its applications to software engineering. Software Practice and Experience 30(11):1203–1233.3.0.CO;2-N>CrossRefGoogle Scholar
Gay, S. J. (2006) Quantum programming languages: survey and bibliography. Mathematical Structures in Computer Science 16(4):581–600.CrossRefGoogle Scholar
Gay, S. J., and Nagarajan, R. (2005) Communicating quantum processes. In Proceedings ofthe 32nd ACM SIGPLAN-SIGACTSymposium on Principles of Programming Languages, pages 145–157. ACM Press.Google Scholar
Gay, S. J., Nagarajan, R., and Papanikolaou, N. (2005) Probabilistic model-checking of quantum protocols. arXiv:quant-ph/0504007v2.Google Scholar
Gay, S. J., Nagarajan, R., and Papanikolaou, N. (2008) QMC: A model checker for quantum systems. In Proceedings of the 20th International Conference on Computer Aided Verification, volume 5123 of Lecture Notes in Computer Science, pages 543–547. Springer.Google Scholar
Gottesman, D. (1999) The Heisenberg representation of quantum computers. In Corney, S. P., Delbourgo, R. and Jarvis, P D., editors, Group22: Proceedings of the XXII International Colloquium on Group Theoretical Methods in Physics. International Press.Google Scholar
Gottesman, D. (2002) An introduction to quantum error correction. In Lomonaco, S. J. Jr. editor, Quantum Computation: A Grand Mathematical Challenge for the Twenty-First Century and the Millennium. American Mathematical Society.Google Scholar
Hoare, C. A. R. (1985) Communicating Sequential Processes. Prentice-Hall.Google Scholar
Holzmann, G. (1991) The Design and Validation ofComputer Protocols. Prentice-Hall.Google Scholar
Holzmann, G. (2003) The SPINModel Checker: Primer and Reference Manual. Pearson Education.Google Scholar
Huth, M. R. A., and Ryan, M. D. (2004) Logic in Computer Science: Modeling and Reasoning about Systems. Cambridge University Press, second edition.CrossRefGoogle Scholar
Jorrand, P., and Lalire, M. (2004) Toward a quantum process algebra. In Proceedings ofthe 1st ACM Conference on Computing Frontiers. ACM Press. Also arXiv:quant-ph/0312067v1.Google Scholar
Jorrand, P., and Lalire, M. (2005) From quantum physics to programming languages: A process algebraic approach. In Unconventional Programming Paradigms: Revised Selected and Invited Papers from the International Workshop UPP 2004, volume 3566 of Lecture Notes in Computer Science. Springer.Google Scholar
Kwiatkowska, M., Norman, G., and Parker, D. (2004) Probabilistic symbolic model checking with PRISM: a hybrid approach. International Journal on Software Tools for Technology Transfer (STTT) 6(2):128–142.Google Scholar
Mateus, P., and Sernadas, A. (2004a) Exogenous quantum logic. In Carnielli, W. A., Dionísio, F. M., and Mateus, P., editors, Proceedings of CombLog'04 – Workshop on Combination of Logics: Theory and Applications, pages 141–150. IST Press, Lisbon.Google Scholar
Mateus, P., and Sernadas, A. (2004b) Reasoning about quantum systems. In Proceedings of Ninth European Conference on Logics in Artificial Intelligence, pages 239–251. Springer.Google Scholar
Mateus, P., and Sernadas, A. (2006) Weakly complete axiomatization of exogenous quantum propositional logic. Information and Computation 204(5):771–794.CrossRefGoogle Scholar
Mayers, D. (2001) Unconditional security in quantum cryptography. Journal ofthe ACM 48(3):351–406.Google Scholar
Milner, R. (1989) Communication and Concurrency. Prentice-Hall.Google Scholar
Nielsen, M. A., and Chuang, I. L. (2000) Quantum Computation and Quantum Information. Cambridge University Press.Google Scholar
Ömer, B. (1998) A Procedural Formalism for Quantum Computing. Master's thesis, Department of Theoretical Physics, University of Vienna.Google Scholar
Ömer, B. (2000) Quantum Programming in QCL. Master's thesis, Institute of Information Systems, Technical University of Vienna.Google Scholar
Papanikolaou, N. (2005a) Reasoning formally about quantum systems: an overview. ACM SIGACTNews 36(3):51–66.Google Scholar
Papanikolaou, N. (2005b) Techniques for Design and Validation of Quantum Protocols. Master's thesis, Department of Computer Science, University of Warwick. Also available as Research Report CS-RT-413.Google Scholar
Perdrix, S. (2008) Quantum entanglement analysis based on abstract interpretation. In Proceedings ofthe 15th International Static Analysis Symposium, volume 5079 of Lecture Notes in Computer Science, pages 270–282. Springer. Also arXiv:0801.4230v1 [cs.LO].Google Scholar
Pietriga, E. (2005) A toolkit for addressing HCI issues in visual language environments. In Proceedings ofthe IEEE Symposium on Visual Languages and Human-Centric Computing, pages 145–152. IEEE Computer Society.Google Scholar
Prost, F., and Zerrari, C. (2008) A logical analysis of entanglement and separability in quantum higher-order functions. arXiv:0801.0649v1 [cs.LO].Google Scholar
Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., and Roscoe, B. (2001) Modelling and Analysis of Security Protocols. Pearson Education.Google Scholar
Sadrzadeh, M. (2006) Actions and Resources in Epistemic Logic. Ph.D. thesis, Universite du Quebec, Montreal, Canada.Google Scholar
Sanders, J., and Zuliani, P. (2000) Quantum programming. In Mathematics of Program Construction, pages 80–99. Volume 1837 of Lecture Notes in Computer Science. Springer.Google Scholar
Selinger, P. (2004) Towards a quantum programming language. Mathematical Structures in Computer Science 14(4):527–586.CrossRefGoogle Scholar
Steane, A. M. (2000) Quantum computing and error correction. In Gonis, A., and Turchi, P., editors, Proceedings ofthe NATO Advanced Research Workshop, pages 284–298. IOS Press.Google Scholar
Sun Microsystems, Inc. (2006) Java platform standard edition 6 sdk. http://java.sun.com/ javase/6/docs/.
van Tonder, A. (2004) A lambda calculus for quantum computation. SIAM Journal on Computing 33(5):1109–1135. Also arXiv:quant-ph/0307150v5.CrossRefGoogle Scholar
Wirth, N. (1971) The programming language Pascal. Acta Informatica 1:35–63.CrossRefGoogle Scholar
Wootters, W. K., and Zurek, W. H. (1982) A single quantum cannot be cloned. Nature 299:802803.CrossRefGoogle Scholar

Save book to Kindle

To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.

Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.

Find out more about the Kindle Personal Document Service.

Available formats
×

Save book to Dropbox

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.

Available formats
×

Save book to Google Drive

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.

Available formats
×