複数の様相を持つ様相論理

必然性演算子▢に相当する記号が複数個出てくる

A::= P|\lnot A|A\lor A| [a]A

この[a]が様相記号になる

これはa\in Lであり、aをlabelと呼ぶ

可能性演算子◇と同様にして

\lang a\rang A:== \lnot [a]\lnot Aも導入される

多重様相論理の構造

クリプキ構造のRをラベルごとに用意する

各ラベルa\in Lに対して、R_aがある

世界は共通

世界の関係をw_1R_a w_aやw_1\xrightarrow{a} w_2のように書く

プログラムでの例

Lはプログラムの集合

Wは計算機の内部状態

w_1\xrightarrow{a} w_2は、

状態w_1で、プログラムaを実行すると、状態w_2になるということを意味する

[a]Aという論理式

プログラムaを実行したとき、aが終了したら必ずAが成り立つ、という意味

A\to[a]Bという論理式

Aが成り立っている状態でプログラムaを実行した時、aが終了したら必ずBが成り立つ、という意味