数据安全的未来依赖于有效利用量子技术。然而，其广泛的实施需要彻底的验证。研究人员提出了一种新方法来确认量子协议的可靠性，使其适用于安全性和保护性至关重要的应用。这个进展对建立可信的量子系统至关重要，而可信的量子系统是安全集成量子技术于需要高可靠性的系统中所必需的。
量子计算有潜力比传统计算机更迅速地解决复杂问题，这得益于量子力学的原理。在人工智能、密码学、深度学习、优化和复杂方程的解决等领域，已经取得了显著的进展。领先的科技公司如IBM、谷歌和微软正在努力创建能够处理更大规模量子信息的实用量子计算机，但要广泛接受量子技术仍需克服相当大的障碍。尽管由于其安全性，量子通信和密码学在商业环境中正在获得关注，但这些技术需要进行全面的验证，以便用于对安全敏感的应用。这一步骤对于避免安全或保护性漏洞至关重要。
为了填补这一空白，助理教授Canh Minh Do与日本先进科学技术学院（JAIST）的副教授高木翼和教授小方和弘合作，设计了一种使用基础动态量子逻辑（BDQL）验证量子程序的自动化技术。BDQL准确表示量子力学中的量子演变和测量过程，提供了一个逻辑结构以形式化和验证量子协议及其基本特性。尽管其有效性，BDQL确实存在某些缺点，尤其是在处理量子协议中参与者之间的交互方面。
为了应对这些弱点，研究人员开发了一种称为并发动态量子逻辑（CDQL）的新逻辑，增强了BDQL的功能，以适应量子协议中的并发性。在他们最近的研究中，该研究于12月12日发表在《ACM软件工程与方法学汇刊》上，Dr. Do表示：“CDQL成功形式化了量子协议中参与者的并发行为和通信。我们的逻辑框架还促进了从CDQL模型到BDQL模型的转变，确保与BDQL语义的一致性，并引入了一种懒惰重写技术，以便于流线型验证。”这一突破不仅增加了逻辑的表现力，还加快了验证过程，从而扩大了经过验证的实用量子解决方案的适用性。
与BDQL相比，CDQL的一个关键优势是其处理同时行动的能力。虽然BDQL限制于顺序行动，CDQL能够建模需要并发行动的量子协议，使其更适合解决现实世界的问题。此外，我们的逻辑框架包括一种懒惰重写策略，旨在提高验证过程的效率。具体来说，这一策略过滤出先前阶段中不相关的交织，并重用结果以防止不必要的计算。这大大提高了验证量子协议的速度和可扩展性。然而，我们的框架确实存在局限，包括无法通过量子通道处理量子数据共享。尽管如此，Dr. Do及其团队打算在未来解决这一局限性，提高CDQL的灵活性。
为了增强量子协议的建模和验证，CDQL作为BDQL的一个进步而出现。研究小组成功地使用BDQL和CDQL形式化并验证了各种量子通信协议。“我们采用BDQL和CDQL的自动化形式验证方法，建立了一个强大的框架，以确保量子协议的顺序和并发模型的准确性。这增强了基础技术的可靠性，如量子通信、量子密码学和分布式量子计算系统。” Dr. Do解释道。这项研究强调了在关键场景中应用量子协议之前确认其正确性的必要性。
总之，CDQL在形式化涉及并发行为的量子协议方面比BDQL更有效。“这项研究提出了一种使用CDQL验证量子协议准确性的自动化策略，确保其在高风险安全和保护性应用中的可靠性。” Dr. Do总结道。他进一步补充道：“通过验证量子协议的准确性，这一举措在未来五到十年中为开发可靠、无错误的量子技术发挥了关键作用，尤其是在量子通信和密码学领域。”
