クリプキ構造について

クリプキ構造とは　
ブール値でラベル付けされた遷移状態中の式で評価される非決定性有限オートマトン。公平性制約 (訳者註：あるイベントが必ず起きてくれることを保証するようなこと）で拡張することが出来る（Webster's Online Dictionary）

。。。なんのこっちゃ。

クリプキ構造は非決定性有限オートマトンの一種である。サウル・クリプキが1963年に発表した。あるシステムの振る舞いというものを表現して、そのモデルを検証する際に使用されている。基本的にグラフである。　ノードがシステムの到達可能状態を表し、エッジは遷移状態を表す。ラベル関数はそれぞれのノードを対応する遷移状態一組のプロパティに変換する役割を持つ。時相論理はクリプキ構造に変換出来ることが知られている。

正式な定義

まず、APを原始命題（これ以上分割出来ない論理式。例えばa=trueとか「今年は閏年だ」とかn<10みたいな)と決める。

クリプキ構造は4つのタプル（集合の要素の集まりみたいなもの）から成る。このように↓
M=(S,I,R,L)

この時の、
Sは有限の状態の集合

Iは初期状態の集合で　I⊆Sと表せる（有限状態集合であるSの部分集合ということ）。

Rは遷移リレーション。　R⊆S×S（RはSとSの直積集合の部分集合のこと）と表せる。ここで、∀s∈S、∃s'∈S
のとき（有限状態集合Sに属する全ての（任意の）要素sと少なくとも1つ以上のs'があるとき）、Rはsからs'の遷移関係を要素に持つ集合である。例えばある時刻にsという状態のものが次の時刻にs'となるようなリレーションのことである。

Lはラベリング関数。　各状態で真になる原始命題APの集合を与える関数　（Wikipedia, the free encyclopedia）　

※「状態」とは例えば信号器の状態なら「赤」とか「青」とか。ビデオデッキの状態なら「録画中」とか「電源オフ」とか。

原文
KRIPKE STRUCTURE 　From　Webster's Online Dictionary
A nondeterministic finite state machine whose states are labeled with boolean variables, which are the evaluations of expressions in that state. It may be extended with fairness constraints. (references)

KRIPKE STRUCTURE 　From 　Wikipedia,the free encyclopedia
A Kripke structure is a type of nondeterministic finite state machine proposed by Saul Kripke in 1963, used in model checking to represent the behaviour of a system. It is basically a graph whose nodes represent the reachable states of the system and whose edges represent state transitions. A labeling function maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures.

Let AP be a set of atomic propositions, i.e. boolean expressions over variables, constants and predicate symbols.