• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2021 年度 研究成果報告書

定式化された形式木言語理論に基づくソフトウェア基盤技術の開発

研究課題

  • PDF
研究課題/領域番号 17K00007
研究種目

基盤研究(C)

配分区分基金
応募区分一般
研究分野 情報学基礎理論
研究機関東北大学 (2018-2021)
電気通信大学 (2017)

研究代表者

中野 圭介  東北大学, 電気通信研究所, 教授 (30505839)

研究期間 (年度) 2017-04-01 – 2022-03-31
キーワード形式木言語理論 / プログラム検証 / 定理証明支援系 / 双方向変換
研究成果の概要

形式木言語理論とは,形式的な木構造データを扱うことのできる木オートマトンや木トランスデューサに関する理論であり,効率的かつ検証可能なソフトウェアへの応用が期待されている.本研究期間ではいくつかの木トランスデューサのクラス間の関係について研究を進めたが,特筆すべき結果として,効率のよいとされるストリーム型木トランスデューサのクラスが,等価性判定問題が決定可能である最大のクラスと一致することを示すことに成功した.この研究成果により,ある種の効率的なプログラムの検証アルゴリズムの開発が期待される.

自由記述の分野

形式木言語理論

研究成果の学術的意義や社会的意義

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

URL: 

公開日: 2023-01-30  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi