ドラフト

いろいろ休み中にドラフトを埋めようとしたが、４０ページにしかならない。
会社の期末報告書ならば、簡単に計１００ページ書けるのになぜ？？

firefoxからなぜかはてなDiaryにアクセスできなくなりました。Safariからはできます。
なぜ？なぜ？

• プロパティφとモデルＭとモデルＭに対する操作Opに関して、Op(M)がφを満たすかどうかを充足性として、φを満たすようなＯｐを見つける問題にまたぶつかった。
• eMSCの場合は、プロパティが順序制約(a→b)であり、Oｐは演算(a→b)である。
• 順序制約をそのままOpに置き換えれば、充足することは自明？であるが逆はいえない
  • φを満たすOpは「自明なOp」以外に沢山ある。
• 一般的（なのか？）に、最大（most general)なOpを最大不動点をつかって求めるのがgameの家風なのだが
  • どうも「自明なOp」がそれに当たっているようだという感触はあったが、やっぱりそうだと思った
• 例えばTICCを使えば、エンコードできて説明だけはできる。

あとは形式化と説明をどう工夫するかですね。。まあドラフトだから掘っておくかな。