An Automata-based Framework for Quantum Circuit Verification
summary
Framework encodes sets of quantum basis trees as tree automata (BDD-like tries) and implements gate updates symbolically — X swaps left/right branches, S multiplies amplitudes by duplicating shared subtrees, and unitary updates run automata minimization afterward. Measurement uses a up-to-scalar inclusion check instead of normalization; loops require a user-supplied automaton invariant. Symbolic amplitude variables allow assertions like probability >= 90%. Prototype verifies Grover-like instances up to 200 qubits in 17s but currently cannot compactly handle global Hadamard across all states.
AI-written summary · about
chapters (11)
- 0:00Automata-based quantum verification
- 1:48BDDs to tree automata
- 3:11Symbolic verification
- 5:39Tree automata structure
- 7:49Quantum gate operations
- 9:33Symbolic exclusion
- 10:58Quantum advantage
- 12:45Verifying loops and branches
- 15:37Summary and future work
- 17:02Call for participation
- 17:42Q&A
related talks
18mQuantum Probabilistic Model Checking for Time-Bounded Properties
30mSymbolic Execution of Hadamard-Toffoli Quantum Circuits
18mFormalization of a Programming Language for Quantum Circuits with Measurement and Classical Control
17mQGAT: A Generate-and-Test Paradigm for Quantum Circuits
15mAssertion-Based Optimization of Quantum Programs
22mQuantum Controlled Measurements via Program Transformation
15mModular Component-Based Quantum Circuit Synthesis
14mEmbedding Quantum Program Verification into Dafny