充足性つづきのメモ

研究 主テーマ

id:henjin1go:20080924の悩みを１ヶ月もたってもまだひきづってます。

プロパティφとモデルＭとモデルＭに対する操作Opに関して、Op(M)がφを満たすかどうかを充足性として、φを満たすようなＯｐを見つける問題にまたぶつかった。

ぐるぐるぐるぐるまわって、空き時間で考えて、なかなかまとまりません。取りあえずメモ。
これから家族サービス。

  • 最初に充足性を定義しなくてはいけない
  • プロセス代数における充足性の定義にはいろいろあるが、
  • 特にプロパティ自身をプロセスで表して、Gameに基づく充足性の定義をする
    • プロパティを表すプロセスをPとすると
    • MとPと間のproduct　M0をとって、M0に対して、環境Ｅに対するM0側の勝利戦略がある集合Win^Oを計算
    • Win^OがもともとのM0と要素が同じならば、充足する
  • P1
  • Pよりも大きいPxがあるとすると、MxがM0=Mより大きくなり矛盾
  • よってOp(P)は、Pを充足する最大の演算
  • Gameに基づく充足性計算を導入したのは、手計算で示せるから、、
  • Win^O、Win^Iの使い分けについて知見が得られた