日本ソフトウェア科学会第 33 回大会 (2016 年度) 講演論文集

グラフ書き換えに基づくモデル記述言語 LMNtal
による LMNtal モデル検査器の実装
恒川 雄太郎

冨岡 太一

上田 和紀

グラフ書き換え系はモデル記述言語としてシステムの非決定的な挙動を簡潔に記述することが可能であり，実際，グ
ラフ書き換え言語 LMNtal をモデル記述言語としたモデル検査器 SLIM などが開発されている．本研究の目的はLMNtal プログラムの状態遷移グラフを扱うようなプログラムの開発を LMNtal 処理系を変更，修正することなく行えるようにすることである．これを実現するために，LMNtal に対して第一級の書き換え規則の設計，実装を行い，さらに LMNtal 処理系 SLIM のプログラム実行機能の一部を LMNtal から利用可能にする API を設計，実装
した．それを用いて，LMNtal プログラムの状態遷移グラフを扱うプログラムである，LMNtal をモデル記述言語としたモデル検査器を LMNtal で実装した．

ルタイムシステムのモデルである時間オートマトン

1 はじめにに対する TCTL モデル検査 [2]，確率的システムのモ

グラフ書き換え系はグラフとグラフ書き換え規則

デルであるマルコフ決定過程に対する PCTL モデルの集まりによって定義される．グラフ書き換え系では検査 [3] などの研究がなされている．これまで SLIM

グラフを状態としその書き換えによって状態遷移を表に対してはリアルタイムモデル検査の導入 [13] などのすことで，多様なシステムを記述できる．これまでグ研究があり，これらは SLIM の状態遷移グラフに対ラフ書き換え系で記述されるシステムを対象としたする操作を変更，拡張することによって実装されていモデル検査器は，GROOVE [15] などが開発されている．しかし，モデル検査器のような巨大で複雑なソフる．その中の１つである SLIM [11] はグラフ書き換え

トウェアの内部実装を変更することは容易ではなく，系 LMNtal によるモデル記述を対象にしたモデル検

新たなモデル検査器の迅速なプロトタイピングは難査器である．モデル検査には対象とする状態遷移系

しい．

および，その性質記述に用いる様相論理について様々

プログラミング言語 Prolog や Lisp では伝統的になバリエーションが存在し，SLIM のように離散的状言語の処理系を変更することなく，構文や意味の変更

態遷移系に対する LTL モデル検査だけでなく，リアを行うようなメタプログラミングが行われてきた [4]．
このようなメタプログラミングはメタインタプリタ

Implementation of Model checkers for LMNtal, modelling language based on Graph Rewriting, in
LMNtalYutaro Tsunekawa, 早稲田大学基幹理工学研究科 情報
理工 · 情報通信専攻, Dept. of Computer Science andCommunications Engineering, Waseda University..
Taichi Tomioka, 早 稲 田 大 学 理 工 学 術 院 情 報 理 工 学科, Dept. of Computer Science and Engineering,
Waseda University..
Kazunori Ueda, 早 稲 田 大 学 理 工 学 術 院 情 報 理 工 学科, Dept. of Computer Science and Engineering,
Waseda University..

を実装し，修正することによって達成される．これによって，新たな言語のプロトタイプ実装を行ったり，
プログラミングの対象となる個々の問題によく適応した言語機能を追加したりすることができる．実際に並行処理指向言語 Erlang の初期の処理系は Prologのメタインタプリタの発展という形で実装された [5]．
メタインタプリタの実装，修正によって言語の意味を変更することは，プログラムが言語自身の第一級のデータ構造で表現されていること，および言語処理系

の基本的機能がプログラムから利用可能であること
によって容易になる．しかし，このようなメタインタ

prove(true).

プリタは状態遷移グラフを第一級のデータ構造とし

prove(Goal1, Goal2) :-て扱わないため，モデル検査器のプロトタイプ実装のprove(Goal1),

基礎とするには十分ではない．

prove(Goal2).

本研究の目的はプログラムの状態遷移グラフを構築

prove(Goal) :-する LMNtal メタインタプリタを実装し，これを基にclause(Goal, Body),

して SLIM を変更することなく，モデル検査器のプロ

prove(Body).

トタイプ実装を行うことである．これに向けて我々はLMNtal における第一級の値として操作可能な書き換

図1

素朴な Prolog メタインタプリタ

え規則の設計，実装を行い，さらに SLIM の状態遷移グラフに対する操作の機能を LMNtal から利用すり，処理系内部の機能が clause や call といった述るための API を設計，実装した．また，LMNtal プ

語としてプログラムから利用可能であるし，Lisp でログラムの状態遷移グラフを構築する LMNtal メタ

はプログラムはリスト構造で表現され，プログラムをインタプリタを実装し，これを拡張することで LTL評価したり，関数に引数を適用したりといった処理系

モデル検査器，CTL モデル検査器のプロトタイプ実に実装されている機能を eval や apply などの関数と装を行った．

してプログラムから利用することができる．

本論文では設計した第一級書き換え規則，および

図 1 にメタプログラミングの例として Prolog によSLIM の状態遷移グラフに対する操作の機能を LM-る素朴なメタインタプリタの実装を示す．このメタイ

Ntal から利用するための API を説明する．また，実ンタプリタは Big-step semantics に基づくものであ

装した LMNtal メタインタプリタ，モデル検査器にる．すなわち，メタインタプリタは初期状態を入力とついても述べる．本研究の成果はプログラムの状態遷して，計算が発散しない場合は到達可能な最終状態を移グラフを構築するようなメタインタプリタの実装

出力する．一方計算が発散する場合は処理が終了しに必要十分な枠組みに対する一つの示唆である．

ないため，扱うことができない．このメタインタプリ
タを基礎として発展させることによって様々な拡張が1. 1 メタプログラミング

行える．たとえば，Small-step semantics に基づくメ

本論文におけるメタプログラミングとは “処理系をタインタプリタに拡張することは容易に可能である．

変更することなく言語の構文や意味を変更する” ようSmall-step semantics に基づくメタインタプリタはなメタプログラミングである．この種のメタプログラ

計算の途中過程を 1 ステップごとに追うことができ

ミングは Prolog や Lisp といった記号処理言語で伝るため，これを出力することによってトレース機能付

統的に用いられてきた手法であり，新しい言語のプロ

きのメタインタプリタを実装することができる．ユー

トタイプ処理系の実装や，プログラミングの対象とな

ザと対話的に 1 ステップごとにプログラムを実行し，る個々の問題に適した言語機能の実装に用いられて内部状態を出力するトレース機能付きメタインタプ

