Symbolic Model Checking Quantum Circuits in Maude

This paper presents a symbolic approach to model checking quantum circuits by using a set of laws from quantum mechanics and basic matrix operations with Dirac notation.We use Maude, a high-level specification/programming language based on rewriting logic, to implement our symbolic approach.As a case study, we use the approach to formally specify and verify the correctness of the quantum teleportation protocol, which is an important quantum communication protocol in the early work of quantum communications.Moreover, our implementation can be used as a general framework to formally specify and verify quantum circuits in Maude in an effortless way, where only an initial quantum state and a sequence of actions describing how a quantum circuit works in a simple way are required.