Saved in:
Bibliographic Details
Main Authors: Dai, Aochu, Ying, Mingsheng
Format: Preprint
Published: 2025
Subjects:
Online Access:https://arxiv.org/abs/2512.04497
Tags: Add Tag
No Tags, Be the first to tag this record!
Table of Contents:
  • 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.