摘要：数据安全的未来取决于量子技术的可靠应用，但其广泛采用需要严格的验证。研究人员开发了一种新颖的方法来验证量子协议，以确保其在安全和关键安全应用方面的可靠性。这一进步解决了对值得信赖的量子系统的需求，这对于在高可靠性系统中安全部署的安全部署至关重要。...

量子计算通过利用量子力学原理来比古典计算机更快地解决复杂问题的潜力。在人工智能，密码学，深度学习，优化和解决复杂方程等领域已取得了重大进步。尽管IBM，Google和Microsoft这样的主要技术公司正在努力努力处理能够处理更大量子信息的实用量子计算机，但在可以广泛采用量子技术之前，仍然存在重大挑战。尽管由于其安全系统，量子通信和加密量越来越多地用于商业应用中，但量子通信和加密术必须进行严格的验证，以便在安全至关重要的应用中使用。这些过程对于确保没有安全或保障的失误至关重要。

为了解决这一差距，助理教授Canh Minh Do，以及日本高级科学技术学院（JAIST）的Tsubasa Takagi副教授和Kazuhiro Ogata教授，日本，开发了一种自动化方法，以验证基于基本动态量子逻辑（BDQL）的量子程序。 BDQL忠实地捕获了量子力学中的量子进化和测量，提供了一个逻辑框架，以正式化和验证其所需属性。尽管具有有效性，但BDQL仍存在局限性，尤其是其无法处理量子协议中参与者之间的相互作用的局限性。

为了克服这些局限性，该团队现在开发了一种新的逻辑，称为并发动态量子逻辑（CDQL），该逻辑扩展了BDQL的能力来处理量子协议中的并发。 In their recent study published on Dec 12 in ACM Transactions on Software Engineering and Methodology, Dr. Do explains, "CDQL effectively formalizes concurrent behaviors and communication between participants in quantum protocols. Our logical framework also provides a transformation from CDQLs models to BDQL models, ensuring compatibility with BDQL semantics, and introduces a lazy rewriting strategy for fast verification."这种进步不仅增强了逻辑的表现力，而且加快了验证过程，使其适用于更广泛的经过验证的实用量子应用。

CDQL比BDQL的主要优点之一是其处理并发动作的能力。尽管BDQL仅限于顺序操作，但CDQL可以建模需要多个动作同时进行的量子协议，从而更适合于现实世界中的问题。此外，我们的逻辑框架提供了一种懒惰的重写策略，以提高验证过程的效率。具体而言，该策略消除了早期阶段的无关交流，并避免了不必要的计算。这可以提高验证量子协议的速度和可扩展性。尽管它具有优势，但我们的框架仍有一些局限性，例如无法处理量子数据共享的量子数据。但是，DO博士和他的团队计划将来解决这一约束，以提高CDQL的多功能性。

为了改善量子协议的建模和验证，CDQL已开发为BDQL的扩展。研究团队在BDQL和CDQL中成功地正式化并验证了各种量子通信协议。 “我们使用BDQL和CDQL的自动形式验证方法提供了一个严格的框架来验证量子协议的顺序和并发模型。这有助于基础技术的可靠性，例如量子通信，量子密码学和分布式量子计算系统，”这项工作强调了在将量子协议部署到关键应用程序中之前确保其正确性的重要性。

总之，CDQL比BDQL更有效，用于以并发作用形式化量子协议。 Do总结说：“这项工作介绍了一种使用CDQL自动化的方法来验证量子协议的正确性，并在部署安全至关重要和关键安全应用程序之前确保其可靠性。”他进一步补充说：“通过确保量子协议的正确性，这项工作有助于在未来5到10年内开发可靠的，无虫的量子技术，尤其是在量子通信和密码学方面。”