DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | 강지훈 | - |
dc.contributor.author | Jeon, Seungmin | - |
dc.contributor.author | 전승민 | - |
dc.date.accessioned | 2024-07-30T19:31:42Z | - |
dc.date.available | 2024-07-30T19:31:42Z | - |
dc.date.issued | 2024 | - |
dc.identifier.uri | http://library.kaist.ac.kr/search/detail/view.do?bibCtrlNo=1097246&flag=dissertation | en_US |
dc.identifier.uri | http://hdl.handle.net/10203/321666 | - |
dc.description | 학위논문(석사) - 한국과학기술원 : 전산학부, 2024.2,[iv, 38 p. :] | - |
dc.description.abstract | 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. | - |
dc.language | eng | - |
dc.publisher | 한국과학기술원 | - |
dc.subject | 양자 컴퓨팅▼a확률 시스템▼a시스템 검증▼a모델체킹 | - |
dc.subject | Quantum computing▼aProbabilistic system▼aSystem verification▼aModel checking | - |
dc.title | Quantum probabilistic model checking | - |
dc.title.alternative | 양자컴퓨터를 이용한 확률 시스템 모델체킹 | - |
dc.type | Thesis(Master) | - |
dc.identifier.CNRN | 325007 | - |
dc.description.department | 한국과학기술원 :전산학부, | - |
dc.contributor.alternativeauthor | Kang, Jeehoon | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.