先生の指摘事項の修正中、進みません。今日は24/31まで進行。

校正を合間をぬって行う。いろいろ学会の流儀があるんだなあー。 「同士」→「どうし」 「一旦」→「いったん」 「全て」→「すべて」 「A.Tarski」→「Tarski, A.」 言い回しが変だだったり、表の説明が本文に内のもあったりして冷や汗もの。得意のEXPACKにして…

情報処理学会の投稿論文の著者校正が来た。いろいろ直すプロというのがいるものだなあ。１３日までに直して送らないといけない。またD論をやっと担当先生が見てくれて、いろいろ間違え（ミスプリレベル）の指摘が来る。 とりあえず直しますが、これを直して…

D論は無事２日の11時AMに到着した（EXPACKはいいな）ところが、どうも論文は、簡易製本してあることが必要だそうで（閲覧に供するため）、簡易製本のファイルを遅れとの連絡が教務係からきた。いそいでファイルを準備し、会社の帰りにEXPACKで送った。製本し…

迫る締め切り 学生各位標記につきまして、本日１０月２日（金）１７時が締切となっております。 時間厳守とし，１７時以降は受領しませんので注意して下さい。 H21.10.2 学生課教務係 追う郵便 ■お問い合わせ番号 XXXXXXXXXX (EXPACK500)◇通過 10月1日 22:25…

チャネル周りの意味論を見直してなんとか、それ以降の展開式が説明できるのでまあいいか。というところでやめた。よくよく調べると、２日が締め切りというのは２日に石川に物理的についてないといけないらしい。。。。家に帰って、最終修正して、必要書類を…

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

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

とn=2とすればよいというのがこの前の話でしたが、n=2ならばとなるわけですしかしを考慮すると、なわけですから、 この制約はだけで十分なわけです。つまりn=∞というわけで横チェーンはという風情になります。追い越し制限が∞ということはOW型の制約というこ…

まえの横チェーンの制約（型の制約を利用）は強すぎて、それから７月に思いついた新横チェーンは緩すぎて、いまのところこてこてのFSMで定義した真横チェーンがよさそうな雰囲気というところまできましたが、制約の要素部品を、とn=2とすれば解決できそうで…

家族サービスウイークに、D論を進めようとかんがえましたが。なんと「研究ノート」を忘れてしまって、まずは大きくざせつ。とはいっても記憶とはてなDiaryをもとに再構築します。横チェーンの進捗状況までフォローアップして終了、あとは目次を見直しました…

休み中に、LaTeX原稿を整備して、著者の写真をカメラのキタムラにてとる等の準備。投稿論文の最終原稿を用意して、プリント２部して、kinkosで作業して、エクスパックにて送付。電子データは別途送付、これにて１０月に著者校正が来るまで作業はない。さて１…

１ヶ月たちましたが、予測どおり（８月の第１水曜日）に採録通知がきた ［情処論文誌：お知らせ］（09-XXXX）投稿論文(採録内定) 15日までに、いろいろコメント反映や、化粧直しをして原稿提出する必要があるうらしい。ううんこのお盆にー！

いちおう論文ではSafety Gameに従って充足性の形式化をしましたが、それをツールで確かめる手段がTICCしか（わるいか）なくて、単なるGameなのにInterface Automataとかを説明した上でTICC用にエンコードした事例を示すわけにもいかないなあ、とおもっていた…

なかなか研究がすすみません、が、JALで移動中に考えた 横チェーンの制約と、演算がぜんぜん種類が違うことを再発見（忘却していたともいう） 縦チェーンも横チェーンのときと同じように素直な制約ってなんだろうと思うと、どうも、ではないだろうか、それだ…

前回の打ち合わせのメモを書くのを忘れていたので記載 コマンド→シナリオ→MSの流れがよくわからない とくにデータと操作という観点であいまいになっている シナリオ合成した結果はFSMですよとか ACPとCCSの関係をちゃんと明らかにしておくこと、なぜそれを選…

IPSJへの投稿がどうやら採録になった旨を、アンオフィシャルに教えてもらった苦節４年弱、３度目（DAC,IPSJ１回目)の正直。でも内容がちょっと不正確なところがあったりして；；同じタイトル始まりの投稿論文があったりして；；

ぼちぼちやってます。個人用にdynabook UXかったのでこれのテスト 新横チェーンはの掛け算で構成できるか？ 結果：少し違う。原因：まだ探索中

24日の打合せで9月卒業が無くなったので、ぼーっとしていましたが 気を取り直して、Ｄ論整備。横チェーンでcntがマイナスになると23日の日記では騒いでいましたが、そんなことは忘れて 今日再発見。上書き型の連係プロトコル挿入の結果のFSMの構造がやっと正…