Building Theoretical Foundation of Computer Science

Laboratory on Computational Logic
Associate Professor：TAKAGI Tsubasa

E-mail：
［Research areas］
Theoretical Computer Science
［Keywords］
Many-sorted Equational Logic, Modal Logic, Dynamic Logic (Hoare Logic), Temporal Logic (Model Checking), Quantum Logic

Skills and background we are looking for in prospective students

It is recommended that students have a motivation to not only use the computer as a tool, but also to understand (or invent) the mechanism of computers.

What you can expect to learn in this laboratory

In our laboratory, students will acquire the ability to solve social problems based on solid logical/mathematical thinking skills. These abilities are versatile and highly applicable skills that will be required for any kind of job after completion of the program. In particular, engineers beyond a certain level of expertise are required to have a high level of specialized knowledge. Through research activities in our laboratory, students will not only be able to program and write specifications, but also to gain a rigorous mathematical understanding of their principles and functions.

【Job category of graduates】IT and communication companies, research institutes

Research outline

Our research field is theoretical computer science. In today's advanced IT society, everyone is using "computers" in the broad sense of the term, such as smartphones and personal computers, to enrich their lives. In our laboratory, we are not just using "computers" as tools, but are conducting research to theoretically re-formulate their mechanisms or to design new ones.

Specifically, we apply mathematical logic, a branch of mathematics, to scientifically explore the functions of programming and the specifications of software and communication protocols. Furthermore, we aim to realize highly reliable software by developing formal verification techniques that mathematically guarantee the correctness of algorithms and programs.

Our laboratory uses mathematical logic to rigorously prove the correctness of quantum computation (quantum protocols and quantum programs) in particular.

Quantum computation is based on a fundamentally different principle from classical computation and is difficult to debug by testing. The reasons for this are: (1) the act of confirming a state in progress changes that state (state collapse due to observation), (2) different measurement values can be obtained probabilistically from the same measurement (nondeterminism of observation), and (3) a state cannot be duplicated in general (no-cloning theorem).

For these reasons, mathematical proof of the correctness of the design of quantum computation (formal verification) is important to increase reliability of quantum computation, which are difficult for intuition to work with.

1. Formal Verification of Quantum Computation Based on Many-sorted Equational Logic

To conduct formal verification, a mathematically rigorous specification of a system or program is first required. In particular, many-sorted equational logic provides the theoretical basis for rigorous specifications expressed by equations (called algebraic specifications), and then formal verification is conducted by equational reasoning based on these specifications. This method has been used with great success in formal verification of classical computation.

Therefore, it is a natural idea to follow this approach and give an algebraic specification of a quantum computation based on many-sorted equational logic. In addition to this, we have successfully implemented an algebraic specification of quantum computation on a classical computer for automated formal verification.

2. Formal Verification of Quantum Computation Based on Dynamic Quantum Logic

It is also interesting to start from the research question of what is the logic of quantum computation, rather than from classical formal verification. John von Neumann, the father of the computer, and his colleague created quantum logic as the logic of quantum mechanics in 1936. Since quantum computation was born half a century later, quantum logic and quantum computation were unrelated at that time. So, how can quantum logic be reborn as a modern logic by incorporating the viewpoint of quantum computation?

One answer to this question is dynamic quantum logic, which integrates dynamic logic and quantum logic. In our research, by formulating an algebra of dynamical quantum logic, we have succeeded in formally verifying various quantum programs based on it in a manner similar to that of Hoare logic. Dynamic quantum logic is also interesting as a merely mathematical structure, and the investigation of its properties is useful for understanding of quantum computation.

Key publications

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.
2. 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, Lecture Notes in Computer Science (LNCS), 14401: 68- 84, 2024.
3. 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, CEUR Workshop Proceedings, 3280: 2-15, 2022.