きた．

リタは，プログラムのデバッグに有用である．

このようなメタプログラミングが容易に可能であることは，プログラムが言語の基本的なデータ構造

1. 2 LMNtal

で表現されていることと，プログラム実行のための

本節ではモデル検査器 SLIM が対象とするグラフ

処理系の機能がプログラムから利用可能であること

書き換え系である LMNtal (の拡張である HyperLM-に起因している．たとえば，Prolog ではプログラム

Ntal: 以下単に LMNtal と書く) について簡単に述べは項と呼ばれる Prolog のデータ構造で表現されておる．詳細は文献 [10]， [9] を参照してほしい．

(P rocess) P ::= 0 | p(X1 , . . . , Xm ) (m ≥ 0) | P, P | {P } | T :-T(T emplate) T ::= 0 | p(X1 , . . . , Xm ) (m ≥ 0) | T, T | {T } | T :-T | @p | $p

図2

LMNtal の構文

LMNtal プログラムはアトム，リンク，膜，書き換

パターンマッチし，プロセス文脈は膜の中の規則以外

え規則 (以下単に規則とも書く) の四つの基本要素かのプロセスのうち，明示的に指定されていないもの全ら成る．アトム，リンク，膜は基本的なデータ構造で体とパターンマッチする．

ある階層グラフを構成する．直感的には，アトムとリ

LMNtal の構文には省略構文が存在する．アトム a

ンクはグラフ理論におけるノードとエッジに相当するの第 n 引数のリンク名の代わりにアトム b を記述す概念であり，膜によってグループ化されたグラフが階ると，アトム a の第 n 引数のリンクとアトム b の最層構造を形成する．規則は書き換え前のグラフパター

終引数のリンクが接続されているものとみなす．たとンと書き換え後のグラフパターンから成り，書き換ええば，a(X, Y), b(Y) というプロセスは省略構文を前のグラフパターンにパターンマッチした階層グラ

用いて a(X, b) と記述できる．また a(X, Y) は特別

フを書き換え後のグラフパターンへ書き換える．図 2

な 2 価アトム = (コネクタアトム) を用いて展開したに LMNtal の構文を示す．

表現 Y=Z, a(X, Z) と等価である．後者を省略構文

P はプロセスと呼ばれ，階層グラフと規則の多重集合である．0 は中身のないプロセス，p はアトム名，に変換すると Y=a(X) になり，これらはすべて同じグ
ラフ構造を表す．

Xi (0 ≤ i ≤ m) はリンク名である．アトム名は大文次に，LMNtal の拡張構文について述べる．LMN-

字アルファベット以外の英数字で始まる識別子，リンtal の拡張構文とは型付きプロセス文脈とガード付き

ク名は大文字アルファベットから始まる識別子であ規則である．型付きプロセス文脈は，グラフの性質にり，リンクの端点を表現している．! から始まるリン

関する制約を伴ってテンプレートに出現するグラフパ

ク名はハイパーグラフにおける多点間をつなぐハイ

ターンである．ガード付き規則は，ガード部と呼ばれパーリンクを表すが詳細は省く. プロセス P に 1 回る部分に記述された制約が満たされる時，書き換えをだけ出現するリンク名は P の自由リンクと呼び，P行うような規則である．たとえば，ガード付き規則に出現するそれ以外のリンク名は P の局所リンクと呼ぶ．p(X1 , . . . , Xm ) のような m 本のリンクを持つa(X, Y), $p[X] :- int($p), $p > 0 |a(X, Y), $p[Y].

アトムは m 価のアトムと呼ぶ．P, P は分子と呼ぶ.

は型付きプロセス文脈 $p が int 型という型制約を満{P } はセルと呼び，プロセス P を膜 {} によってグ

たし，かつ 0 より大きいとき書き換えを行う．int 型

ループ化して階層構造を形成する．以下，誤解のおそに属するグラフは整数をアトム名とした 1 価のアトれがないときはプロセス P を膜で囲った {P } を膜とムであり，整数アトムと呼ばれる．

呼ぶこともある．T :-T は規則であり，:- の左辺にパターンマッチしたグラフ構造を右辺のパターンに書
き換える．

1. 3 モデル検査器 SLIM
モデル検査器 SLIM はモデル記述としての LMNtal

T はプロセステンプレートと呼ばれ，規則を構成

プログラムとモデルの性質記述としての LTL 式を入する :- の左辺および右辺に出現するグラフパターン

力として，モデルが性質を満たすかどうかの検証を行である．テンプレートはアトム，リンク，膜，規則のう．SLIM は検証の際に，LMNtal の階層グラフ構造

他に @p で表されるルール文脈と $p で表されるプロ

を状態，規則によるグラフの書き換えを状態遷移としセス文脈を含む．ルール文脈は膜の中の全ての規則とた状態遷移グラフを構築する．

状態遷移グラフの構築は，未展開状態のスタックの表現できる．

先頭の状態に対して遷移先の状態を求め，求めた状態
が未展開の状態ならばスタックへ追加する処理を繰り第一級書き換え規則の構文は次のようなものである．

返して行う．遷移先の状態とはある状態に対して規則’:-’({Head}, {Guard}, {Body})の適用を行うことで得られる書き換え後の階層グラ

第一級書き換え規則は 3 価の’:-’ アトムから成る階フである．LMNtal においてある規則で書き換え可能層グラフである．この階層グラフは，全体で Headなグラフが他の規則でも書き換え可能な場合や，あ:- Guard | Body という書き換え規則を表現する．

る規則が複数の部分グラフを書き換え可能な場合に，

たとえば，次のような第一級書き換え規則

どの規則がどの部分グラフを書き換えるかは非決定’:-’({a(X, Y), b(X), c(Y)},的である．したがって SLIM は，プログラム中の各{},

規則ごとに可能な書き換えパターンを全て試すこと{b(X, Y), c(X), a(Y)})

によって遷移先の状態を計算している．
また，SLIM は階層グラフから計算したハッシュ値
をキー，状態をエントリとしたハッシュ表を用いて状態の管理を行っている．状態遷移グラフ構築の際に，はa(X, Y), b(X), c(Y) :b(X, Y), c(X), a(Y).
という規則を表現する．

遷移先の状態 s のハッシュ値から求めたエントリに既に状態が登録されている場合には，SLIM はグラフの2. 2 処理系の内部機能に対する API

同型性判定を行う．グラフの同型性判定によって，sLMNtal プログラムの状態遷移グラフを LMNtalが登録済みの状態と等しければ，s は既出の状態と判プログラムによって構築したり，効率的に管理したり定できる．また，等しくなければハッシュ値に対応すするために処理系の内部に実装されている機能に対するエントリにリンクリンストを構成して s を新規のる API の設計，および実装を行った．今回設計，お状態としてハッシュ表に登録する．

