Model Checking for Verification of Quantum Circuits

TL;DR

This paper introduces a framework for verifying quantum circuits using model checking techniques, representing circuits as tensor networks and employing quantum logic assertions for simulation-based verification.

Contribution

It develops a novel assertion-based verification framework for quantum circuits using tensor network representations and extends model checking algorithms to quantum systems.

Findings

Quantum circuits modeled as tensor networks for verification.

Quantum assertions based on extended quantum logic.

Algorithms for reachability analysis using tensor contraction.

Abstract

In this talk, we will describe a framework for assertion-based verification (ABV) of quantum circuits by applying model checking techniques for quantum systems developed in our previous work, in which: (i) Noiseless and noisy quantum circuits are modelled as operator- and super-operator-valued transition systems, respectively, both of which can be further represented by tensor networks. (ii) Quantum assertions are specified by a temporal extension of Birkhoff-von Neumann quantum logic. Their semantics is defined based on the design decision: they will be used in verification of quantum circuits by simulation on classical computers or human reasoning rather than by quantum physics experiments (e.g. testing through measurements); (iii) Algorithms for reachability analysis and model checking of quantum circuits are developed based on contraction of tensor networks. We observe that many optimisation techniques for computing relational products used in BDD-based model checking algorithms can be generalised for contracting tensor networks of quantum circuits.