Tsubasa Takagi's Personal Webpage

Tsubasa Takagi, Ph.D.  0000-0001-9890-1015

Contact

• Ogata Laboratory at School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
• E-mail:

Curriculum Vitae

Work Experience

• JSPS Research Fellow (DC1), Japan Society for the Promotion of Science (April. 2022 -- September. 2023)
• JSPS Research Fellow (PD), Japan Society for the Promotion of Science (October. 2023 -- March. 2025)

Education

• Doctor of Philosophy (Information Science), Japan Advanced Institute of Science and Technology (October. 2021 -- September. 2023)
• Master of Science (Information Science), Japan Advanced Institute of Science and Technology (April. 2020 -- September. 2021)

Area of Study

• Theoretical Computer Science
• Mathematical Logic
• Formal Verification
• Quantum Computation

Research Interests

I am interested in the mathematics of quantum computer programs (quantum programs) and its application to formal verification.

Quantum computing is counter-intuitive and distinct from classical computing, which makes it challenging to design and implement quantum protocols, algorithms, and programs accurately. Therefore, it is crucial to ensure their correctness through verification.

While existing logics/algebras can be used to verify that classical systems enjoy some desired properties, they cannot be directly applied to quantum systems due to the distinct principles used in quantum computing.

I am aiming to establish formal verification techniques for quantum programs by combining Dynamic Logic with Quantum Logic.

Keywords

Quantum Logic, Quantum Computation, Formal Verification, Modal Logic, Dynamic Logic, Temporal Logic, Equational Logic, Algebraic Structure, State Transition System, Model Checking, Automata

Publications

Journal Papers (refereed)

1. Tsubasa Takagi, Semantic Analysis of a Linear Temporal Extension of Quantum Logic and Its Dynamic Aspect. ACM Transactions on Computational Logic, 24(3): 1-21, ACM, 2023. [PDF]
2. Tsubasa Takagi, Translation from Three-Valued Quantum Logic to Modal Logic. International Journal of Theoretical Physics, 60(1): 366–377, Springer, 2021. [PDF]
3. Tsubasa Takagi, Observable-Dependent Kripke Semantics for Quantum Logic (in Japanese). Japanese Student Research Notes of Philosophy of Science, 4: 1-8, Japan Association for Philosophy of Science, 2021. (Japanese Title: 量子論理のオブザーバブル依存Kripke意味論, 新進研究者 Research Notes) [PDF]
4. Tsubasa Takagi, Validity Checking by K4 Tableau and Filtration Method (in Japanese). Journal of Science and Philosophy, 2(1): 4-23, 2019. (Japanese Title: K4タブローによる妥当性判定と濾過法, Journal of Science and Philosophy) [PDF]

Conference Papers (refereed)

1. Tsubasa Takagi, Canh Minh Do, Kazuhiro Ogata. Automated Quantum Program Verification in Dynamic Quantum Logic. In Proceedings of DaLí: Dynamic Logic – New trends and applications, (DaLí 2023), Forthcoming, 2023.
2. Tsubasa Takagi, An Algebra of Quantum Programs with the Kleene Star Operator. In Proceedings of International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (FAVPQC 2022), CEUR Workshop Proceedings, 3280: 2-15, 2022. [PDF]

Technical Reports (not refereed)

1. Tsubasa Takagi, Quantum Program Verification and Its Implementation Based on Dynamic Quantum Logic (in Japanese). In the special interest group technical reports of Information Processing Society of Japan (9th Quantum Software Workshop at IPSJ), IPSJ SIG Technical Report, Vol.2023-QS-9 (6): 1-6, 2023. (Japanese Title: 動的量子論理による量子プログラム検証およびその実装, 研究報告量子ソフトウェア(QS))

Research Grants

As a principal investigator:

1. Construction of Mathematical Logic System to Verify Quantum Communication Networks and Its Quantum Computational Implications (Japanese Title: 量子通信ネットワークを検証する数理論理体系の構築と量子計算的意味付け), Grant-in-Aid for JSPS Research Fellow Grant Number 22J23575 (2,500,000 JPY, April. 2022 -- March. 2025).

As a co-investigator:

1. An Automated Approach to Verify Quantum Programs Using Dynamic Quantum Logic, JAIST Research Grants FY 2023 (500,000 JPY, April. 2023 -- March. 2024), Canh Minh Do (principal investigator).

Teaching

• Teaching Assistant for "Fundamentals of Logic and Mathematics" (JAIST, 2023)
• Teaching Assistant for "Mathematical Logic" (JAIST, 2021, 2022)
• Teaching Assistant for "Fundamental Mathematics for Information Science" (JAIST, 2021, 2022, 2023)

Financial Support

1. JSPS Research Fellow (DC1), Japan Society for the Promotion of Science (April. 2022 -- March. 2025)
2. Research Assistant in Ogata Laboratory at Japan Advanced Institute of Science and Technology (October. 2021 -- March. 2022)
3. JASSO Scholarship for Ph.D. Students, Exemption from refund due to outstanding performance, Japan Student Services Organization (October. 2021 -- March. 2022)
4. JASSO Scholarship for Master's Students, Exemption from refund due to outstanding performance, Japan Student Services Organization (April. 2020 -- September. 2021)
5. SD Program Scholarship, Japan Advanced Institute of Science and Technology (April. 2020 -- March. 2022)