2019 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)
佐藤 亮介 九州大学, システム情報科学研究院, 助教 (10804677)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| Project Period (FY) |
2015-05-29 – 2020-03-31
|
| Keywords | 高階モデル検査 / プログラム検証 / 不動点論理 / 高階文法 / データ圧縮 / 確率付き文法 |
|---|
| Outline of Annual Research Achievements |
本課題では、高階モデル検査の（１）理論的基盤の強化とそれに基づく高階モデル検査アルゴリズムの改良、（２）プログラム検証への応用、（３）高階モデル検査の拡張、（４）データ圧縮への応用、の４つを柱に研究を進めている。以下、それぞれの項目について、2019年度（およびその繰越として遂行した2020年度の一部の結果）について述べる。
（１）理論的基盤の強化：高階モデル検査の平均時計算量について、ある仮定のもとで、ほとんどすべての問題は（性質を表現するオートマトンのサイズに関して）k重指数時間完全であるという結果を得た。また、もう一種の高階モデル検査であるHFLモデルについて、確率の入った拡張を考え、その決定不能性を示すとともに、決定可能なサブクラスを与えた。
（２）プログラム検証への応用：これまでのHORSモデル検査に基づく方式の集大成として、7000行程度からなる高階モデル検査器HorSat2のコードの検証実験を行い、単純な性質については全自動で検証を行えることを確認した。
（３）拡張高階モデル検査：２種類の高階モデル検査の一つであるHFLモデル検査に整数を加えて拡張したHFLzモデル検査問題とそのプログラム検証への応用について研究を進めた。オーダー1のHFLモデル検査の応用として、Cプログラムの時相的性質の自動検証ツールなどを作成し、その有効性を確認した。また、HFLの特殊ケースである制約付きホーン節(CHC)への帰着を通して、破壊的代入やオブジェクトを持つプログラムの自動検証手法を考案・実装して有効性を示した。
（４）データ圧縮への応用：確率付き文法を用いた高階圧縮方式を考え、その理論的有効性を示すとともに、圧縮に用いる確率付き高階文法を自動で獲得するためのアルゴリズムとして、確率付き文脈自由文法の学習に用いられるInside-Outsideアルゴリズムの高階文法への拡張を考案した。
|
| Research Progress Status |
令和元年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和元年度が最終年度であるため、記入しない。
|
