Specification and Verification of Quantum Protocols

by Simon J. Gay, Rajagopal Nagarajan, Nikolaos Papanikolaou
Abstract:
We describe model-checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of 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 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, the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to number of case studies, including quantum teleportation and BB84 quantum coin-flipping protocol.
Reference:
Specification and Verification of Quantum Protocols (Simon J. Gay, Rajagopal Nagarajan, Nikolaos Papanikolaou), Chapter in Semantic Techniques in Quantum Computation (S.J. Gay, I. Mackie, eds.), Cambridge University Press, 2010.
Bibtex Entry:
@INCOLLECTION{Gay2010,
  author = {Simon J. Gay and Rajagopal Nagarajan and Nikolaos Papanikolaou},
  title = {Specification and Verification of Quantum Protocols},
  booktitle = {Semantic Techniques in Quantum Computation},
  publisher = {Cambridge University Press},
  year = {2010},
  editor = {S.J. Gay and I. Mackie},
  chapter = {11},
  abstract = {We describe model-checking techniques for protocols arising in quantum
	information theory and quantum cryptography. We discuss the theory
	and implementation of 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 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, the verification algorithms that have been implemented
	in the tool. We demonstrate our techniques with applications to number
	of case studies, including quantum teleportation and BB84 quantum
	coin-flipping protocol.},
  owner = {Nick},
  timestamp = {2010.06.20},
  url = {http://www.amazon.co.uk/Semantic-Techniques-Quantum-Computation-Simon/dp/052151374X/ref=sr_1_10?ie=UTF8&s=books&qid=1243948315&sr=1-10}
}