打合せ

先生とサテライトキャンパスで打合せ

• コマンドのプロセス代数へのマッピングをちゃんと書くこと
  • AlureやHarelの形式化の最後をプロセス代数にマッピングすることで対応
• MSCからプロセス代数へマッピングできるところの制限事項等の明確化
  • なんでも変換できるわけでは無いだろう、暗黙の制限で隠れているかも
• 制約をあたえて、最大解を求めるのは設計問題としてはあたりまえなのでなにか工夫はできないか？

というような話だった。最後の部分は興味深い。今回はgameに基づき充足解を求めているので、不動点を求める繰り返し演算の途中に外的要因を忍ばせることは可能なんだけど、、、、

あとは、朝国道１５号沿いのいつものMacで気づいたこと

• 順序制約演算の交換性に関する議論は、別の見方（充足性）ができて、それは、射影したとき、同じと見なせるあたりが怪しく、これは証明できなければ、具体例（たて・よこチェーン）ではこういう性質をもつと示すぐらいにとどめなくてはならない。

• 順序制約１つだけを、操作させると、無限の状態遷移系が得られるので、云々というのは間違い。順序制約(a→b)はaとbの離反の最大値nでパラメータ化されて、nを上限として、結局有限な状態遷移系しかできない。なかなか本質的なところ。

戦線が（私の度量に対して）長くて、あちらこちらにほころびがあります、、、
ほとんど誰もレビューしてないし、、、、。

というところで、朝Macは終了、これから家族サービスです。