← Back to papers
QReach: A Reachability Analysis Tool for Quantum Markov Chains
Aochu Dai, Mingsheng Ying·December 4, 2025·DOI: 10.1007/978-3-031-65633-0_23
Quantum Physicscs.LO
AI Breakdown
Get a structured breakdown of this paper — what it's about, the core idea, and key takeaways for the field.
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.