Book contents
- Frontmatter
- Contents
- Contributors
- Preface
- 1 No-Cloning in Categorical Quantum Mechanics
- 2 Classical and Quantum Structuralism
- 3 Generalized Proof-Nets for Compact Categories with Biproducts
- 4 Quantum Lambda Calculus
- 5 The Quantum IO Monad
- 6 Abstract Interpretation Techniques for Quantum Computation
- 7 Extended Measurement Calculus
- 8 Predicate Transformer Semantics of Quantum Programs
- 9 The Structure of Partial Isometries
- 10 Temporal Logics for Reasoning about Quantum Systems
- 11 Specification and Verification of Quantum Protocols
- Index
- References
11 - Specification and Verification of Quantum Protocols
Published online by Cambridge University Press: 05 July 2014
- Frontmatter
- Contents
- Contributors
- Preface
- 1 No-Cloning in Categorical Quantum Mechanics
- 2 Classical and Quantum Structuralism
- 3 Generalized Proof-Nets for Compact Categories with Biproducts
- 4 Quantum Lambda Calculus
- 5 The Quantum IO Monad
- 6 Abstract Interpretation Techniques for Quantum Computation
- 7 Extended Measurement Calculus
- 8 Predicate Transformer Semantics of Quantum Programs
- 9 The Structure of Partial Isometries
- 10 Temporal Logics for Reasoning about Quantum Systems
- 11 Specification and Verification of Quantum Protocols
- Index
- References
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 - 472Publisher: Cambridge University PressPrint publication year: 2009
References
- 6
- Cited by