Model Checking Applied to Quantum Physics
arXiv:1902.03218
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.
References in corpus (12)
- Thermalization and its mechanism for generic isolated quantum systems
- Persistent entanglement in arrays of interacting particles
- The foundations of statistical mechanics from entanglement: Individual states vs. averages
- Quantum mechanical evolution towards thermal equilibrium
- Open Quantum Random Walks
- Quantum Information Meets Quantum Matter -- From Quantum Entanglement to Topological Phase in Many-Body Systems
- Asymptotics of quantum channels: conserved quantities, an adiabatic limit, and matrix product states
- Irreducible forms of Matrix Product States: Theory and Applications
- Reachability Probabilities of Quantum Markov Chains
- Reachability and Termination Analysis of Concurrent Quantum Programs
- Model Checking Quantum Systems --- A Survey
- The Structure of Decoherence-free Subsystems