所提出的模型检查方法可用于量子电路的规范和验证，并具有其所需的特性。图片来源：PeerJ 计算机科学 （2024）。DOI： 10.7717/peerj-cs.2098

量子计算是一项快速发展的技术，它利用量子物理定律来解决经典计算极其困难的复杂计算问题。世界各地的研究人员已经开发了许多量子算法来利用量子计算，显示出对经典算法的显著改进。

量子电路是量子计算的模型，对于开发这些算法至关重要。它们用于在量子硬件上实际部署之前设计和实现量子算法。

量子电路包括一系列量子门、量子比特的测量和初始化，以及其他操作。量子门通过对量子比特（经典比特（0 和 1）的量子对应物）进行操作以及操纵系统的量子态来执行量子计算。量子态是量子电路的输出，可以对其进行测量以获得具有概率的经典结果，从中可以进行进一步的操作。

由于量子计算通常违反直觉，并且与经典计算截然不同，因此出错的概率要高得多。因此，有必要验证量子电路是否具有预期的所需特性和功能。这可以通过模型检查来完成，模型检查是一种形式化的验证技术，用于验证系统是否满足所需的属性。

尽管一些模型检查器专用于量子程序，但由于量子电路中的表示形式不同且没有迭代，因此模型检查量子程序和量子电路之间存在差距。

为了解决这一差距，日本科学技术高等研究院（JAIST）的Canh Minh Do助理教授和绪方和弘教授提出了一种符号模型检查方法。

Do博士解释说：“考虑到模型检查方法在经典电路验证方面的成功，量子电路的模型检查是一种很有前途的方法。我们开发了一种符号方法，用于使用量子力学定律和使用Maude编程语言的基本矩阵运算对量子电路进行模型检查。

他们的方法在发表在《PeerJ Computer Science》杂志上的一项研究中进行了详细介绍。

Maude 是一种基于重写逻辑的高级规范/编程语言，支持复杂系统的形式化规范和验证。它配备了线性时态逻辑 （LTL） 模型检查器，用于检查系统是否满足指定的属性。

此外，Maude 允许创建精确的系统数学模型。研究人员在莫德正式指定了量子电路，作为一系列量子门和测量应用，表示为使用量子力学定律和狄拉克符号的基本矩阵运算。他们在 LTL 中指定了系统的初始状态和所需属性。

通过使用一组量子物理定律和我们规范中形式化的基本矩阵运算，可以在 Maude 中推理量子计算。然后，他们使用内置的Maude LTL模型检查器来自动验证量子电路是否满足所需的属性。

更多信息：Canh Minh Do 等人，在 Maude 中检查量子电路的符号模型，PeerJ 计算机科学 （2024）。DOI： 10.7717/peerj-cs.2098