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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

QRAT: A Reachability Analysis Tool for Quantum Programs

  • Canh Minh Do,
  • Kazuhiro Ogata

摘要

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.