Probabilistic Model Checking (PMC) is an automated method for analyzing probabilistic systems. For example, PMC is employed to verify the reliability of distributed systems, assess communication protocol performance, and evaluate the safety of autonomous driving systems, which are crucial for preventing human casualties. However, PMC struggles with the state explosion problem, which limits its scalability in complex and large systems. To address these issues, methods like statistical model checking have been proposed, but they still have limitations in analyzing large systems with high accuracy.
In this thesis, we introduce Quantum Probabilistic Model Checking (QPMC), a new approach utilizing quantum computing to address the scalability-accuracy tradeoff in PMC. QPMC focuses on PMC problems associated with discrete-time Markov chains and bounded reachability. It efficiently translates large-scale PMC problems into quantum circuits, enabling quantum computers to solve PMC problems more efficiently. Additionally, QPMC proposes a technique for reducing the qubit requirements for practical resource limits. We prove the correctness of QPMC, ensuring that it correctly encodes PMC problems and produces results identical to traditional PMC. Our performance evaluation demonstrates that QPMC achieves a quadratic speedup compared to classical SMC. Experimentally, our qubit optimization technique has proven to reduce qubit usage by 15%-45% in select large-scale PMC problems.
확률적 모델 체킹(PMC)은 확률적 시스템을 분석하기 위한 자동화된 방법이다. 예를 들어, PMC는 분산 시스템의 신뢰성을 검증하고, 통신 프로토콜의 성능을 평가하며, 또한 자율 주행 시스템의 안전성을 평가하는 데도 사용되며, 이는 인명 사고를 방지하는 데 중요하다. 하지만 PMC는 복잡하고 대규모 시스템에서 확장성을 제한하는 상태 폭발 문제에 직면하고 있다. 이러한 문제를 해결하기 위해 통계적 모델 체킹과 같은 방법이 제안되었지만, 대규모 시스템을 높은 정확도로 분석하는 데에는 여전히 한계가 있다.
이 논문에서는 양자 컴퓨팅을 활용하여 PMC의 확장성-정확성 간의 균형을 맞추는 새로운 접근 방식인 양자 확률적 모델 체킹(QPMC)을 소개한다. QPMC는 이산 시간 마르코프 체인과 경계 도달성과 관련된 PMC 문제에 초점을 맞추고 있다. 이 방법은 대규모 PMC 문제를 효율적으로 양자 회로로 변환하여, 양자 컴퓨터가 PMC 문제를 더 효율적으로 해결할 수 있게 한다. 또한, QPMC는 실용적인 자원 한계 내에서 큐비트 요구사항을 줄이는 기술을 제안한다. 우리는 QPMC의 정확성을 입증하여, 이것이 PMC 문제를 정확하게 인코딩하고 전통적인 PMC와 동일한 결과를 생성함을 보장한다. 성능 평가를 통해 QPMC가 고전적 통계적 방법에 비해 이차적인 속도 향상을 달성한다는 것을 보였다. 실험적으로, 우리의 큐비트 최적화 기술은 선택된 대규모 PMC 문제에서 큐비트 사용량을 15%-45%까지 줄일 수 있음을 증명했다.
