Verifying Quantum Circuits with Level-Synchronized Tree Automata

We present a new method for the verification of quantum circuits based on a novel
symbolic representation of sets of quantum states using level-synchronized tree
automata (LSTAs). LSTAs extend classical tree automata by labeling each
transition with a set of choices, which are then used to synchronize subtrees of
an accepted tree. Compared to the traditional tree automata, LSTAs have an
incomparable expressive power while maintaining important properties, such as
closure under union and intersection, and decidable language emptiness
and inclusion. We have developed an efficient and fully automated symbolic
verification algorithm for quantum circuits based on LSTAs. The complexity of
supported gate operations is at most quadratic, dramatically improving the
exponential worst-case complexity of an earlier tree automata-based approach.
Furthermore, we show that LSTAs are a promising model for parameterized
verification, i.e., verifying the correctness of families of circuits with the
same structure for any number of qubits involved, which principally lies
beyond the capabilities of previous automated approaches. We implemented this
method as a C++ tool and compared it with three symbolic quantum circuit
verifiers and two simulators on several benchmark examples. The results show that
our approach can solve problems with sizes orders of magnitude larger than the
state of the art.