よび実装した 4 つの API を図 3 に示す．API はグラ
フパターンであり，その実装は処理系の内部機能に

2 第一級書き換え規則と処理系の内部機能に対する API

よって書き換えを行う規則である．すなわち，API のユーザはプログラム中で図 3 に示したパターンにマッ

本節では，まず LMNtal でメタプログラミングをチするグラフを生成することで，実装された規則の適行うために設計，および実装を行った第一級の書き換用という形で処理系の内部機能を利用することがで

え規則について述べる．次に，処理系の内部機能をきる．API を実装する規則はライブラリとして提供

LMNtal から利用するために設計，実装した API にしたため，API を利用するためにユーザはライブラついて述べる．

リをインポートするだけでよい．以下説明のために，個々の API をパターンマッチの対象となるアトム名2. 1 第一級書き換え規則で呼ぶ．

本研究では階層グラフ構造で表現された規則として

4 つの API のうち，rule.react_nd と membrane.eq

LMNtal における第一級書き換え規則の設計を行っは状態遷移グラフ構築のために必須の API である．

た．LMNtal プログラムは階層グラフと規則の集合で一方で，rule.react と membrane.hash は後述するあるため，規則を階層グラフ構造で表現することにモデル検査器の高速化と，効率的な状態管理のための

よって，LMNtal プログラムを LMNtal の基本デー

API である．図 3 中の RetRule や RetM em といっタ構造である階層グラフ構造の集合として表現できたリンクには，API 実行前に別のリンクで参照してることになる．したがって，LMNtal でも Prolog やいた規則や膜へのリンクが，実行後にそのまま接続

Lisp と同様にプログラムをその言語のデータ構造でされる．LMNtal のリンクは 1 対 1 接続であるため，• rule.react(RuleM em, GraphM em, RetRule, Ret)• rule.react_nd(RuleM em, GraphM em, RetRule, Ret)• membrane.hash(M em, RetM em, Ret)• membrane.eq(M em0 , M em1 , RetM em0 , RetM em1 , Ret)

図3

処理系の内部機能に対する API

API に渡した規則や膜へのリンクをこれらの引数かには RuleM em が接続される．rule.react_nd は可ら返却してもらい，API の実行後にこれらの規則や能な書き換えパターンが存在しない場合，Ret に空の膜にアクセスできるようにしている．

リストを接続する．次に rule.react_nd の使用例を

2. 2. 1 rule.react
rule.react は，RuleM em に接続された膜中の規示す．

rule.react_nd({a(X) :- b(X)},

則を GraphM em に接続された膜中のグラフに 1 ス{a(1), a(2), a(3)},

テップ適用する．適用結果のグラフを表すグラフを

retrule,Ret に接続する．適用結果を表すグラフは，適用が成

ret).

功した場合と失敗した場合で異なる．成功した場合というグラフは rule.react_nd によっては 2 価の success アトムの第 1 引数に適用後のグラ

retrule({a(X) :- b(X)}),フ，第 2 引数に Ret が接続される．また，失敗した

ret([{b(1), a(2), a(3)},場合は 2 価の fail アトムの第 1 引数に適用に失敗し{a(1), b(2), a(3)},たグラフ，すなわち元々GraphM em に接続されてい{a(1), a(2), b(3)}]).

たグラフ，第 2 引数に Ret が接続される．RetRuleというグラフに書き換えられる．[. . . ] という記法はには RuleM em が接続される．次に rule.react のLMNtal におけるリスト構造を表す．

使用例を示す．

2. 2. 3 membrane.hashrule.react({a(X) :- b(X)},

membrane.hash はハッシュ表を実装するために設{a(1), a(2), a(3)},計した API である．membrane.hash は M em に接続

retrule,された膜のハッシュ値を計算する．計算したハッシュ

ret).

値は整数アトムとして Ret に接続する．RetM em にというグラフは rule.react によってたとえばは，M em に接続された膜を接続する．

retrule({a(X) :- b(X)}),

2. 2. 4 membrane.eq

ret(success({b(1), a(2), a(3)})).

membrane.eq は M em0 に接続された膜内のグラフというグラフに書き換えられる．a(1) が a(X) :-と M em1 に接続された膜内のグラフの同型性判定を

b(X) によって書き換えられた例を示したが，a(2) ま行う．二つの膜内のグラフが同型である場合は true

たは a(3) が書き換えられる可能性もある．

アトムを，同型でない場合は false アトムを Ret に2. 2. 2 rule.react nd

接続する．RetM em0 には M em0 に接続された膜をrule.react_nd は RuleM em に接続された膜中の接続し，RetM em1 には M em1 に接続された膜を接規則を GraphM em に接続された膜中のグラフに対して 1 ステップ適用する．このとき rule.react と異なり，全ての可能な書き換えパターンに対して書き換えを行い，結果をリストにして Ret に接続する．RetRule

続する．

3 LMNtal メタインタプリタ

S := {s0 }; T := ∅; Stack := ∅本節ではまず LMNtal メタインタプリタについて

push s0 Stack

述べる．LMNtal メタインタプリタとは，LMNtal プ

while Stack ̸= ∅ログラムを入力としてプログラムの状態遷移グラフ

s := pop Stackを出力する LMNtal プログラムである．このメタイ

succ := expand(s)ンタプリタは第一級の規則と処理系 SLIM の内部機

forall s′ ∈ succ能に対する API を用いて実装を行った．また，実装

if s′ is a new state then

した LMNtal メタインタプリタと Prolog メタインタ

S := S ∪ {s′ }プリタとの違いについても述べる．

T := T ∪ {(s, s′ )}push s′ Stack

3. 1 アルゴリズム

else if (s, s′ ) is a new transition thenT := T ∪ {(s, s′ )}LMNtal メタインタプリタは入力されたプログラム
から状態遷移グラフを構築する．状態遷移グラフ構
築のアルゴリズムを示した擬似コードを図 4 に示す．

end forallend while

状態遷移グラフは状態の集合 S と状態遷移の集合 Tの組である．はじめは S は初期状態 s0 のみを要素と

図4

状態遷移グラフ構築の擬似コード

しており，T は空である．また，未展開状態のスタッ
クには初期状態のみがプッシュされている状態であ

rule.react_nd と異なり，複数の第一級書き換え規則

る．アルゴリズムは全体で 2 重ループを構成し，深を含んでよい．Graph には書き換えの対象となる階層

