[4K2-OS-16b] AI における離散構造処理と制約充足(2)

[4K2-OS-16b-02] グラフ書き換え言語LMNtalによる容易に拡張可能なモデル検査器の実装

〇恒川 雄太郎¹、上田 和紀¹ (1. 早稲田大学)

キーワード：モデル検査、メタプログラミング、グラフ書き換え系

LMNtalとはグラフ書き換えに基づくモデリング言語であり，そのモデル検査器SLIMは状態空間探索およびLTLモデル検査を備えている．
これまでSLIMに対して様々な拡張や変種が開発されてきたが，それらはすべてC言語で実装されたSLIMのソースコードを改変・修正することによって成されてきた．
本論文ではメタインタプリタを基礎にした容易に拡張可能なモデル検査器の実装のためのフレームワークを提案する．
フレームワークは(1)LMNtalにおける第一級の書き換え規則と(2)処理系SLIMに対するプログラム実行のためのAPIから成る．
これらの機能によってプログラマはLMNtalプログラムの状態遷移グラフを第一級のオブジェクトとしてLMNtalプログラム内で扱えるようになり，SLIMを変更することなく様々な変種を実装することが可能になる．
本研究ではLMNtalメタインタプリタを基礎にしてLTLモデル検査器，CTLモデル検査器，TCTLモデル検査器の実装および拡張を行った．