Equivalence Checking of Quantum Circuits Based on Dirac Notation in Maude

This paper presents an approach to checking the equivalence of quantum circuits based on Dirac notation in Maude. Specifically, we specify quantum states and quantum gates in Dirac notation with scalars and use a set of laws from quantum mechanics and matrix operations to reason about quantum computation. The equivalence of quantum circuits can be reduced to matrix equivalence modulo a global phase in Dirac notation. To achieve this, we compare each column vector of two matrices with respect to the same global phase, making it faster than the actual matrix equivalence check, especially in cases of non-equivalent quantum circuits. Furthermore, our approach enhances the reliability in determining the equivalence problem by taking into account constant inputs for quantum circuits, which have been ignored by state-of-the-art tools. We use Maude, a high-level specification/programming language based on rewriting logic, to develop a support tool called \( \left| \mathrm{{QCEC}} \right\rangle \) for our approach. Several case studies have been conducted with the tool. These demonstrate the effectiveness of our approach and \( \left| \mathrm{{QCEC}} \right\rangle \) for the equivalence checking of quantum circuits.