QReach: A Reachability Analysis Tool for Quantum Markov Chains
By: Aochu Dai, Mingsheng Ying
Potential Business Impact:
Checks if quantum computers work correctly.
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.
Similar Papers
Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networks
Machine Learning (CS)
Makes robots safe with math proof.
Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks
Symbolic Computation
Helps computers check if systems will fail.
Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks
Symbolic Computation
Finds how likely systems will reach a goal.