Game

予備審査が１２月１４日に決まったから、草稿はその２Ｗ前、２８日が閉めきりか。
すこし、伸びたが、焼け石に水か。。

最近は、シナリオ形式化部分を強化中。プロセス代数における充足性をGameと
interface automataを混ぜて説明しているところを、整理する。

• GameにはModel Checking game(MC Game)、□-game、◇-gameがある。
• MC Gameとは、モデルMとプロパティφが与えられたとき、一定のルールでPlayer1,player2が（Ｍ，φ）を書き換える
• □-gameとは、ゴールRにずっと入るような、Playe1(環境)側の勝利集合<1>□Rが求まるかどうか
• ◇-gameとは、ゴールＲにいつかはいるような、以下同じ

後者２つは、最大・最小不動点計算と関係。

プロセス代数におけるプロパティの充足性は、プロパティがHMLのような論理式で
記述される場合は、MC Gameで計算が可能であるが

プロパティをプロセスで記述する場合は、

1)プロパティ・プロセスにNG遷移をまぜておいて、M|P/LがNG遷移を示さないかを確認。

2)プロパティ・プロセスとモデルＭとのproduct（|と同じ？）をとって、環境側の勝利集合を
もとめて、これがもとのモデルと同じならば（減らないならば）、Ｍ|=φなのかな。

前者は普通で, weak trace equivalenceを使うのか、後者は独自で、最大不動点計算に帰着される。

手計算するには、MC-gameか2)がいい気がします、CWB等のツールで確認するなら1)ですな。