2023 Fiscal Year Research-status Report
Construction of Mathematical Logic System to Verify Quantum Communication Networks and Its Quantum Computational Implications
| Project/Area Number |
22KJ1483
|
|---|
| Allocation Type | Multi-year Fund |
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
高木 翼 東京工業大学, 情報理工学院, 特別研究員(PD)
|
|---|
| Project Period (FY) |
2023-03-08 – 2025-03-31
|
| Keywords | 量子論理 / 動的論理 / Maude / 形式検証 / 量子プログラム / 量子プロトコル |
|---|
| Outline of Annual Research Achievements |
本年度は簡略化された動的量子論理(Basic Dynamic Quantum Logic, BDQL)に基づいて量子プログラムを形式検証する手法を提案した。また、その手法に基づいて自動的に形式検証を実行するツールをプログラミング言語Maudeによって実装した。さらに、ケース・スタディとして、超密度符号化、量子テレポーテーション、量子秘密分散、量子もつれスワッピング、量子ゲートテレポーテーションの5つの量子プロトコルに加え、それらの変種である、量子リレースキーム、双方向量子テレポーテーション、二量子ビットテレポーテーション、量子ネットワークコーディングの4つの量子プロトコルの自動形式検証に成功した。本ツールは、動的量子論理に基づく実装としては世界初の実装であり、従来の手法と比較して高度な自動化が達成されている。つまり、補題やヒューリスティクスによって定理証明を人間が誘導（補助）する必要は一切なく、量子プログラムと仕様（満たすべき性質）を入力するだけで自動的にそのプログラムが仕様を満たすかどうかの判定が行われる。また、いずれのプロトコルも数秒以内に検証が完了しており、ツールの実行速度としては十分満足できるものになった。特に、今回検証した最大のプロトコルである量子ネットワークコーディングは14量子ビットのプロトコルであり、その検証は4秒程度で完了した。計算機に依存しない指標である書き換えステップ数については約1000万ステップとなった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の予定通り、前年度に構築した数理論理体系に基づいて、今年度は具体的な量子プログラムの検証を行うことができた。また、当初想定していたよりも多くの量子プログラムの検証を行えたため、進捗としては十分なものになったといえる。
|
| Strategy for Future Research Activity |
今後は本年度の成果をさらに発展させ、検証可能な量子プログラムの種類を増やしていくことを目指す。
|
| Causes of Carryover |
研究の進捗状況を鑑みて当初参加を予定していた学会への参加を見送ったため。代わりに、次年度で当該学会に参加する予定である。
|
