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