取りあえずは合格、コメント等は大きく分けると以下の通り、 ロジカルな深さを追求するか、ツールをつくるか？ ロジカルな深さはそんなに見込みはない、CCSを拡張しているわけでもなんでもなく、マクロ程度である だから考え方を整理したというレベルなので…

いちおうスライドは８割がたできたところで、外部審査員をお願いしていた 産総研の先生からD論草稿にコメントがかえってきた 関係の意味定義の曖昧さ CCSの拡張部分がなんかおかしい そのた書き間違え、言い間違え多数指摘 あとはCSPならこんなに素直に書け…

同じプロセス代数だと油断していたのですが、２つのプロセス代数の流派を使い分ける 理由と正しさが訴求できません。通信同期を伴わない同時実行を、ＡＣＰは含む、ＣＣＳは含まないということなのですが。これもあまり本質的ではない気がします。問題なのは…

どうも用意されている時間が２時間で、半分発表としても１時間のプレゼンを準備 しなくてはいけないことを発見。。この前、同期生のＤ論審査会にでたときの雰囲気ですね。ということでページを倍増せねば。beamerを使ってますが、とてもwordyになるので、Pow…

どうにか、内容は増やさなくても、章立ての調整で、なんとかみれる体裁にまとめた。早朝送付。今日も朝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が互い違いに手番になるのでは…

id:henjin1go:20080924の悩みを１ヶ月もたってもまだひきづってます。 プロパティφとモデルＭとモデルＭに対する操作Opに関して、Op(M)がφを満たすかどうかを充足性として、φを満たすようなＯｐを見つける問題にまたぶつかった。 ぐるぐるぐるぐるまわって、…

Gameにも色々ある 整理した。 当面プロセス代数の充足性はGameで説明で行きましょいIpod touch入力は辛い

予備審査が１２月１４日に決まったから、草稿はその２Ｗ前、２８日が閉めきりか。 すこし、伸びたが、焼け石に水か。。 最近は、シナリオ形式化部分を強化中。プロセス代数における充足性をGameと interface automataを混ぜて説明しているところを、整理する…

いろいろLatexのバージョンの違いの罠とか落ちましたが、60Pぐらいにはなりそうふと履修ガイドをみると、予備審査願いでは、願いの１枚の紙を提出するだけだった。。というわけで、論文草稿の送付には、１ヶ月の猶予があることがわかりました。といっても、…

いろいろ休み中にドラフトを埋めようとしたが、４０ページにしかならない。 会社の期末報告書ならば、簡単に計１００ページ書けるのになぜ？？firefoxからなぜかはてなDiaryにアクセスできなくなりました。Safariからはできます。 なぜ？なぜ？ プロパティφ…

少しづつ進んでいるが、後退しているかも。縦・横チェーンの結果の連動性？の説明が、口述的であったのをどうにか形式化 しようと試みた。合成結果R0の動作が、明らかに連動するSpecの動作にtrace containmentされること を示めせば、良いだろう（ほんとうか…

どうも休みは朝一番で、マックに行かないとやる気が出ない。環境のせいだろうか？家の机をきれいにしても、同じだし。なんだろうね。魔の机か。やったこと ちょっとReactive Systemsを読んだ 再帰的HLMの解について、最大の解、最小の解をもとめたい理由がわ…

休みなのですが、実家に帰ったりとなかなかすすみまません。 とにかく、これまで、雰囲気・気分だったところを、文章におとしていかなければいけません。これは骨が折れる仕事で、のらないと出来ない。 書かれてない箇所の補強 プロセス代数、プロパティ記述…

案内がきた、１０月３日しめきりだ。それまでに、ドラフトがまとまるかなあ。無理だなあ。 でもできるところまでやろう、会社の報告書は平気で１００pageかけるのだから。うまらないことはない。でもWordに慣れちゃったなあ。

久しぶりに、みなおす。最近 Acetoのamazon:Reactive Systemsにはまっていて CCSってどうやって実装されていたっけということCCS case study Maude2.0をつかって遷移ルールがかかれている 再帰方程式を素直にrewriteするととまらないのでfrozen指示子をつか…

久しぶりの打合せ。とりあえず。IPSJで指摘された問題点を解決すべき大枠をつくって望む。とりあえず、予備審査に進むことにする。予備審査というのは、ほぼ本論文ができてないといけないそうだから、とにかく今あるものをまとめるか。社内技術報告２つ分ぐ…

通信をenforceする再帰変数同士の並行結合( )は 通信に失敗する組合せを展開時に逐次に変換して消してゆく になった項は、展開をさかのぼってを伝播して消してゆく を消しながら展開方向に対して逆進する伝播Fは、項の集合に対しては単調 最大展開された項の…

★主なレビューワの指摘事項 シナリオ動作でなくて、「動作シナリオ」を定義すること シナリオ図をプロセス代数で定式化 シナリオ合成の入出力の明確化 各種定義の厳密化 ★作戦 動作シナリオは、st(X),en(X)を用いた順序制約として定義する シナリオ図のプロ…

AlfaloのInerface Automataは、いわゆるsafety-game理論に基づきインターフェースのスリ合わせをする体系なのですが、どうも、それってプロセス代数では何？とおもってはいました考えてみると、通信関数とを使った並行結合(||)演算で、通信出来ないところを…

同期入学者（同級生）で優秀な方はすでに公聴会へと駒を進めたのでこれを聴講に。 方法論の提案には、なんらかの説得力が必要とくに、ＳＷＥでは根拠が薄いから 社内でつかいましたよ ツール化しましたよ 具体的な事例で検証しましたよ がないとつらい。二木…