QMC: A Model Checker for Quantum Systems

by Simon Gay, Rajagopal Nagarajan, Nikolaos Papanikolaou
Abstract:
We introduce a model-checking tool intended specially for the analysis of quantum information protocols. The tool incorporates an efficient representation of a certain class of quantum circuits, namely those expressible in the so-called stabiliser formalism. Models of protocols are described using a simple, imperative style simulation language which includes commands for the unitary operators in the Clifford group as well as classical integer and boolean variables. Formulas for verification are expressed using a subset of exogenous quantum propositional logic (EQPL). The model-checking procedure treats quantum measurements as the source of non-determinism, leading to multiple protocol runs, one for each outcome. Verification is performed for each run.
Reference:
QMC: A Model Checker for Quantum Systems (Simon Gay, Rajagopal Nagarajan, Nikolaos Papanikolaou), In Proceedings of 20textsuperscriptth International Conference on Automated Verification (CAV 2008), Springer, volume 5123, 2008.
Bibtex Entry:
@INPROCEEDINGS{Gay2008,
  author = {Simon Gay and Rajagopal Nagarajan and Nikolaos Papanikolaou},
  title = {{QMC}: A Model Checker for Quantum Systems},
  booktitle = {Proceedings of 20textsuperscript{th} International Conference on
	Automated Verification (CAV 2008)},
  year = {2008},
  volume = {5123},
  series = {Lecture Notes in Computer Science},
  address = {Princeton, NJ, USA},
  month = jul,
  publisher = {Springer},
  abstract = {We introduce a model-checking tool intended specially for the analysis
	of quantum information protocols. The tool incorporates an efficient
	representation of a certain class of quantum circuits, namely those
	expressible in the so-called stabiliser formalism. Models of protocols
	are described using a simple, imperative style simulation language
	which includes commands for the unitary operators in the Clifford
	group as well as classical integer and boolean variables. Formulas
	for verification are expressed using a subset of exogenous quantum
	propositional logic (EQPL). The model-checking procedure treats quantum
	measurements as the source of non-determinism, leading to multiple
	protocol runs, one for each outcome. Verification is performed for
	each run.},
  owner = {Nick},
  timestamp = {2010.06.20},
  url = {../files/gnp-cav.pdf}
}