Construction of Mathematical Logic System to Verify Quantum Communication Networks and Its Quantum Computational Implications

验证量子通信网络的数学逻辑系统的构建及其量子计算意义

基本信息

批准号：
22KJ1483
负责人：
高木翼
金额：
$ 1.6万
依托单位：
Japan Advanced Institute of Science and Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2023
资助国家：
日本
起止时间：
2023-03-08 至 2025-03-31
项目状态：
未结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22KJ1483/
关键词：
量子論理線形時相論理動的論理様相論理動的代数

项目摘要

本年度は、様相論理（動的論理・線形時相論理）を拡張することで、量子プログラム（量子通信プロトコルを含む）の数理論理体系を構築した。（１）量子プログラムの代数として量子動的代数(Quatum Dynamic Algebra)を新たに提案した。この代数は従来の動的量子論理(Dynamic Quantum Logic)とは異なり、繰り返しを表すクリーネスターを扱える。さらに、量子システムを表現する量子状態遷移系から量子動的代数を構成する方法を確立した。以上の成果を国際会議International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (FAVPQC 2022)において発表した。さらに、同成果はCEUR Workshop Proceedingsに掲載された。（２）線形時相量子論理(Linear Temporal Quantum Logic, LTQL)を新たに提案した。古典計算とは異なり、量子計算には通常の計算（量子ゲート）に加えて測定という操作がある。しかし、従来の線形時相論理には測定を表現するオペレータがない。そこで、さらに動的量子論理のアイディアに基づいてLTQLに測定オペレータを追加した動的線形時相量子論理(Dynamic Linear Temporal Quantum Logic, DLTQL)を提案し、その数学的性質を調べた。以上の成果は国際学術誌ACM Transactions on Computational Logicに掲載された。

今年，我们通过扩展模态逻辑（动态逻辑和线性时态逻辑），构建了量子程序（包括量子通信协议）的数理逻辑系统。 (1)我们提出了一种新的量子动态代数作为量子程序的代数。该代数与传统动态量子逻辑的不同之处在于它可以处理代表重复的干净星体。此外，我们建立了一种从代表量子系统的量子状态转换系统构造量子动态代数的方法。上述结果已在后量子密码协议形式分析与验证国际研讨会（FAVPQC 2022）上公布。此外，研究结果发表在 CEUR 研讨会论文集上。 (2)我们新提出了线性时间量子逻辑(LTQL)。与经典计算不同，量子计算除了正常计算（量子门）之外还涉及一种称为测量的操作。然而，传统的线性时序逻辑没有运算符来表达测量值。因此，基于动态量子逻辑的思想，我们提出了动态线性时间量子逻辑（DLTQL），在LTQL的基础上添加了测量算子，并研究了其数学特性。上述成果发表在国际学术期刊ACM Transactions on Computational Logic上。