さ優先探索によって状態遷移グラフを構築する．1 段

グラフを含む膜を接続し，書き換え結果はリストを構目のループでは未展開状態のスタックの先頭要素に対成して Ret に接続される．この rule.react_nd_set

して状態の展開を行う．expand は渡された状態を遷を対象にした書き換えは図 4 中の expand の処理に移元として，遷移先の状態を全て返す手続きである．

相当する．

2 段目のループでは展開によって得られた遷移先状態

ハッシュテーブルの操作を行う規則について述べが新状態であるか，また遷移関係が新規であるかの判る．実装した操作はハッシュテーブルの生成，問い合定を行い，新規であればそれぞれ集合に追加する．

わせ，追加の 3 つである．このハッシュテーブルは膜をエントリとし，膜のハッシュ値をキーとしている．

3. 2 API を用いたライブラリの実装

ハッシュテーブルの生成は次の hash.init アトムを

メタインタプリタの実装にあたって 2. 2 節で述べた対象とする．

API を用いていくつかのライブラリを実装した．こhash.init(Ret)

こでは実装したライブラリを構成する規則について

書き換えの結果，Ret にハッシュテーブルが接続さ

述べる．

れる．

まず，複数の第一級書き換え規則による非決定的なハッシュテーブルへの問い合わせは次の hash.get

書き換え結果全てを計算する規則について述べる．こを対象にした書き換えによって行われる．問い合わせの規則は 2. 2. 2 節で述べた rule.react_nd を用いての際は膜のハッシュ値を計算するために 2. 2. 3 節で実装を行い，次の rule.react_nd_set アトムを対象

述べた membrane.hash を用いた．また，ハッシュ値としている．

が衝突した際には問い合わせ対象の膜とハッシュテー

rule.react_nd_set(Rs, Graph, Ret)
Rs には第一級書き換え規則を含む膜を接続するが，ブルのエントリが真に等しいことを 2. 2. 4 節で述べた membrane.eq を用いて判定している．

表現される．

hash.get(Hash, Ent, Res, Ret)state_space(States, T ransition, Ret)

Hash には問い合わせを行うハッシュテーブルを接続

States は 状 態 の 集 合 と し て の ハッシュテ ー ブ ル ，する．Ent には問い合わせ対象の膜を接続する．Res

T ransition は状態遷移の集合としてのハッシュテーには問い合わせ結果を表すアトムが接続される．問い

ブルが接続される．Ret はこの状態遷移グラフへの参合わせた膜が存在するならば，Res には次の some ア照である．状態遷移は次のような階層グラフで表現

トムの Ret が接続される．

する．

some(Ent, Ret)d(F rom, T o)

Ent にはハッシュテーブルに存在した膜が接続されF rom には遷移元の状態を表す階層グラフを含む膜，

る．問い合わせた膜が存在しない場合は，Res には 1

T o には遷移先の状態を表す階層グラフを含む膜が価の none アトムが接続される．hash.get アトムの接続される．アトム d から成る階層グラフ全体でRet には Hash に接続したハッシュテーブルが接続“F rom に接続する状態から T o に接続する状態へのされて返される．

状態遷移” を表現する．遷移関係をハッシュテーブル

ハッシュテーブルへの追加は次の hash.put を対象で管理するのは，状態 A から状態 B への遷移が複数に行われる．追加の際も問い合わせの際と同様に膜のある場合に重複する辺を除去するためである．重複す

ハッシュ値を membrane.hash を用いて計算している．

る辺を除去することによって，冗長な状態遷移グラフ

hash.put(Hash, Ent, Ret)の構築を避けることができる．

Hash にはハッシュテーブルを接続し，Ent には追加

図 5 に実装した LMNtal メタインタプリタのプロするエントリを接続する．Ret には Hash に接続したグラムを示す．各規則の先頭には識別子 rulename

ハッシュテーブルが接続されて返される．なお，Ent にを “rulename@@” のように付加した．以下説明のた接続される膜のハッシュ値を計算にも membrane.hash

めに各規則を rulename で呼ぶ．

を用いている．

プログラムの入力は前述の通り run アトムである．

run アトムは規則 run によって次に示す exp アトム
3. 3 メタインタプリタ実行の流れに書き換えられる．

本節では LMNtal メタインタプリタの実行の流れ

exp(Rs, Stk, S, T , Ret)について述べる．実装した LMNtal メタインタプリ

Rs は第一級書き換え規則を含む膜が接続される．Stk

タは LMNtal プログラムを入力として，プログラムには未展開状態のスタックが接続される．run からのの状態遷移グラフを出力する．LMNtal プログラムの書き換えでは Stk は初期状態のみが push された状状態とは階層グラフであり，状態遷移とは規則による態になる．S ，T にはそれぞれ状態の集合として状態

階層グラフの書き換えである．プログラムの非決定的のハッシュテーブル，状態遷移の集合として遷移関係な実行に伴って現れる全状態とその遷移関係を表したを表す階層グラフのハッシュテーブルが接続される．

グラフ構造を状態遷移グラフと呼ぶ．

run アトムからの書き換えでは，hash.init アトム

LMNtal メタインタプリタの入力は LMNtal プロが接続され前述のライブラリの規則によってハッシュ

グラムである．入力とする LMNtal プログラムは次テーブルが接続される．さらに，S に接続されるハッのような階層グラフ構造で表現される．

シュテーブルには hash.put によって初期状態を追加

run(RuleSet, Init, Ret)している．Ret はこの exp アトムへの参照である．

RuleSet には第一級書き換え規則を含む膜，Init に

exp アトムの書き換えは図 4 の while ループに相は初期状態を表す階層グラフが接続される．Ret はこ

当する．未展開状態のスタックが空になるまで繰りの階層グラフへの参照である．メタインタプリタの出返し状態を展開する．exp アトムは未展開状態のス

力は状態遷移グラフであり，次のような階層グラフでタック Stk が空かどうかで書き換え結果が異なる．

