Technology Introduction:
We model quantum states as perfect binary trees and utilize tree automata to recognize large sets of such trees, allowing us to compactly represent collections of quantum states. Based on this novel approach, we design efficient algorithms for simulating quantum gates, enabling fast and scalable quantum circuit verification. Our method supports common quantum gates and control flow constructs.
Industry Applicability:
Our tool can be used to verify quantum circuit correctness before deployment and check circuit equivalence before and after compiler optimizations, supporting deployment platforms like IBM Qiskit. We can also develop an interactive, visual interface for quantum state preparation and gate operations like Frama-C. It can also be used to aid education by letting students compare circuits intuitively.