Tsubasa Takagi's Personal Webpage

Tsubasa Takagi  0000-0001-9890-1015

Contact

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

Research History

Work Experience

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

Education

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

Area of Study

• Theoretical Computer Science
• Mathematical Logic

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

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

1. 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]

Research Grants

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 (April. 2022 -- March. 2025)

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)