run@@Ret = run(Rs, {$ini[]}) :Ret = exp(Rs, [{$ini[]}], hash.put(hash.init, {$ini[]}), hash.init).
exp0@@Ret = exp({$rs[], @rs}, [], S, T) :Ret = state_space(S, T).
exp1@@Ret = exp({$rs[], @rs}, [{$f[]}|Stk], S, T) :Ret = suc({$rs[]}, Stk, {$f[]}, rule.react_nd_set({$rs[]}, {$f[]}), S, T).
succ0@@Ret = suc(Rs, Stk, {$f[]}, [], S, T) :Ret = exp(Rs, Stk, S, T).
succ1@@Ret = suc(Rs, Stk, From, [{$t[]}|Succ], S, T) :Ret = ns(Rs, Stk, From, {$t[]}, Succ, Res, hash.get(S, {$t[]}, Res), T).
new_st0@@Ret = ns(Rs, Stk, {$f[]}, {$t[]}, Succ, some({$s[]}), S, T) :Ret = nt(Rs, Stk, {$f[]}, {$t[]}, Succ, Res, S, hash.get(T, {d({$f[]}, {$t[]})}, Res)).
new_st1@@Ret = ns(Rs, Stk, {$f[]}, {$t[]}, Succ, none, S, T) :Ret = suc(Rs, [{$t[]}|Stk], {$f[]}, Succ, hash.put(S, {$t[]}), hash.put(T, {d({$f[]}, {$t[]})})).
new_tr0@@Ret = nt(Rs, Stk, From, {$t[]}, Succ, some({$s[]}), S, T) :Ret = suc(Rs, Stk, From, Succ, S, T).
new_tr1@@Ret = nt(Rs, Stk, {$f[]}, {$t[]}, Succ, none, S, T) :Ret = suc(Rs, Stk, {$f[]}, Succ, S, hash.put(T, {d({$f[]}, {$t[]})})).
図5

LMNtal メタインタプリタ

空の場合は規則 exp0 によって状態遷移グラフを表す

き換え結果が異なる．空の場合は規則 succ0 によっ

state_space アトムに書き換えられ，全体の処理はて exp アトムに書き換えられる．空でない場合は，停止する．スタックが空でない場合は，exp1 によっsucc1 によって ns アトムに書き換えられ，遷移先状て suc アトムに書き換えられ，スタック先頭の未展開

態が新規状態かどうかの判定を行う処理に移る．ns

状態を展開する処理に移る．suc アトムを次に示す．

アトムを次に示す．

suc(Rs, Stk, F r, Scc, S, T , Ret)ns(Rs, Stk, F r, T o, Scc, Res, S, T , Ret)

Rs，S ，T ，Ret は exp アトムから同名のリンクを引Rs，Stk，F r，S ，T ，Ret は suc アトムから同名のき継ぐ．Stk に接続されるスタックは exp に接続さリンクを引き継ぐ．Scc には succ アトムに接続されれていたスタックから先頭要素を取り除いたものであていた遷移先リストの先頭が取り除かれたリストがり，先頭の状態は状態遷移の遷移元の状態として F r

接続され，取り除かれた先頭の遷移先状態は T o に接に接続される．Scc には F r に接続された状態から遷続される．Res には T o に接続される遷移先状態を S

移可能な状態がリストを構成して接続される．exp かのハッシュテーブルへ問い合わせた結果を表すアトム

らの書き換えでは Scc には rule.react_nd_set アトが接続される．

ムが接続され，状態が展開される．

ns アトムの書き換えは図 4 の f orall 中で行う if

suc アトムの書き換えは図 4 の f orall ループに相文に相当する．すなわち，状態が新状態か既出の状当する．全ての遷移先状態に対して新状態であるか態かを判定する．ns アトムは Res に接続される問

どうか，また遷移が新規であるかどうかを判定する．

い合わせ結果によって書き換え結果が異なる．ハッsuc アトムは遷移先状態のリストが空かどうかで書

シュテーブルにエントリが存在しない場合は，規則

new_st1 によって suc アトムに書き換えられる．このとき，T o に接続される状態は新状態と判定され，新状態を未展開状態のスタックにプッシュ，状態のハッシュテーブルに追加する．さらに F r から T o への状態遷移が遷移関係のハッシュテーブルに追加される．
ハッシュテーブルにエントリが存在する場合は，規則

new_st0 によって nt アトムに書き換えられ，遷移関係が新規遷移関係かどうかの判定を行う処理に移る．

nt アトムを次に示す．
nt(Rs, Stk, F r, T o, Scc, Res, S, T , Ret)

図6

状態遷移グラフRes 以外のリンクは nt アトムから同名のリンクを引き継ぐ．Res には F r の状態から T o の状態への遷移関係を T の遷移関係のハッシュテーブルへ問い合わせた結果を表すアトムが接続される．

インタプリタとの違い

Prolog メタインタプリタは Prolog プログラムを入力として，プログラムから到達可能な最終状態を出力

ns アトムの書き換えは図 4 の f orall 中で行うとして列挙する．このとき，Prolog メタインタプリ

else if 文に相当する．すなわち，状態の遷移関係がタは Prolog プログラムの状態を明示的に第一級の値

新規のものか既出のものかを判定する．nt アトムはとして扱っていない．一方で LMNtal メタインタプ

Res に接続される問い合わせ結果によって書き換え結リタは状態を階層グラフ構造とし，膜を用いてその他果が異なる．ハッシュテーブルにエントリが存在しなの階層グラフと区別することによって，状態を明示的い場合は，規則 new_tr1 によって scc アトムに書きに第一級の値として扱う．また，LMNtal メタインタ

換えられる．このとき，F r から T o への状態遷移が

プリタは状態遷移を第一級のデータ構造として扱う．

新規の遷移関係であると判定し，遷移関係のハッシュ

例えば，次のような階層グラフは状態遷移を表すデー

テーブルにこの遷移関係を追加する．ハッシュテーブ

タ構造として十分である．

ルにエントリが存在しない場合も，規則 new_tr0 にd({a, b}, {a(X), b(X)})

よって succ アトムに書き換えられるが，この場合はこのアトム d から成る階層グラフは，“a, b” というハッシュテーブルに追加する操作は行わない．

状態から “a(X), b(X)” という状態への遷移関係を例としてこのメタインタプリタに次のような階層グラフを入力して実行する．

表す．状態の遷移を第一級に扱うことによって，遷移に対して情報を付加するなどの操作が可能である．

ret = run({’:-’({a(!X)}, {}, {b(!X)})},

状態および状態の遷移関係を第一級の値として扱{a(1), a(2), a(3)}).

うことができるため，LMNtal メタインタプリタでは初期状態 a(1), a(2), a(3) からの遷移先はどの a状態遷移グラフを第一級の値として扱うことができ

アトムが書き換えられるかによって 3 通りに分岐す

る．そのため，モデル検査器のような状態遷移グラフ

る．また，最終状態は b(1), b(2), b(3) のみであを操作するプログラムの実装が，このメタインタプリ

り，どのような遷移をたどっても必ず停止する．実行

タを基礎にして可能である．

結果出力される階層グラフが表現する状態遷移グラ
フを図 6 に示す．図 6 の円は状態を表し，矢印は状4 LMNtal モデル検査器

