Abstract
We present a new method for analyzing and identifying errors in quantum circuits. In our approach, we define the problem using a triple {P}C{Q}, where the task is to determine whether a given set P of quantum states at the input of a circuit C produces a set of quantum states at the output that is equal to, or included in, a set Q. We propose a technique that utilizes tree automata to efficiently represent sets of quantum states, and we develop algorithms to apply the operations of quantum gates within this representation. Our work creates a link between quantum program verification and automata, introducing new possibilities for leveraging automata theory and automata-based verification in the field of quantum computing. To enhance the effectiveness of this approach, we introduce a new model of tree automata called Level-synchronized tree automata (LSTAs), which extends classical tree automata by labeling each transition with a set of "choices" to synchronize subtrees of an accepted tree. This new model enables more efficient gate operations compared to classical tree automata. Additionally, we discuss our efforts to extend the framework from verifying quantum circuits to verifying quantum programs.