AI 中文总结
研究人员开发出首个针对Qiskit程序调试的量子模型检查器QisMC，基于量子-经典转换系统与qCTL构建，可实现自动化详尽验证并生成反例，经评估具备实用、高效及可扩展的特性。
AI 中文摘要
我们提出QisMC，这是首个专门用于调试Qiskit程序的量子模型检查器。理论层面，我们引入量子-经典转换系统的概念，以及基于伯克霍夫-冯·诺依曼逻辑的量子计算树逻辑（qCTL），分别用于建模Qiskit程序的行为和指定其属性。实现层面，QisMC提供端到端框架，涵盖转换系统生成、逻辑公式表示及模型检查算法，且基于决策图高效执行图像计算。这些方法与设计原则使QisMC相较于现有Qiskit程序调试器具备优势，包括统一的属性规范语言、完全自动化且详尽的验证流程，以及生成反例的能力。大量示例与基准评估表明，QisMC在验证实际量子程序方面具备实用性、高效性与可扩展性。
英文摘要
We present QisMC, the first quantum model checker dedicated to debugging Qiskit programs. On the theoretical side, we introduce the notion of quantum-classical transition system and a quantum computation tree logic (qCTL) grounded in Birkhoff-von Neumann logic for modeling the behaviors and specifying the properties of Qiskit programs, respectively. On the implementation side, QisMC provides an end-to-end framework encompassing transition system generation, logical formula representation, and model checking algorithms, and it efficiently performs image computation based on decision diagrams. These methods and design principles give QisMC advantages over previous Qiskit program debuggers, including a unified property specification language, a fully automated and exhaustive verification process, and the ability to generate counterexamples. Extensive illustrative examples and benchmark evaluations demonstrate the practicality, efficiency, and scalability of QisMC in verifying realistic quantum programs.