態遷移を表す．図の最も左に位置する状態は初期状態

本節ではメタインタプリタを用いて実装した LTL，であり，最も右に位置する状態が最終状態である．

3. 4 LMNtal メタインタプリタと Prolog メタ

および CTL モデル検査器について述べる．

4. 1 LTL モデル検査器
LTL モデル検査とは状態遷移系に対して線形時相(AtomicF ormula) AF ::= true

論理 (LTL) の検証を行う技術である．LTL モデル検

| false査器は LTL 式とモデル記述を入力として，モデルが| P ropositionalSymbol

LTL 式を満たす場合は真を，満たさない場合はその| not AF

ようなモデルの状態列を反例として出力する．モデル| AF and AF

が LTL 式 p で定義される性質を満たすかどうかの検| AF or AF

証は，¬p が満たされるようなモデルの状態列を網羅的に探索することによって行う．探索の対象となる状

図7

原子論理式の構文規則

態遷移グラフは，モデルと，LTL 式と等価な Büchi
オートマトンとの同期的な実行によって得られる．あ遷移関係を表す階層グラフを構成するアトム d はる LTL 式 p と等価な Büchi オートマトンとは，p をF rom に遷移元の状態を表す整数アトムを接続し，満たす状態列 s0 , s1 . . . について，原子論理式 ap のAF には後述する原子論理式を表す階層グラフを接続

列 ap0 , ap1 . . . (s0 |= ap0 , s1 |= ap1 , . . . ) をちょうどし，T o には遷移先の状態を表す整数アトムを接続す受理する Büchi オートマトンである [6]．今回実装しる．この遷移関係は AF に接続された原子論理式がた LTL モデル検査器への入力は，モデル記述として満たされる場合，F rom に接続された状態から T o にの第一級書き換え規則，初期状態の階層グラフ，お接続された状態へ遷移可能であることを表す．原子論

よび性質記述としての LTL 式の否定と等価な Büchi

理式を表すグラフは図 7 に示す構文規則によって定

オートマトンを表す階層グラフである．モデル検査器

義される原子論理式の構文木である．

はモデルが LTL 式を満たす場合は true アトムを出

図 7 中の Propositional Symbol は，次に述べるモ

力し，満たさない場合は，反例を表す状態を要素としデルの状態を対象にした命題を表す階層グラフへのたリストを出力する．

参照として，ハイパーリンクを用いて表す．モデルの4. 1. 1 性質記述

状態を対象にした命題を表す階層グラフは次の 4 価

まず，LTL モデル検査器への入力であるオートマの p アトムから成る．

トンを表す階層グラフについて述べる．オートマトンp({Head}, {Guard}, {Body}, !H)を表す階層グラフは次のような 6 価の ba アトムを用

この階層グラフは “’:-’({Head}, {Guard}, {Body})

いて表現する．

という第一級書き換え規則が適用可能であれば真，適ba(S, Delta, S0 , F , P , Ref )．

用できなければ偽” という意味の命題を表す．ハイ

S にオートマトンの状態の集合として整数アトムのパーリンク!H はこの階層グラフへの参照である．こ

リストを接続する．各オートマトンの状態は一意なのように表現された命題の真偽を計算するために 2. 2

整数アトムによって管理される．この整数アトムには節で述べた rule.react を用いる．命題を表す階層グ

後述する初期状態や受理状態と整合していれば任意

ラフから第一級書き換え規則を生成し，状態とともの整数を用いてよい．Delta に遷移関係の集合としてに rule.react によって書き換えを行う．書き換えのd(F rom, AF , T o, Ref ) というグラフのリストを

結果 success アトムが生成されれば命題は真であり，接続する．S0 には初期状態の集合として初期状態を

fail アトムが生成されれば命題は偽と求められる．

表す整数アトムのリストを接続する．F には受理状

たとえば，ある状態に対して “プロセス a(X) が出

態の集合として受理状態を表す整数アトムのリスト現する” という命題を P ，“プロセス b(Y) が出現すを接続する．P には命題の集合として前述の命題をる” という命題を Q としたとき，P ∧ (¬Q ∨ P ) とい表す階層グラフの膜を接続する．Ref はこのオートう原子論理式は図 8 に示す階層グラフによって表されマトンを表す階層グラフへの参照である．

る． 図 8 中の円はアトム，四角形は膜，アトムからことを考える．それぞれの哲学者の間には 1 本のフォークがあり，哲学者は食事をする場合にまず左にあるフォークを取る．続いて右にあるフォークを取り，フォークを 2 本獲得した哲学者は食事が可能となる．食事を終えると元の位置にフォークを戻す．このようなモデルに対して “哲学者のうち誰かが食事を行う” ということが無限回起きることを検証する．モデル記述としての第一級書き換え規則と初期状態の階層グラフの記述を図 9 に示す．図 9 に示したモデル
記述において，アトムは哲学者とフォークを表現して
図8

原子論理式 “P ∧ (¬Q ∨ P )” の階層グラフ表現

いる．哲学者とフォークを表すアトム同士のリンクによる接続関係は，哲学者とフォークが隣同士であると伸びる実線はリンク，破線はハイパーリンクを表す．

いう関係を表現している．５つの哲学者を表すアトム

また，アトムの円周上の矢印はリンクの順序を表す．

と 5 つのフォークを表すアトム，およびそれらの関4. 1. 2 実装

係を表現しているリンクによる接続関係は，全体で 1

次に，LTL モデル検査器の実装について述べる．本つの環状のグラフを構成している．このような対称な研究では文献 [8] で述べられているアルゴリズムを基

グラフ表現は食事する哲学者の問題における対称性にして実装を行った．

を自然に表現するため，モデルの状態遷移グラフは小まず，検査の対象とする状態遷移グラフの構築につさくなる．

いて述べる．この状態遷移グラフを構成する状態はモ

また，““哲学者のうち誰かが食事を行う” というこ

デルの状態 sm とオートマトンの状態 sa との組であとが無限回起きる” という性質は，図 9 に示したモる．状態の展開は，モデルの状態の展開および，オーデル記述においては，命題 p を “p_eating(L, R) な

トマトンの状態の展開によって得られる．モデルの状るプロセスが出現する” とおいて “□♢p” という LTL

態展開は，展開元となる状態に対して第一級書き換え式で表現する．“□♢p” という LTL 式の否定と等価な規則を 1 ステップ適用した結果得られる全ての状態

Büchi オートマトンの階層グラフ表現はを 2. 2 節で述べた rule.react_nd から得ることで行

