高階モデル検査

本ページは、JSPS科学研究費補助金 基盤研究S 「高階モデル検査とその応用」(科研費番号:23220001、 平成23〜26年度、研究代表者:小林直樹)、 基盤研究S 「高階モデル検査の深化と発展」(平成27〜31年度、研究代表者:小林直樹) の補助をうけた研究プロジェクトについての紹介です。

新着ニュース

高階モデル検査とは?

モデル検査とは、ソフトウェアやハードウェアなどのシステムを数学的にモデル化し、それが与えられた仕様を 満たす否かを判定するための手法であり、システム検証手法として現在もっとも有望視されているものの一つです。 モデル検査の概念は30年以上前に提案され、発案者のClarke教授(CMU)らが「コンピュータサイエンス分野のノーベル賞」 といわれるチューリング賞を2007年に受賞しています。

高階モデル検査とは、従来のモデル検査をより一般化、強力にしたものであり、正確には、「高階再帰スキーム」と 呼ばれる高階の木生成文法によって生成される無限木が与えられた性質(例えば「無限パスを持つか?」「aというラベルがついたノードの下にbというラベルが出現しうるか?」など)を検証する手法です。

そのような高階モデル検査が原理的に可能である(高階モデル検査問題が決定可能である)ことは 2006年にオックスフォード大学のOng教授によって証明されましたが、その最悪時間計算量が莫大(k階の高階再帰スキームの モデル検査はk重指数完全)であること、実際、Ong教授による決定可能性の証明で与えられているアルゴリズムが ほぼ常にk重指数時間かかるアルゴリズムであったことなどから、しばらくは理論家の間だけの興味の対象でした。

これに対し、2009年に小林が(1)一部のパラメタを固定すれば、高階モデル検査問題は、実は文法のサイズに対して 多項式時間で解けることを示すとともに、(2)典型的な入力に対しては効率よく動作する高階モデル検査を発見し、 さらに(3)多くの関数型プログラムの検証問題が高階モデル検査問題に帰着できることを示しました。 これによって、高階モデル検査問題はもはや理論家だけの興味の対象ではなく、応用への道が開けました。

本研究プロジェクトの概要

上の結果をふまえ、本プロジェクトでは、以下の4つのテーマについて研究を進めています。 詳しい最新の成果については小林の論文リストなどをご覧ください。 また、小林による講演のスライドのいくつかがこちらに公開されています。

プロジェクトで開発したツール群

プロジェクトで開発したツール群のうち、以下のツールのソースまたはデモ画面を公開しています。

プロジェクトのメンバー

問い合わせ先:小林(