Development of software foundation based on certified formal tree language theory

2021 Fiscal Year Final Research Report

• Project/Area Number: 17K00007
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Theory of informatics
• Research Institution: Tohoku University (2018-2021); The University of Electro-Communications (2017)
• Principal Investigator: Nakano Keisuke 東北大学, 電気通信研究所, 教授 (30505839)
• Project Period (FY): 2017-04-01 – 2022-03-31
• Keywords: 形式木言語理論 / プログラム検証 / 定理証明支援系 / 双方向変換

Outline of Final Research Achievements

Formal tree language theory is a theory of tree automata and tree transducers for a formal model of tree-structured data, and is expected to be applied to efficient and verifiable software. In this research project, we have studied the relation between several classes of tree transducers and succeeded in showing that the class of stream-type tree transducers that is considered efficient corresponds to the largest class in which the equivalence problem is decidable. The results of this research are expected to lead to the development of some efficient program verification algorithms.

Free Research Field

形式木言語理論

Academic Significance and Societal Importance of the Research Achievements

二つのプログラムの振舞いが全く同じであるか（等価性）を検証する問題は一般に決定不能であるが，形式を制限することで決定可能になることが知られている．この制限は非常に強く，特に効率を意識したプログラムにおいてはその複雑さから等価性を判定することは困難であるとされてきた．本研究の成果では，ストリーム型変換と呼ばれる効率的かつ煩雑なプログラムについても等価性判定が決定可能であることが証明され，これはプログラム検証における新たな可能性を示している．提案した等価性判定の手法は，特定の条件下での等価性（部分等価性）の判定も扱うことができるため，後方互換性を意識したソフトウェアの保守にも応用が可能である．