This program is tentative and subject to change.
Probabilistic model checking (PMC) is a verification technique for analyzing the properties of probabilistic systems. However, exisiting PMC 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 this problem by simulation approach, it suffers from runtime explosion, needing 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. QPMC addresses state explosion by encoding PMC problems into quantum circuits that superpose states within qubits. Additionally, QPMC alleviates runtime explosion through Quantum Amplitude Estimation, efficiently estimating the probabilities of specified properties. We prove that QPMC is correct in solving PMC problems and achieves a quadratic speedup in time complexity compared to SMC.
This program is tentative and subject to change.
Fri 25 OctDisplayed time zone: Pacific Time (US & Canada) change
11:00 - 12:20 | |||
11:00 20mTalk | Modular Synthesis of Efficient Quantum Uncomputation OOPSLA 2024 Hristo Venev INSAIT, Sofia University "St. Kliment Ohridski", Timon Gehr ETH Zurich, Dimitar Dimitrov INSAIT, Sofia University, Martin Vechev ETH Zurich | ||
11:20 20mTalk | Quantum Probabilistic Model Checking OOPSLA 2024 Seungmin Jeon KAIST, Kyeongmin Cho Rebellions, Chan Gu Kang Korea University, Janggun Lee KAIST, Hakjoo Oh Korea University, Jeehoon Kang KAIST | ||
11:40 20mTalk | Quarl: A Learning-Based Quantum Circuit Optimizer OOPSLA 2024 Zikun Li Carnegie Mellon University, Jinjun Peng Columbia University, Yixuan Mei Carnegie Mellon University, Sina Lin Microsoft, Yi Wu Tsinghua University, Oded Padon VMware Research, Zhihao Jia Carnegie Mellon University | ||
12:00 20mTalk | Synthetiq: Fast and Versatile Quantum Circuit Synthesis OOPSLA 2024 Anouk Paradis ETH Zurich, Jasper Dekoninck ETH Zurich, Benjamin Bichsel ETH Zurich, Switzerland, Martin Vechev ETH Zurich |