多重様相論理
multi-modal logic
$ A::= P|\lnot A|A\lor A| [a]A
この$ [a] が様相記号になる
これは$ a\in Lであり、$ aをlabelと呼ぶ $ \lang a\rang A:== \lnot [a]\lnot A も導入される
多重様相論理の構造
各ラベル$ 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が成り立つ、という意味