QReach：量子马尔可夫链的可达性分析工具
QReach: A Reachability Analysis Tool for Quantum Markov Chains
AI总结：
QReach是一种基于CFLOBDD的量子马尔可夫链可达性分析工具，通过新的框架和模型检查子过程提升量子电路和算法的验证效率。
摘要：
我们介绍了QReach，这是基于决策图CFLOBDD（在CAV 2023上发表）的第一个量子马尔可夫链可达性分析工具。QReach提供了一种新的框架来寻找可达子空间，以及一系列模型检查子过程，如图像计算。实验表明其在验证量子电路和算法中的实用性。QReach预计将在未来的量子模型检查器中发挥核心作用。
英文摘要：
We present QReach, the first reachability analysis tool for quantum Markov chains based on decision diagrams CFLOBDD (presented at CAV 2023). QReach provides a novel framework for finding reachable subspaces, as well as a series of model-checking subprocedures like image computation. Experiments indicate its practicality in verification of quantum circuits and algorithms. QReach is expected to play a central role in future quantum model checkers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
