可能世界のフレームと状態遷移構造

2019年5月27日のコメントペーパーより。レジュメは様相命題論理。

コメント：非妥当性の証明で出来上がる反例モデルのイラストが有限状態オートマトンのようだった。何か関係しているのだろうか。

回答：(あやふやな記憶だけで書きますが) 有限状態オートマトンは、

f:id:takuro_logic:20190817230639p:plain

のような状態遷移図で表せる構造ですね。状態 ( $s_1,s_2,s_3$ ) の集合とそのあいだの遷移 (矢印) によって構成され、状態の中に特別な状態として、開始状態 (ここでは $s_1$ ) と受理状態( $s_3$ )が指定されることがあります。

このような状態遷移図は、コンピュータ、より一般には何らかのシステムが、入力 (ここでは $a,b$ の2種類だけ)に応じて、その内部状態を変化させていく様子を表しているものと考えることができます (上の図は、

$abab, ababab, abababab,ababababab,\ldots$

という形の入力に対して (そしてそのような入力に対してのみ)、コンピュータが

$s_1\to s_2\to s_3\to s_2\to \cdots s_2\to s_3$

というような状態遷移を経て計算が終わる、というプログラムを表現しています)。

様相論理のフレームと何か関係があるかというともちろんあって、わたしたちがいまやっている $K$ フレームは、このような状態遷移構造のもっともシンプルな形ですね。上のオートマトンは、開始状態と受理状態があったり、遷移にも $a$ と $b$ の2種類があったりと、 $K$ フレームよりもリッチな構造ですが、逆に言えば、 $K$ フレームにいくつかオプションを乗せただけの派生形とも考えられるわけです。

ポイントは、様相論理には論理式があるということです。それにより、次のようなシステム検査が可能になります。

システムに満たしてほしい性質 (エラーが起こらないとか) を論理式で表現する。
( $\Box$ と $\diamondsuit$ だけでは表現力が弱いので、さまざまな演算子が導入されます。)
他方で、いま作っているシステムのふるまいを、状態遷移構造 (フレーム) として表現する。
1の論理式が、2において (とくにその開始状態において) 真であるかどうか、つまり満たしてほしい性質を満たしているかをチェックする。(このチェックも自動化できるように工夫する。)