Model Checking Quantum Protocols

by Nikolaos Papanikolaou
Abstract:
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.
Reference:
Model Checking Quantum Protocols (Nikolaos Papanikolaou), PhD thesis, Department of Computer Science, University of Warwick, 2009.
Bibtex Entry:
@PHDTHESIS{Papanikolaou2009,
  author = {Nikolaos Papanikolaou},
  title = {Model Checking Quantum Protocols},
  school = {Department of Computer Science, University of Warwick},
  year = {2009},
  abstract = {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.},
  owner = {Nick},
  timestamp = {2010.06.20},
  url = {../files/nphd.pdf}
}