QReach: A Reachability Analysis Tool for Quantum Markov Chains

TL;DR

QReach is a pioneering tool that performs reachability analysis for quantum Markov chains using decision diagrams, enabling verification of quantum circuits and algorithms with promising practical applications.

Contribution

It introduces the first reachability analysis framework for quantum Markov chains utilizing CFLOBDD decision diagrams, advancing quantum model checking capabilities.

Findings

Effective in verifying quantum circuits and algorithms

Demonstrates practicality through experimental results

Lays groundwork for future quantum model checkers

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.