Model Checking Quantum Systems --- A Survey

TL;DR

This survey reviews the challenges and progress in developing model-checking techniques for quantum systems, covering quantum communication protocols and general quantum systems including physical and computational models.

Contribution

It provides a comprehensive overview of existing research and introduces new approaches by the authors for verifying quantum systems.

Findings

Identified key difficulties in quantum model checking.

Reviewed early research on quantum communication protocols.

Presented new methods for checking general quantum systems.

Abstract

This article discusses the essential difficulties in developing model-checking techniques for quantum systems that are never present in model checking classical systems. It further reviews some early researches on checking quantum communication protocols as well as a new line of researches pursued by the authors and their collaborators on checking general quantum systems, applicable to both physical systems and quantum programs.