| 研究課題/領域番号 |
17K00007
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 東北大学 (2018-2021)
電気通信大学 (2017) |
|---|
研究代表者 |
中野 圭介 東北大学, 電気通信研究所, 教授 (30505839)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2022-03-31
|
| キーワード | 形式木言語理論 / プログラム検証 / 定理証明支援系 / 双方向変換 |
|---|
| 研究成果の概要 |
形式木言語理論とは，形式的な木構造データを扱うことのできる木オートマトンや木トランスデューサに関する理論であり，効率的かつ検証可能なソフトウェアへの応用が期待されている．本研究期間ではいくつかの木トランスデューサのクラス間の関係について研究を進めたが，特筆すべき結果として，効率のよいとされるストリーム型木トランスデューサのクラスが，等価性判定問題が決定可能である最大のクラスと一致することを示すことに成功した．この研究成果により，ある種の効率的なプログラムの検証アルゴリズムの開発が期待される．
|
| 自由記述の分野 |
形式木言語理論
|
| 研究成果の学術的意義や社会的意義 |
二つのプログラムの振舞いが全く同じであるか（等価性）を検証する問題は一般に決定不能であるが，形式を制限することで決定可能になることが知られている．この制限は非常に強く，特に効率を意識したプログラムにおいてはその複雑さから等価性を判定することは困難であるとされてきた．本研究の成果では，ストリーム型変換と呼ばれる効率的かつ煩雑なプログラムについても等価性判定が決定可能であることが証明され，これはプログラム検証における新たな可能性を示している．提案した等価性判定の手法は，特定の条件下での等価性（部分等価性）の判定も扱うことができるため，後方互換性を意識したソフトウェアの保守にも応用が可能である．
|
