# Towards a model-checker for quantum stabilizer protocols

## Nick Papanikolaou, University of Warwick

We will report on work-in-progress on developing a model-checking
tool for quantum communication protocols and quantum cryptographic
protocols. Our early experiments with probabilistic model checking
will be reviewed; then the general model-checking problem for
quantum protocols will be formalised and its complexity discussed.
This will naturally lead to the question of which protocols can be
efficiently simulated on a classical computer. An overview of the
stabilizer formalism will be given, followed by a summary of the
Aaronson-Gottesman algorithm for simulation of stabilizer
circuits. We will present QMC, a tool for automatically verifying
properties of such circuits; properties of protocols are expressed
using a subset of EQPL, a logic developed by Mateus and Sernadas. This
is joint work with Rajagopal Nagarajan (University of Warwick) and
Simon Gay (University of Glasgow)