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

点击翻译按钮获取中文摘要

本年度は、様相論理（動的論理・線形時相論理）を拡張することで、量子プログラム（量子通信プロトコルを含む）の数理論理体系を構築した。（１）量子プログラムの代数として量子動的代数(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に掲載された。