Model Checking Applied to Quantum Physics
Ji Guan, Yuan Feng, Andrea Turrini, Mingsheng Ying

TL;DR
This paper demonstrates how model checking techniques can be adapted for quantum physics, enabling the verification of quantum systems modeled as quantum Markov chains using linear-time temporal logic.
Contribution
It introduces a novel approach to apply model checking to quantum physics by modeling quantum systems as Markov chains and verifying properties with an efficient algorithm.
Findings
Successfully modeled quantum systems as Markov chains
Developed an efficient algorithm for property verification
Validated approach with case studies on quantum problems
Abstract
Model checking has been successfully applied to verification of computer hardware and software, communication systems and even biological systems. In this paper, we further push the boundary of its applications and show that it can be adapted for applications in quantum physics. More explicitly, we show how quantum statistical and many-body systems can be modeled as quantum Markov chains, and some of their properties that interest physicists can be specified in linear-time temporal logics. Then we present an efficient algorithm to check these properties. A few case studies are given to demonstrate the use of our algorithm to actual quantum physical problems.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Quantum Computing Algorithms and Architecture · Distributed systems and fault tolerance
