チャネルの導入とその動作の操作的な意味定義がおかしい、いい加減だというわけで急遽見直ししている。どんなにダサくても、ちゃんと動作が復元できる、操作的意味をつくるしかない。もう明後日提出だし。。

先生との打合せ 「はじめに」の最初で各章で何が語られるか照会する 「おわりに」で各章で何が語られたかをサマリする 「まとめ」に設計問題からみた課題（制約をあたえて合成する＋αの話）を追加すること とくにパラメータ？に対するsensitivity?の話 「関…

家族が帰ってくるので、実質の最終日でした昨日は、朝から千葉方面に 遠征。227km走って17.4km/lの燃費、なかなかよい。ではなくて昼過ぎには 帰って、後半の補強２ やったこと 様相論理(HMLでいいから)の説明をどこかに 特に最大、最小不動点のところは補強…

ぐるぐるまわってましたが、とりあえず。形にしました。モザイク模様なのは、D論らしい。 つかれたので、今日は外の空気を吸ってきます。 やったこと ACPとCCSの関係を、前段に移動 実装のところを、うまく整理、 シナリオ合成、シナリオマージ（いわゆる後…

どうもACPとCCSの続きのところをやってると、ルールが足らなかったり、上書きの場合()の場合どするとか、いろいろ決めないといけないことが抜けてます。それにACPとCCSの関係を、「プロセス代数による形式化」の章の後でこそっと入れるのはいかにも罰がわる…

連休で家族を送り出し、ぼちぼちやってます。それにしても、この日記は Chrome+モバイル環境では、なぜかまともに記事を書くことができません、しょうがないからFireFox復活。IE8いれたろか。 やったこと ACPでの順序制約や演算について、CCSのそれを補足す…

またまた土曜は朝からMacで活動いろいろボロが見えてきましたが27日に指導教官との打ち合わせを設定して、それまでにD論をがんばって書かねば、実装ACP_drtへの展開を考えるとCCSで書かれたLTSでいろいろ検証とかするのは都合が悪いことが判明。といってもCC…

ACPもCCSもプロセス代数の一派で、どちらがどちらというわけではないのですが通信を伴わない動機並行動作を表現しようとするとACPの方が優れていて、そこからACP_drtなる離散時間版を展開したりしています。どうもD論では、CCS,ACP,ACP_drtが入り乱れていて…

いろいろ考えたら無限の内部遷移()のループに陥る可能性があることを プロパティでかけばよいではないか。 prop can_livelock = min X = livelock_now \/ <->X prop livelock_now = max X = <t>X最大不動点と最小不動点の組み合わせたプロパティになる。 proc X</t>…

Ｄ論みなおしていて、連動性の検証をCWBでやっていたのだがどうも変だ X=a.b.X, Y=c.d.Yのとき Z=X|Yに対して ZはXあるいはYに対する連動性がありません ずっとX(Y)が占有する可能性があるから というのをCWBで占めそうとおもったのですが obseqオプションは…

順序制約に関する正しい分解法則を整理して、横チェーンの見直しと縦チェーンの見直しをほぼ終了。ふと振り返って、それ以前の充足性の判定とか演算の導入とかみると、いまやったところと温度差がありすぎ、記法もバラバラ、n巡目を区別するといっていてもな…

最近の考察に従い横チェーンの検証の節を少し修正、１時間３０分で少しすすんだ、毎日やらないとだめだ。。

期末に突入したので、Ｄ論が書けません。。なぜかPGSolverに現実逃避 danilewskiの例 Piotr Danilewski's Slides Page18/54 http://react.cs.uni-sb.de/fileadmin/user_upload/react/gamesseminar08/Danilewski-Slides.pdfがうまくできないと、問い合わせて…