Probabilistic Model-Checking of Quantum Protocols

by Simon Gay, Rajagopal Nagarajan, Nikolaos Papanikolaou
Abstract:
We establish fundamental and general techniques for formal verification of quantum protocols. Quantum protocols are novel communication schemes involving the use of quantum-mechanical phenomena for representation, storage and transmission of data. As opposed to quantum computers, quantum communication systems can and have been implemented using present-day technology; therefore, the ability to model and analyse such systems rigorously is of primary importance. While current analyses of quantum protocols use a traditional mathematical approach and require considerable understanding of the underlying physics, we argue that automated verification techniques provide an elegant alternative. We demonstrate these techniques through the use of PRISM, a probabilistic model-checking tool. Our approach is conceptually simpler than existing proofs, and allows us to disambiguate protocol definitions and assess their properties. It also facilitates detailed analyses of actual implemented systems. We illustrate our techniques by modelling a selection of quantum protocols (namely superdense coding, quantum teleportation, and quantum error correction) and verifying their basic correctness properties. Our results provide a foundation for further work on modelling and analysing larger systems such as those used for quantum cryptography, in which basic protocols are used as components.
Reference:
Probabilistic Model-Checking of Quantum Protocols (Simon Gay, Rajagopal Nagarajan, Nikolaos Papanikolaou), In Proceedings of 2textsuperscriptnd International Workshop on Developments on Computational Models (DCM 2006), 2006.
Bibtex Entry:
@INPROCEEDINGS{Gay2006,
  author = {Simon Gay and Rajagopal Nagarajan and Nikolaos Papanikolaou},
  title = {Probabilistic Model-Checking of Quantum Protocols},
  booktitle = { Proceedings of 2textsuperscript{nd} International Workshop on Developments
	on Computational Models (DCM 2006)},
  year = {2006},
  address = {San Servolo, Venice, Italy},
  month = jul,
  abstract = {We establish fundamental and general techniques for formal verification
	of quantum protocols. Quantum protocols are novel communication schemes
	involving the use of quantum-mechanical phenomena for representation,
	storage and transmission of data. As opposed to quantum computers,
	quantum communication systems can and have been implemented using
	present-day technology; therefore, the ability to model and analyse
	such systems rigorously is of primary importance.
	
	
	While current analyses of quantum protocols use a traditional mathematical
	approach and require considerable understanding of the underlying
	physics, we argue that automated verification techniques provide
	an elegant alternative. We demonstrate these techniques through the
	use of PRISM, a probabilistic model-checking tool. Our approach is
	conceptually simpler than existing proofs, and allows us to disambiguate
	protocol definitions and assess their properties. It also facilitates
	detailed analyses of actual implemented systems. We illustrate our
	techniques by modelling a selection of quantum protocols (namely
	superdense coding, quantum teleportation, and quantum error correction)
	and verifying their basic correctness properties. Our results provide
	a foundation for further work on modelling and analysing larger systems
	such as those used for quantum cryptography, in which basic protocols
	are used as components.},
  owner = {Nick},
  timestamp = {2010.06.20},
  url = {../files/dcmpaper.pdf}
}