QRAT: A Reachability Analysis Tool for Quantum Programs
摘要
This paper introduces QRAT, the first reachability analysis tool for quantum programs, leveraging a state-of-the-art decision diagram developed in MQT Core for quantum computing. QRAT provides a novel framework for specifying quantum programs, defining their reachability properties, and searching for satisfied reachable states from an initial state, similar to the classical case. Experimental results demonstrate its effectiveness and practicality in verifying quantum programs. Since reachability analysis is a fundamental component of model-checking algorithms, QRAT represents an essential step toward the development of a full-fledged model checker for quantum programs.