ba([0, 1],う．また，オートマトンの状態展開は，展開元となる[d(0, true, 0),状態を遷移元とした遷移関係が存在し，かつ遷移元とd(0, not(!P), 1),

なるオートマトンと組になっているモデルの状態に対d(1, not(!P), 1)],

して遷移の条件となる原子論理式が真であるとき，ま[0],

たそのときに限り行う．状態遷移グラフは状態の展開[1],によって構築するが，常にその全てを構築するわけで{p({p_eating(!X, !Y)},はない．探索アルゴリズムである Nested-DFS によっ{},て訪問される状態に対してのみ状態展開を行うため，{ret(!X, !Y)}, !P)}),

状態遷移グラフの構築は反例となる状態列が発見されとなる．図 9 に示したモデル記述と初期状態，およ

たとき打ちきることができる．状態の管理は 3. 3 節

び LTL 式 “□♢p” と等価なオートマトンを表す階層

で述べた方法と同様にハッシュ表を用いて管理する．

グラフを入力として LTL モデル検査器を実行すると，4. 1. 3 例題: 食事する哲学者

反例として全員がフォークを 1 本取った状態への状態

食事する哲学者の問題はプロセスの同期に関する列が出力される．これはデッドロックに陥る状態列で問題である．5 人の哲学者が円卓に座り食事を行う

あり，検証が成功したこと示す．

// system rules’:-’({p_thinking(!Lx0, !Rx0), fork_free(!Lx1, !Rx0)},{},{p_one_fork(!Lx0, !Rx1), fork_used(!Lx1, !Rx1)}),’:-’({p_one_fork(!Lxx0, !Rxx0), fork_used(!Lxx1, !Rxx0), fork_free(!Lxx0, !Rxx1)},{},{p_eating(!Lxx2, !Rxx2), fork_used(!Lxx1, !Rxx2), fork_used(!Lxx2, !Rxx1)}),’:-’({p_eating(!Lxxx0, !Rxxx0), fork_used(!Lxxx0, !Rxxx1), fork_used(!Lxxx1, !Rxxx0)},{},{p_thinking(!Lxxx2, !Rxxx2),fork_free(!Lxxx2, !Rxxx1), fork_free(!Lxxx1, !Rxxx2)}),// init statep_thinking(L0, R0), fork_free(L0, R1),
p_thinking(L1, R1), fork_free(L1, R2),
p_thinking(L2, R2), fork_free(L2, R3),
p_thinking(L3, R3), fork_free(L3, R4),
p_thinking(L4, R4), fork_free(L4, R0).
図9

食事する哲学者のモデル記述と初期状態

4. 2 CTL モデル検査器
CTL モデル検査とは状態遷移系に対して時相論理(CT L F ormula) ϕ ::= trueの一種である計算木論理（CTL）の検証を行う技術| falseである．CTL モデル検査器への入力は CTL 式とモ| P ropositionalSymbol

デル記述であり，出力は CTL 式を満たす状態の集合| not ϕに初期状態が含まれている場合は真，含まれていな| ϕ1 or ϕ2い場合は偽である．本研究では文献 [1] で述べられて| AF ϕいるアルゴリズムを基にして，LMNtal によるモデル| EX ϕ記述を対象にした CTL モデル検査器を LMNtal で| ϕ1 EU ϕ2実装した．今回実装した CTL モデル検査器への入力は，モデル記述としての第一級書き換え規則，初期状

図 10

CTL 式の最小セットを定義する構文規則

態の階層グラフ，および CTL 式を階層グラフで表現したものである．

CTL モデル検査器への入力である CTL 式のグラフ

CTL モデル検査は入力された CTL 式 ϕ を満たす

表現について述べる．まず，入力の対象となる CTL

状態の集合を Sϕ とおいて，モデルの状態集合から Sϕ

式の最小セットを定義する構文規則を図 10 に示す．

を求める問題に帰着できる．Sϕ は論理式 ϕ の構成に

CTL 式の最小セットとは CTL の論理的同値性より，ついて帰納的に求めることができる．たとえば，p1 を

任意の CTL 式と同値な式を生成可能な最小の CTL

命題記号として “EX (not p1 )” という CTL 式 ϕ に

部分式である． モデル検査器への入力は CTL 式のついて Sϕ を求める問題を考える．まず，モデルの全最小セットの構文木を階層グラフで表現したものであ状態の集合 S から Sp1 = {s ∈ S | s |= p1 } を求める．

る．Propsitional Symbol は LTL モデル検査同様に

次に Snot p1 を求めるが，これは Sp1 の補集合である．

状態に対する命題を表す階層グラフへの参照として，最後に SEX (not p1 ) を求める．これは，Snot p1 を用

ハイパーリンクを用いて表す．

いて SEX (not p1 ) = {s ∈ S | s から s′ (∈ Snot p1 ) へ実装した CTL モデル検査器では入力される CTL

遷移が存在する } を計算することによって求めるこ

式 ϕ の構文木について，葉から根に向かって ϕ の部とができる．

分式を満たす状態の集合を帰納的に求めることによっトを用いると not (true EU (not (true EU Init)))という式で表せる．この CTL 式のグラフ表現は

not(eu(true, not(eu(true, !P)))),p({init}, {}, {}, !P).となる．検証を行った結果は真であった．確かに図 11より，任意の状態から命題 Init が成り立つ状態である 3 へ遷移可能である．

5 関連研究
グラフ書き換えに基づくモデル記述言語は存在す
るが，モデル記述言語によって実装されたモデル検査
器は著者の知る限りでは存在しない．また，モデル
記述が記述言語自身のデータ構造で表現される点は
図 11

電子レンジのモデルの状態遷移図

他のモデル記述言語にない特徴である．McErlang [7]は Erlang で実装された Erlang プログラムを対象とて ϕ を満たす状態の集合を求めている．また，CTL

したモデル検査器である．モデル検査器が対象とするモデル検査器は入力された CTL 式を満たす状態の集記述言語とその実装言語が同じである点は本研究と合をモデルの状態遷移グラフから求めることによって共通する．また，Erlang においては関数が第一級で検証を行うため，LTL モデル検査器の場合とは異なあるため Erlang プログラムの操作がある程度可能でり，検証の前段階としてモデルの完全な状態遷移グラある．しかし，Erlang の関数はデータ構造ではないフを構築する．

ため，関数自体に対して変更や修正を行うことができ

4. 2. 1 例題: 電子レンジ
CTL モデル検査器に入力するモデルの例題として，
電子レンジのモデルを扱う．電子レンジのモデルのない．一方本研究で拡張した LMNtal では規則自体を変更することができるため，Erlang と比較してより自由度の高いプログラミングが可能である．

