一句话：提出 QPMC，用量子电路编码概率模型检测并以量子振幅估计求解时间有界性质，较 SMC 获二次加速。
概率模型检测（PMC）能分析概率系统性质，但面对大型系统时受状态爆炸困扰；统计模型检测（SMC）虽通过仿真回避状态爆炸，却因需要大量样本而出现运行时间爆炸，难以高精度验证大型系统。为此，作者提出量子概率模型检测（QPMC），这是首个利用量子计算对时间有界性质进行 PMC 的方法。QPMC 将 PMC 问题编码为量子电路，用量子比特叠加状态来缓解状态爆炸；并借助量子振幅估计高效估计指定性质的概率，从而缓解运行时间爆炸。作者证明 QPMC 能正确求解 PMC 问题，且相对 SMC 在时间复杂度上取得二次加速。
Probabilistic model checking (PMC) is a verification technique for analyzing the properties of probabilistic systems. However, existing techniques face challenges in verifying large systems with high accuracy. PMC struggles with state explosion , where the number of states grows exponentially with the size of the system, making large system verification infeasible. While statistical model checking (SMC) avoids PMC’s state explosion problem by using a simulation approach, it suffers from runtime explosion, requiring numerous samples for high accuracy. To address these limitations in verifying large systems with high accuracy, we present quantum probabilistic model checking (QPMC), the first method leveraging quantum computing for PMC with respect to timebounded properties. QPMC addresses state explosion by encoding PMC problems into quantum circuits that superpose states within qubits. Additionally, QPMC resolves runtime explosion through Quantum Amplitude Estimation, efficiently estimating the probabilities of specified properties. We prove that QPMC correctly solves PMC problems and achieves a quadratic speedup in time complexity compared to SMC.
@article{JeonCKLOK24,
title = {Quantum Probabilistic Model Checking for Time-Bounded Properties},
author = {Seungmin Jeon and Kyeongmin Cho and Chan Gu Kang and Janggun Lee and Hakjoo Oh and Jeehoon Kang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689731}
}