QReach: A Reachability Analysis Tool for Quantum Markov Chains
arXiv:2512.04497 · doi:10.1007/978-3-031-65633-0_23
Abstract
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.
15 pages, 5 figures