Software

This section is devoted to the software Nick developed as part of his PhD, namely, the Quantum Model Checker (QMC). You will find here a description of the tool and:

QMC is a tool that automatically explores all possible behaviours arising from a quantum protocol description expressed in QMCLANG and enables QCTL properties to be checked over the resulting structure. Quantum protocols include only Clifford group operations on stabilizer states.

The QMC tool has three main components: (1) a process scheduler, (2) a language interpreter, and (3) a model checker. The role of component (1) is essentially to perform the tasks described in the previous paragraph. The language interpreter handles the execution of individual commands and keeps track of the overall classical and quantum state at each step. Finally, the verifier is responsible for evaluating QCTL formulae over the structure generated by (1) and (2). QMC has a graphical user interface which includes a user–friendly editor for models and properties.

A protocol model consists of definitions of one or more processes. The commands performed by these processes are interleaved, in order to simulate concurrent execution. Nondeterministic choices are resolved in all possible ways, producing a tree of all possible executions of the protocol.

QMC provides an interface to the GraphViz graph layout tool, and the ZGRVIEWER application, which can display the program execution tree.

Given a model and a QCTL formula for verification, QMC outputs the following:

  • a summary of the files provided as input and basic feedback on the model provided including the number of states and the total number of runs,
  • a verification result for the formula provided,
  • a list of states (if any) that serve as counter-examples to the formula,
  • a prompt which allows the user to track individual states and trace runs of interest, as well as to verify further formulae.