QReach: A Reachability Analysis Tool for Quantum Markov Chains

TL;DR

QReach tackles the challenge of verifying quantum systems by computing reachable subspaces in quantum Markov chains using a CFLOBDD-based symbolic backend. It introduces a BFS-like reachability algorithm that leverages image and projection computations over Kraus representations to efficiently determine the subspace $R_C( ho)$. The work provides complexity insights ($O(d^3)$) and practical strategies like frontier simplification to handle quantum circuit verification tasks. Experimental results on quantum circuits and protocols illustrate QReach's practicality and its potential to underpin 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.