QMC: A Model Checker for Quantum Systems
| dc.creator | Gay, Simon | |
| dc.creator | Nagarajan, Rajagopal | |
| dc.creator | Papanikolaou, Nikolaos | |
| dc.date | 2007-04-27 | |
| dc.date | 2008-04-21 | |
| dc.date.accessioned | 2026-07-07T09:33:19Z | |
| dc.date.available | 2026-07-07T09:33:19Z | |
| dc.description | 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 quantum computational tree logic (QCTL). 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. | |
| dc.identifier | https://arxiv.org/abs/0704.3705 | |
| dc.identifier | http://arxiv.org/abs/0704.3705 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/159092 | |
| dc.subject | Quantum Physics | |
| dc.title | QMC: A Model Checker for Quantum Systems | |
| dc.type | text |