2022 Fiscal Year Annual Research Report
Construction of Mathematical Logic System to Verify Quantum Communication Networks and Its Quantum Computational Implications
| Project/Area Number |
22J23575
|
|---|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
高木 翼 北陸先端科学技術大学院大学, 先端科学技術研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2022-04-22 – 2025-03-31
|
| Keywords | 量子論理 / 線形時相論理 / 動的論理 / 様相論理 / 動的代数 |
|---|
| Outline of Annual Research Achievements |
本年度は、様相論理（動的論理・線形時相論理）を拡張することで、量子プログラム（量子通信プロトコルを含む）の数理論理体系を構築した。
（１）量子プログラムの代数として量子動的代数(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に掲載された。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
当初の計画では、量子論理および動的論理を用いて量子プログラムの数理論理体系を構築する予定であった。それは、動的論理の代数的意味論を介した量子動的代数の定式化によって早期に達成された。そこで、動的論理とは異なる様相論理のうち、線形時相論理について検討を行ったところ、同様に量子論理と線形時相論理を用いて量子プログラムの数理論理体系が構築できることが分かった。結果的には、量子論理・線形時相論理・動的論理の三つを組み合わせた動的線形時相量子論理が得られたため、当初の計画以上に進展しているといえる。
|
| Strategy for Future Research Activity |
本年度の研究により数理論理体系が構築できたため、今後は具体的な量子アルゴリズム・量子通信プロトコルの検証を行っていく。
|
