2017 Fiscal Year Annual Research Report
Refinement and Extension of Higher-Order Model Checking
| Project/Area Number |
15H05706
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
小林 直樹 東京大学, 大学院情報理工学系研究科, 教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
篠原 歩 東北大学, 情報科学研究科, 教授 (00226151)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
佐藤 亮介 九州大学, システム情報科学研究院, 助教 (10804677)
|
|---|
| Project Period (FY) |
2015-05-29 – 2020-03-31
|
| Keywords | 高階モデル検査 / プログラム検証 / データ圧縮 / 高階文法 |
|---|
| Outline of Annual Research Achievements |
本課題では、高階モデル検査の（１）理論的基盤の強化とそれに基づく高階モデル検査アルゴリズムの改良、（２）プログラム検証への応用、（３）高階モデル検査の拡張、（４）データ圧縮への応用、の４つを柱に研究を進めている。以下、それぞれの項目について、平成29年度（およびその繰越として遂行した平成30年度の一部の結果）について述べる。
（１）理論的基盤の強化：HORSモデル検査の対象である高階文法についての反復補題がある予想の下に（オーダー３の場合については無条件に）成立することを証明した。従来はオーダー２までの反復補題しか知られておらず、約40年ぶりの進展を得た。また、高階モデル検査の平均時計算量の分析の前準備として、単純型付きラムダ項の簡約列の長さについて研究し、ほとんどすべてのラムダ項が極めて長い簡約列を持つことを示した。また、Streettオートマトンを入力仕様として直接扱える新しいHORSモデル検査アルゴリズムを考案し実装した。
（２）プログラム検証への応用：プログラム検証で扱えるプログラムの規模を拡大するため、プログラムを分割して検証するための、モジュラー検証手法を開発した。また、検証で必要になる述語の推論、制約付きホーン節制約の解法などの改良を行った。
（３）拡張高階モデル検査：２種類の高階モデル検査の一つであるHFLモデル検査に整数をいれて拡張したHFLzモデル検査問題を考え、関数型プログラムの様々な検証問題がHFLzモデル検査に帰着できることを示した。これにより、これまでのHORSモデル検査に基づく方式に比べて、広範囲のプログラム検証問題を統一的に扱うことが可能になった。
（４）データ圧縮への応用：高階圧縮の知識発見への応用の試みの一環として、確率文脈自由文法を用いて自然言語の文章を圧縮する試みを行った。また、高階圧縮のための様々な要素技術について研究を進めた。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
POPL, ICLAP, ESOP, CAV, FoSSaCSなどのトップ会議に論文が採択されるとともに、理論面では反復補題に関する40年ぶりの進展、応用面ではこれまで想定していなかったHFLzモデル検査に基づく新しいプログラム検証手法が得られるなど、順調に成果がでている。
|
| Strategy for Future Research Activity |
高階モデル検査にはHORSモデル検査とHFLモデル検査の2種類があるが、後者に基づく方式の方が有望であることがわかってきたので徐々に重点を移す。
データ圧縮への応用、特にそれを通した知識発見についてはもともと萌芽的色彩の強いものであったが、難航している。形式言語の学習手法を取り入れるなどの試みを行う予定である。
|
