どうにか、内容は増やさなくても、章立ての調整で、なんとかみれる体裁にまとめた。早朝送付。今日も朝3:00起き。あと予備審査本番まで2週間で、いろいろプレゼン資料を作る作業が始まります。1時間枠だから、３０分なら３０枚か。つまり2枚/日のペースで作…

原稿かきです 交換性のロジックが、やっぱり編なので修正 そのた諸々修正 いちおう、起承転結は付いたかな、足らないところは足らないなりに？ でも見直すと、第三者的には理解できるのだろうか？？

CWB(Concurrency Work Bench)をつかって、色々作業。 交換性をcongruenceとからめて定義しなおす 連動性の性質を、合成したLTSを射影すると、（たぶん）weak congruenceがなり立つことに書き直す 縦・横チェーンを本物（バッファ長1のoverflowも辞さず型の▽…

なんかはまるところが多すぎて、（考えてなかったんだろう？）時間切れで、 ドラフト送付。Pros: 上書きされない性質がなんか出てきたのはよかった。 クロスで、上書きされない例とされる例がでてきたのもよかった いろいろいい加減な定義を、すこし明確にで…

有限性とか、クロスすればOKとかいってましたが、いろいろ、形式化をちゃんとやって精査すると、全然成り立たないことが判明。クロスしようが、だめになるケースがあります。だめにならないケースは、事例でしめすしかない（証明を展開できない）ていたらく…

脳内では、もう充足性と、▽演算の関係はきまったので、あとは書き起こす作業。その他のところ、いまわかっている範囲を分かりやすく書くように方針を変えよう。出力モード切替、まにあいません。ドラフト送付は今週末、風邪ぎみになってきたし。。

▽演算と充足性の関係をしめすところを、ノートでは概要がわかっているものを出力作業 ▽演算の操作的な意味定義 LTSを変換してみる じつはプロパティをプロセス(LTS)に変換したものとの間の並行結合演算と同等であることを示す 充足性を判定するためにつくっ…

順序制約演算を細分化（厳密化）したら、いろいろ直さなくてはならないことがでてきた特に、有限性(image finite)を示すところが、ボロボロです。なんか頭いたい。

コマンド形式化を見直してなおした、１日behind!!!! non blocking read型のチャネルはつかいません。 ACPをσdで離散化したものをつかう(ACPdか) チャネルを導入して意味定義 上記意味定義はACPなので、書き換え規則っぽくなた 以降の章では、LTSを導入して、…

先生とサテライトキャンパスで打合せ コマンドのプロセス代数へのマッピングをちゃんと書くこと AlureやHarelの形式化の最後をプロセス代数にマッピングすることで対応 MSCからプロセス代数へマッピングできるところの制限事項等の明確化 なんでも変換できる…

プロパティをプロセス代数で表すとやっぱり、何回回った(n)を意識しないと駄目みたいということで、へこむ。充足性もまた、なやみだすが、Turn-based Gameの定義を理解して、すこしすっきりTurn-based GameではPlayer1, Player2が互い違いに手番になるのでは…