Model Checking Applied to Quantum Physics

Model Checking Quantum Systems --- A Survey

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.

Model checking quantum Markov chains

Although the security of quantum cryptography is provable based on the principles of quantum mechanics, it can be compromised by the flaws in the design of quantum protocols and the noise in their physical implementations. So, it is indispensable to develop techniques of verifying and debugging quantum cryptographic systems. Model-checking has proved to be effective in the verification of classical cryptographic protocols, but an essential difficulty arises when it is applied to quantum systems: the state space of a quantum system is always a continuum even when its dimension is finite. To ove…

Model Checking for Verification of Quantum Circuits

In this talk, we will describe a framework for assertion-based verification (ABV) of quantum circuits by applying model checking techniques for quantum systems developed in our previous work, in which: (i) Noiseless and noisy quantum circuits are modelled as operator- and super-operator-valued transition systems, respectively, both of which can be further represented by tensor networks. (ii) Quantum assertions are specified by a temporal extension of Birkhoff-von Neumann quantum logic. Their semantics is defined based on the design decision: they will be used in verification of quantum circuit…

对矩阵积态进行线性链逻辑的模型检查

Model Checking Matrix Product States against Linear Chain Logic

本文提出线性链逻辑(LCL)，用于验证周期性MPS家族在系统尺寸增长时的物理性质，如环上的非平凡性和大尺寸渐进行为，通过完全正映射分析MPS的定量特征，实现高效的模型检查算法。

Probabilistic Model--Checking of Quantum Protocols

We establish fundamental and general techniques for formal verification of quantum protocols. Quantum protocols are novel communication schemes involving the use of quantum-mechanical phenomena for representation, storage and transmission of data. As opposed to quantum computers, quantum communication systems can and have been implemented using present-day technology; therefore, the ability to model and analyse such systems rigorously is of primary importance. While current analyses of quantum protocols use a traditional mathematical approach and require considerable understanding of the under…

浅层量子电路的可扩展等价性检查与验证

Scalable Equivalence Checking and Verification of Shallow Quantum Circuits

本文研究浅层量子电路的等价性检查问题，提出基于局部投影约束的判定方法，在经典计算机上实现了与量子比特数呈线性关系的时间与空间复杂度，并支持静态与运行时断言检查。