まだまだ充足性

プロパティをプロセス代数で表すとやっぱり、何回回った(n)を意識しないと駄目みたいということで、へこむ。

充足性もまた、なやみだすが、Turn-based Gameの定義を理解して、すこしすっきり

Turn-based GameではPlayer1, Player2が互い違いに手番になるのではなくて、
状態SがPlayer1の手番の状態の集合S1,Player2の手番の状態の集合S2にわかれる

S=S1 U S2

ということであって、べつに互い違いでなくても良いのであった。

充足性を判定するときは、Player1（モデル）とPlayer2（プロパティ）の間の
Turn-based Gameになって、Player1に関する勝利集合 Win_1(S,□R)がえれたとき

Win_1(S,□R) \cap S1 = S1であるときに充足。

たぶんPlayer2の勝利集合でも同じことがいえて、充足性を判定するにはどちらでも
よい。