QMC: A Model Checker for Quantum Systems

TL;DR

This paper presents QMC, a model checker tailored for quantum information protocols, leveraging stabiliser formalism and quantum logic to verify quantum protocols efficiently through simulation and non-deterministic analysis.

Contribution

Introduces QMC, a novel model checking tool for quantum systems that uses stabiliser formalism and a specialized logic for protocol verification.

Findings

Efficient representation of stabiliser circuits

Verification of quantum protocols with non-determinism

Supports classical and quantum variables in modeling

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 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.