状態遷移図を図 11 に示す．図 11 中の各状態にはそれぞれの状態に対する命題を記述している．“~” が6 まとめと今後の課題

先頭についている命題はその状態で成り立たず，そ本論文では，LMNtal でメタプログラミングを行う

れ以外の命題はその状態で成り立つことを表す．まことを目的として設計，実装を行った第一級書き換え

た，各状態の左上に記述した整数は状態の識別子を規則，および処理系の内部機能に対する API につい表す．例えば状態 3 では Close と Init という命題て述べた．プログラムの状態遷移グラフを構築するメが成り立ち，Start，Heat，Error という命題は成り

タインタプリタの実装について述べ，そのメタインタ

立たない．この電子レンジのモデルに対して CTL 式

プリタを基礎にしたモデル検査器の実装についても

AG (EF Init) の検証を行う．この式は “任意の状態述べた．提案したメタプログラミングのための枠組み

から初期状態へ戻ることが可能である” という性質をは状態遷移グラフを構築するメタインタプリタの実表している．なお，このモデルは文献 [14] で示されて装に十分であり，そのようなメタインタプリタを基礎いる例に対して，初期状態かどうかの命題 Init を各にしてモデル検査器のプロトタイピングが可能であ状態に追加したモデルである．

ることを示した．

モデル記述としての第一級書き換え規則と初期状態の階層グラフの記述を図 12 に示す．

CTL 式 AG (EF Init) は図 10 で示した最小セッ

今後の課題としては，実装した LMNtal モデル検査器の性能の向上があげられる．これに関して部分評
価 [12] と呼ばれる最適化手法について検討の価値があ//system rules’:-’({-start, -close, -heat, -error, -init}, {}, {start, -close, -heat, error, -init}),’:-’({-start, -close, -heat, -error, -init}, {}, {-start, close, -heat, -error, init}),’:-’({start, -close, -heat, error, -init}, {}, {start, close, -heat, error, -init}),’:-’({-start, close, -heat, -error, init}, {}, {-start, -close, -heat, -error, -init}),’:-’({-start, close, -heat, -error, init}, {}, {start, close, -heat, -error, -init}),’:-’({-start, close, heat, -error, -init}, {}, {-start, -close, -heat, -error, -init}),’:-’({-start, close, heat, -error, -init}, {}, {-start, close, heat, -error, -init}),’:-’({-start, close, heat, -error, -init}, {}, {-start, close, -heat, -error, init}),’:-’({start, close, -heat, error, -init}, {}, {start, -close, -heat, error, -init}),’:-’({start, close, -heat, error, -init}, {}, {-start, close, -heat, -error, init}),’:-’({start, close, -heat, -error, -init}, {}, {start, close, heat, -error, -init}),’:-’({start, close, heat, -error, -init}, {}, {-start, close, heat, -error, -init}),//init state-start, close, -heat, -error, init
図 12

電子レンジのモデル記述と初期状態ると考えている．また，今回実装を行った LTL モデ
ル検査器，CTL モデル検査器の他にも多様な状態遷
移系，様相論理に対するモデル検査器の実装は今後の課題である．
謝辞 本研究の対象である LMNtal の研究開発に携わってきた早稲田大学上田研究室の皆様に感謝しま
す．特に，研究の初期段階に有用なアドバイスを頂いた奈良耕太氏，研究に関連した検証技術について議論していただいた松本翔太氏に感謝します．

参 考 文 献[ 1 ] Clarke, E. M., Emerson, E. A.: Design and synthesis of synchronization skeletons using branchingtime temporal logic, Proc. Workshop of Logic ofPrograms, LNCS 131, Springer-Verlag, pp.52–71,
1981.
[ 2 ] Alur, R., Courcoubetis, C., Dill, D.: ModelChecking In Dense Real-Time, Inf. Comput.,Vol. 104, No. 1, pp.2–34, 1993.
[ 3 ] Kwiatkowska, M., Norman, G., Parker, D.:
Probabilistic Symbolic Model Checking with
PRISM: A Hybrid Approach, International Journal
on Software Tools For Technology Transfer, Vol. 6,
No. 2, pp.128–142, 2004.
[ 4 ] Bratko, I.: Prolog Programming for Artificial Intelligence(4th Edition), Pearson Education Canada
4th edition, 2011.
[ 5 ] Armstrong, J.: Erlang - a Survey of theLanguage and its Industrial Applications, Proc.
INAP’96, Vol. 96, 1996.
[ 6 ] Vardi, M., Wolper, P.: Reasoning about infi-

nite computations, Information and Computation,
Vol. 115, No. 1, pp.1–37, 1994.
[ 7 ] Fredlund, L., Svensson, H.: McErlang: a model
checker for a distributed functional programming
language, Proceedings of the 12th ACM SIGPLAN
International Conference on Functional Programming, pp.125–136, 2007.
[ 8 ] Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-Eﬃcient Algorithms for the
Verification of Temporal Properties, ComputerAided Verification, Springer-Verlag, pp.129–142,
1992.
[ 9 ] Ueda, K., Ogawa, S.: HyperLMNtal: An Extension of a Hierarchical Graph Rewriting Model,Künstliche Intelligenz, Vol. 26, No. 1, pp.27–36,
2012.
[10] 村山敬, 工藤晋太郎, 櫻井健, 水野謙, 加藤紀夫, 上田和紀.: 階層グラフ書き換え言語 LMNtal の処理系, コ
ンピュータソフトウェア, Vol. 25, No. 2, pp.47–177,
2008.
[11] 後町 将人, 堀 泰裕, 上田 和紀.: LMNtal 実行時処
理系の並列モデル検査器への発展, コンピュータソフト
ウェア, Vol. 28, No. 4, pp.137–157, 2011.
[12] 二村 良彦.: 計算過程の部分評価-コンパイラ · コン
パイラの一方法-, コンピュータソフトウェア, Vol. 21,
No. 5, pp.343–351, 2004.
[13] 清水 涼子, 川端 聡基, 上田 和紀.: Explicit-time
method によるモデル検査器 SLIM におけるリアルタ
イムモデル検査, 日本ソフトウェア学会第 28 回大会,
2011.
[14] Clarke, E. M., Grumberg, O., Peled, D. E.:
Model Checking, MIT Press, 1999.
[15] Rensink, A.: The GROOVE Simulator: A Tool
for State Space Generation, ProcApplications ofGraph Transformations with Industrial Relevance,
LNCS 3062, Springer-Verlag, pp.479–485, 2004.