いろいろ考えたら無限の内部遷移()のループに陥る可能性があることを プロパティでかけばよいではないか。 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の構造がやっと正…

例が古くて、がたがたなので、最新の環境で検証ししようとする。横チェーンで繰り返し(cnt)を考慮する場合って、追い抜きがexocr(a) = ocr(a) - ocr(c)と いうことは、マイナスになることがあるのね。というわけで本当は難しかった。もうツール化するしかな…

とりあえず、３つのうち２つは出来て、３つめは目処が立った。Gameによる定式化は、どこにも正しい参考文献がないから、いろいろかき集めて付録に書いていたいのを忘れていた。http://d.hatena.ne.jp/henjin1go/20081101 これに従えば、ちゃんと計算を説明で…

だいぶ立ってしまったが、予備審査時に出した草稿を修正中。7月初旬に、実は提出期限が来る予定なので、それまでに直るのか、追加できるのか？まずは、予備審査のときに、外部審査員の先生に指摘された事項を振り返る（いまごろ？？）色々鋭いしてきがあって…

昨日の夜と早朝でなんとか修正。いろいろ直した。 LTSとプロセスと状態遷移機械がごちゃごちゃだったのでなおした 順序制約[tes:\psi]の間違えの修正 順番をかえた コマンドの説明を追加して、構造をもつMSCからの合成のイメージを出した 複雑性への言及 い…

先日の同期の件は、実装とCCSの間のギャップという話であるが、大して問題になりそうになさそう。 ということで、落着しよう。それよりも、肝心の順序制約の意味が揺らいで、投稿論文にだしたもの(2月)はなんか違っている。むしろ予備審査に出した物(12月)が…

そういえば、並行実行するLTS間の動作を定義するにあたって、並行実行(|)を 考慮しなくてもよいの？LTS間でアクションの順序関係を定義するならば、同時に実行する場合ってどうするの？CCSはとの間のみに同期通信が発生してと遷移するんだったわね。だからそ…

IPSJへの投稿の結果「条件付き採録」となった、査読者コメントの主なものは以下のとおり 計算時間に関する言及（アルゴリズムの複雑さへの言及ということ） 演算は、まあ単なるかけ算にすぎないはなし 充足性計算は、最小不動点を求める演算なのでこれは既知…

どうももやもやしているところは以下 順序制約演算(演算)をかける話とチャネル挿入の話の整理 順序制約を充たすような、（最大の）全体の遷移系を求めるためにを適用するというところまではOK.でも実際は遷移系としては、並行に動作する、LTSとして実現され…

あと充足性計算って、普通の遷移系の形式化ではなににあたる？trace containment?全てのMのトレースをψに射影したものは、ψに受理される模倣性とtrace containmentは関係し、模倣性はGameで計算できるから、充足性がgameで計算できるのは、自明だったりする…

４月末には、投稿論文の結果が判明するけども、それまでなにもしないわけにはいかない。4/初が6月卒業申請でしたから、9月卒業申請は7月初、論文投稿の可否は判定していますが D論をまとめるのに必要な部分を整備しなくては、4-5月に進捗報告する、別の投稿…

情処の投稿論文で手で計算したところがあるので、これをticc改で動かす ことを再構築中。いきなりABCD型の例題をかましてみるも、連動演算を挿入する ことにより、本来ならば単純な直積よりも遷移系の規模が小さくなるはずのに、 同じ遷移数と状態数。なにか…

すみません、あれから仕事が期末で、あまりすすんでいません。見直しています。IPSJへの投稿論文でticcをつかって実験的なことをしたのですが、 途中手で行うところが多々あったのを、すこし自動化するというところから入ります。今日は、ocamlの勉強、別フ…

情処の特集に投稿した。いつもギリギリもう疲れました。