QReach: A Reachability Analysis Tool for Quantum Markov Chains
Quantum Physics
2025-12-05 v1 Logic in Computer Science
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.
Cite
@article{arxiv.2512.04497,
title = {QReach: A Reachability Analysis Tool for Quantum Markov Chains},
author = {Aochu Dai and Mingsheng Ying},
journal= {arXiv preprint arXiv:2512.04497},
year = {2025}
}
Comments
15 pages, 5 figures