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 Workshop on Quantum Cryptography and Security (Lisbon Quantum Computation, Information and Logic Meetings Series: LQCIL’07), 2007.

Bibtex Entry:

@INPROCEEDINGS{Gay2007, author = {Simon Gay and Rajagopal Nagarajan and Nikolaos Papanikolaou}, title = {{QMC}: A Model Checker for Quantum Systems}, booktitle = {Proceedings of Workshop on Quantum Cryptography and Security (Lisbon Quantum Computation, Information and Logic Meetings Series: LQCIL'07)}, year = {2007}, address = { Lisbon, Portugal}, month = jul, 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-lqcil.pdf} }