利用者:Qnighy/高階モデル検査

計算機科学において、高階モデル検査 (higher-order model checking)はモデル検査問題の亜種で、システムの振る舞いが高階関数によって決定される場合を扱う。

定義

高階モデル検査は、与えられた高階再帰スキームが生成するラベル付き木が、交替性パリティオートマトンによって受理されるかを判定する問題である。

ラベル付き木

一般的なモデル検査では、検証対象のシステムを有限状態機械などで記述するが、高階モデル検査では無限の状態を扱うため、検証対象のシステムは無限木として定義される。

ランク付きアルファベット (ranked alphabet) とは、関数 $\Sigma \colon \mathrm {dom} (\Sigma )\to \mathbb {N}$ であって $\mathrm {dom} (\Sigma )$ が有限のものである。このとき、各 $a\in \mathrm {dom} (\Sigma )$ は 終端記号 (terminal symbol) と呼ばれ、 $\Sigma (a)$ は a のアリティをあらわす。

Σ-ラベル付き木 (Σ-labeled tree) とは、(有限とは限らない)根つき木 T に以下の情報を追加したものである。

• 各頂点 v に終端記号 $T(v)\in \mathrm {dom} (\Sigma )$ が対応づけられている。
• 各頂点 v にはちょうど $\Sigma (T(v))$ 個の子ノードが存在し、それぞれの辺は 1 から $\Sigma (T(v))$ までの整数で付番されている。

高階モデル検査では、ラベル付き木を高階再帰スキームで記述し、その性質を交替性パリティオートマトンで記述する。

高階再帰スキーム

高階再帰スキームは、再帰を許した単純型つきλ計算によってラベル付き木を記述する方法である。

高階再帰スキームにおける単純型はソート (sort) あるいはカインド (kind) と呼ばれる。ソートはただ1つの基本型を持つ単純型で、以下のように帰納的に定義される。

• 特別な記号 o について、 o はソートである。
• $\kappa _{1}$ と $\kappa _{2}$ がソートであるとき、 $(\kappa _{1}\to \kappa _{2})$ はソートである。 「$\to$」は右結合として、曖昧性の虞れがないときは括弧を省略する。たとえば、 $\mathrm {o} \to \mathrm {o} \to \mathrm {o}$ は $(\mathrm {o} \to (\mathrm {o} \to \mathrm {o} ))$ の略記である。

ソートにはアリティ (arity) と オーダー (order) と呼ばれる自然数が以下のように割り当てられている。アリティは引数の個数、オーダーは高階関数の高階さをあらわす。

• $\mathrm {arity} (\mathrm {o} )=0$
• $\mathrm {arity} (\kappa _{1}\to \kappa _{2})=\mathrm {arity} (\kappa _{2})+1$
• $\mathrm {order} (\mathrm {o} )=0$
• $\mathrm {order} (\kappa _{1}\to \kappa _{2})=\max\{\mathrm {order} (\kappa _{1})+1,\mathrm {order} (\kappa _{2})\}$

このとき、高階再帰スキーム (higher-order recursion scheme) とは、組 $(\Sigma ,{\mathcal {N}},{\mathcal {R}},S)$ であって、以下の条件を満たすものである。

• Σはランク付きアルファベットである。
• ${\mathcal {N}}$ は有限集合 $\mathrm {dom} ({\mathcal {N}})$ の各元にソートを割り当てる関数である。各元 $F\in \mathrm {dom} ({\mathcal {N}})$ は非終端記号 (non-terminal symbol) と呼ばれる。
• ${\mathcal {R}}$ は各非終端記号 $F\in \mathrm {dom} ({\mathcal {N}})$ にλ項を割り当てる関数である。このλ項は全てのλ抽象が先頭にある形 ($\lambda x_{1}.\,\lambda x_{2}.\,\ldots \lambda x_{n}.\,t$, ここで t は型 o を持つアプリカティブなλ項) でなければならない。より正確には、アプリカティブなλ項は以下のように帰納的に定義される。

 * 終端記号 $a\in \mathrm {dom} (\Sigma )$ はアプリカティブなλ項である。