首届国际理论计算机联合大会（International Joint Conference on Theoretical Computer Science，IJTCS）于2020年8月17日-22日在线上举行，主题为“理论计算机科学领域的最新进展与焦点问题”，由北京大学与中国工业与应用数学学会（CSIAM）、中国计算机学会（CCF）、国际计算机学会中国委员会（ACM China Council）联合主办，北京大学前沿计算研究中心承办。  

　　8月19日，悉尼科技大学的应明生教授受邀在IJTCS大会上做了题为《量子系统的模型检查（Model-Checking Quantum Markov Chains）》的特邀报告，介绍了量子模型检查与量子马尔可夫链。报告由北京大学前沿计算研究中心讲席教授邓小铁主持。

　　应老师首先介绍了模型检查的基本概念。模型检查是一种用于验证系统的某些性质的技术，其问题可以形式化为，给定一个（有限的）转移系统  和时态逻辑命题 φ，判断是否有。特别地，当算法给出否定的回答时，我们还希望算法能给出反例，即一条导出与 φ 矛盾的命题的路径。这本质上是一个图上可达性的问题。模型检查的好处在于这个过程是完全自动的，而且算法可以提供反例，这对于程序查错是非常有用的。对于量子系统的模型检查，我们可以计算量子马尔可夫链的可达性。对于经典的图，我们可以用简单的搜索算法计算可达性；然而对于量子的图结构，其状态空间是不可数的，除了经典的邻接结构之外，还有叠加态带来的线性代数的性质，普通的搜索算法往往会破坏这种性质。

　　应老师还简单介绍了一些量子理论的基础。首先，量子系统的状态空间是复希尔伯特空间（带有内积且完备），有限维的情况即 Cⁿ。一个量子比特的状态空间是2维希尔伯特空间，一个量子比特的纯态可以表示为两个基的叠加，即

　　对于混合态，即以概率 p_i 处于 |ψ_i〉，可以用密度算符（矩阵半正定且迹为1）表示混合态，即。实际上，对于任意密度算符，都存在混合态与之对应。关于量子系统的动态，我们可以用关于其密度算符的微分方程描述。对于离散时间，我们可以用作用在密度算符上的超算子描述，如同概率分布之间的变换。Kraus 定理告诉我们，任何超算子都能表示为如下形式：

其中  是半正定的。

　　随后应老师介绍了量子马尔可夫链及关于其可达性的一些结果。量子马尔可夫链由一个有限维希尔伯特空间 及其上的超算子描述，对于起始状态 ρ，可以定义其到达子空间 G 的概率为

其中 ，即将该超算子限制在子空间外。定义一个状态与另一个状态相邻：若后者的非零特征值对应的特征向量张成的子空间经超算子作用后包含了前者的相应子空间。与经典的图论中类似地可以定义强连通分量为极大的强联通子空间（即其中任意两个状态可达）。特别地，若强联通分量关于超算子是不变的，则称之为 bottom strongly connected component。与经典的马尔可夫链类似地，对某个子空间，若从任意起始状态出发到达该子空间的概率都为0，则定义该子空间是 transient。实际上，令

则任何量子马尔可夫链的空间都能分解为两个空间的直和：

其中后者是最大的 transient 子空间，前者可以被分解为相互正交的 bottom strongly connected component 的直和，这种分解满足一种弱唯一性，即若存在两种不同的分解方式，则两种分解方式的 bottom strongly connected component 的个数是相同的，并且将它们分别按维数从小到大排序后，对应的维数也是相同的。分解可以在 O(d⁸) 时间内计算，这里 d 是空间的维数。可以证明：

利用 bottom strongly connected component 分解的算法，我们就可以在 O(d8) 时间内计算出到达概率。

　　最后，应老师提出了一些开放问题。首先，量子图论仍有很大的发展空间：我们对于量子的图知道的还很少，比如我们还不知道怎么定义量子的图上的生成树。其次，量子模型检查算法也可能有改进。最后，非常重要的是如何应用这些理论，帮助比如量子电路的验证，量子程序查错，甚至应用到量子物理的领域中去。