| Project/Area Number |
22KJ1483
|
|---|
| Project/Area Number (Other) |
22J23575 (2022)
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Multi-year Fund (2023)
Single-year Grants (2022) |
|---|
| Section | 国内 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Tokyo Institute of Technology (2023)
Japan Advanced Institute of Science and Technology (2022) |
|---|
Principal Investigator |
高木 翼 東京工業大学, 情報理工学院, 特別研究員(PD)
|
|---|
| Project Period (FY) |
2023-03-08 – 2025-03-31
|
| Project Status |
Discontinued (Fiscal Year 2023)
|
| Budget Amount *help |
¥2,500,000 (Direct Cost: ¥2,500,000)
Fiscal Year 2024: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2023: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2022: ¥900,000 (Direct Cost: ¥900,000)
|
|---|
| Keywords | 量子論理 / 動的論理 / Maude / 形式検証 / 量子プログラム / 量子プロトコル / 線形時相論理 / 様相論理 / 動的代数 |
|---|
| Outline of Research at the Start |
本研究は、1936年以来量子計算とは無関係に発展してきた量子論理を量子計算の形式検証の補助という観点から見直し、現代的な論理に生まれ変わらせることを目的とする。具体的には、動的論理の発想（プログラムの実行を様相演算子により表現する）を取り入れ、動的量子論理を定式化する。また、その有効性を示すため、具体的な量子プロトコル、例えば超密度符号化、量子テレポーテーション、量子秘密分散、量子もつれスワッピング、量子ゲートテレポーテーション等の仕様記述を動的量子論理によって行い、それに基づく形式検証を自動化するツールを開発する。さらに、以上の成果を発展させ、量子通信ネットワークの仕様記述・形式検証を行う。
|
| 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 |
今後は本年度の成果をさらに発展させ、検証可能な量子プログラムの種類を増やしていくことを目指す。
|
