Summary
This thesis describes 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 detail the syntax, semantics and type system of QMC’s modelling language, the logic QCTL which is 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.
Read More ↓Edition Statements
- Publication Date:2009
Thesis Information
- Degree:Ph.D.
- University:University of Warwick
Publication Statements
- Language:eng
- Publication Date:2009
Edition Identifiers
- ethos:505020
Subjects
Writers
No reviews yet. Be the first to rate this work.
Rate & Review