Quantum Probabilistic Model Checking for Time-Bounded Properties
summary
Encodes time-bounded probabilistic model checking as quantum circuits that superpose the 2^n state distribution, implements state transition circuits by translating guard/choice/update into gates using Cas kit, and extracts probabilities with Quantum Amplitude Estimation to claim a quadratic speedup over statistical model checking. Paper proves correctness and analyzes complexity; prototype counts show required qubits from ~1,000 to >10,000 and gate counts from ~100K to >1,000K, so method is asymptotically faster but needs large quantum hardware to be practical.
AI-written summary · about
chapters (11)
- 0:00Probabilistic systems intro
- 1:26Classical scalability challenges
- 2:26Quantum advantage for model checking
- 3:53Quantum state transitions
- 5:39Quantum circuits for transitions
- 7:05Model to quantum circuits
- 9:57Complex models with quantum circuits
- 10:38Summary of quantum model checking
- 11:20Time complexity comparison
- 12:25Quantum circuit resources
- 13:09Q&A
related talks
22mAn Automata-based Framework for Quantum Circuit Verification
15mAssertion-Based Optimization of Quantum Programs
15mModular Component-Based Quantum Circuit Synthesis
20mMarQSim: Reconciling Determinism and Randomness in Compiler Optimization for Quantum(…)
30mSymbolic Execution of Hadamard-Toffoli Quantum Circuits
18mFormalization of a Programming Language for Quantum Circuits with Measurement and Classical Control
24mConcurrent Quantum Separation Logic for Fine-Grained Parallelism
32mOptimal Quantum Programs