年末は帰省して暮らしてます。仕事関係の深耕してましたが、どうも話がプロセス代数に行ってしまいます。 オートマトンの話の筈だったのに：ﾜでもプロセス項のマッチングについて知見が得られた。形式化をプロセス代数でやったと言うことなんですが、まだ御…

大分停滞している気もするが、とりあえず方向性を列挙 PA関係 IMPOSEをPAPに拡張する（記号と意味の追加) matchingをprojectionとsimulation関係で定義する １つのProcess Termを分解(例えばA/Gとか)する方法 回路組み合わせがA/Gに基づくproof graph構造に…

どうも "From PSL to NBA: a Modular Symbolic Encoding" によると。LTLはTableau法にてautomatonになるけども、PSLはLTLを拡張している からABA(Alternating Buchi Automata:universal and existential branchingが特徴)になるんだけども。 これをNBA(Non-d…

なんか重要そうな論文をみつけた。Fokkinkの論文だからいい論文だろう。 読まねば。。 # W.J. Fokkink, J. Pang and J.C. van de Pol, Cones and foci: A mechanical framework for protocol verification, Formal Methods in System Design 29(1):1-31 (Jul…

最近Kripke Structureにはまっている。原子命題AP上のKripke Structure Mとは４タプルである。 は有限の状態の集合 は初期状態の集合 は全象の遷移関係 は個々の状態で成立する命題の集合への写像関数 これは、Reactive Systemの基本モデル言語ともされるし…

Assume/Guaranteeという考え方がすごく気に入ってしまった。 仕事＞研究よりの興味ではあるんですが。 A/Gにより検証付きIPを作る A/Gによる、余分なプロトコルの削減？（指折り算の代替として） A/GでMSCのコマンドをモデル化すると、全体でのMCが不要にな…

大学のサテライトキャンパスにて所蔵本が借りれることになった。 といっても、サテライト授業関係の書籍ばっかりでありますが、 ないよりましですね。早速、HOL/Isabelle本と、Verification of reactive systems を借りた。 後者は形式検証にまつわる全てを…

打ち合わせも都合がつかないので、取りあえず加算合成関係でやれるところまでやるということで 縦横チェーンおよびそれらの合成の整理 オブジェクト合併の整理 シナリオの畳み込みを探索最適化問題として定式化（端緒） に関する作業をやった。ところで次は…

加算合成のめどがついたのですが、そこで停滞気味です。 もうちょっと最後までやろう。 現行のしくみで加算合成の出るパターンをすべて書き下してみる 実は、２つのＦＳＭの合体も加算合成の変種であることを示す。 そうすると、ずんずん、加算合成をやって…

アルゴリズムの正しさを証明するためのシステムとしてWhyをいうのがある。 こいつはoccaml風のアルゴリズム＋アサーションを入力として、各種定理証明器向けの入力を 出力するという代物です。下はsqrtの例ですが、ここまで書かないと正しさを証明はできない…

http://www.diku.dk/~yokoyama/TetsuoYokoyamaOld.htmlさんの論文Deterministic Higher-order Patterns for Program Transformationというのがあった、どうもパターン（ルール）をつかって言語変換するといいうフレームワークの理論的な論文らしい。 Higher-…

会社賢人その１と加算合成関係の話していたら、どうも、圏論で一連の論理展開は整理できるそうです。 加算合成は、圏論でいうところのPushoutに相当するそうで*1、どうもプロセス代数は有名な例だそうです。圏論が本研究の何の役に立つのかよくわかりません…

PAP上の加算合成は、つまるところは で表せる対象に、という順序依存性を インポーズするということ。対象式を展開すると ・・ M1 ・・LM3 ・・ M1ここで、bとcの順序依存性を考慮して矛盾項を消去すると。 のみが残るという計算をしますということたったそ…

PAでは、PAP(Process Algebra for Parallelism)にデッドロックとencapsulation を追加した ものを ACP(Algebra of Communicating Processes)と呼ぶのだが*1やっとencapsulation の意味がわかった。これは、通信実行（同期実行）を強制するためのオペレーショ…

いろいろ考えると、STG(状態遷移グラフ)、EDG(イベント依存グラフ)、 EPT(イベントプロセス項)、EPG(イベントプロセスグラフ) の間に成り立つ直上的な変換関係は以下のようになるのだが STG_v->STG_e->EDG->(EPTEPG) EDGをSTG_e(STG_v)に逆変換する方法がよ…

いままで、雰囲気で取り扱ってきた、イベント依存グラフを、すこし 形式化しようとしている。結局加算合成をイベント依存グラフ上で 計算しないといけないことになって、悩む。とくに状態とイベント依存 関係がごっちゃになってしまう。ふとノートを見返すと…

PAのなかのPAPのやっかいなところは、ループ構造を直接的には表せないところだ。 regularなものが必要になる。ここでPAの勉強がとまっていたが、 Regular Expressions in Process Algebra http://alexandria.tue.nl/extra1/wskrap/publichtml/200511.pd当面…

やっぱり論文形式のドキュメントはGoogleDocで書くのはつらい。 元の木阿弥 Latexに戻すことにする。MACとwindows機の間で特定のファイルやフォルダを手っ取り早くsyncさせたいのだが FolderShareなるサービスが結構使えそうだ。 https://www.foldershare.co…

Google Docs & SpreadSheets を使ってみる。 Web上のドキュメントエディタと、フォルダ。見方によっては自分用のwiki（下書き専用）といえる。 クロスプラットフォームだったり、会社と家で両方アクセス できるという意味では優れもの（会社でブロックされな…

どうも、 値ベースの状態遷移イベントベースの状態遷移 前者でかけるものが後者でかけないものがある イベント依存グラフProcess Graph これはあたりまえProcess Termでまとめても、だから何だということで、 どうもEDGが本質なのかしらん？？そうすると 値…

とりあえず目標たてないとこまる、取りあえずは 最近やっていることをネタにして、FOCUSしましょう。 MSC→EDG→ETG(PA)の流れの説明 EDG,ETGを形式化して説明 PAの加算合成のイメージをまとめる これで次回打ち合わせになるのか？？？ MACで作業するのにまだ…

今週は、やっと隙間時間をつかって検討する時間がとれた。 ９月に作った進捗レポートにあるEDG（イベント依存グラフ）を、 PAに翻訳して考えようとしている。PAもだいぶ忘れているし。。そこで、９月に書いた加算合成の絵が間違っていることを 発見。おかし…

古くて新しい組織にかあって、もう１週間がたちますが。 ここ１週間の研究活動総和時間は０です。 やはり前の会社は職種が違ったから頭の切り替えが できていたのか、通勤時間が倍増して時間が捻出できなかった のか。やりかたをかえないといけないなあー。…

昔の研究組織だ。なんか前の会社と温度が違うなあー。ノリも違うなーとりあえず、移籍のごたごたが終わったら研究活動再開だ。 あたらしいしごとの中でどういうふうに位置づけられるのかとても 不安ですが。ゆらがないために個人的な研究をしてきたのですか…

１０年ぶりのマックだ、すぐにair Wireにてネットに接続される のにはしびれた。すぐに Xをインストールして、それから、MacXWorkshopにてemacs,latex環境を インストールする。このあたりはLinuxと同じ（あたりまえか）。それにしてもフォントがきれいだ、…

復職*1することになった。どうも趣味？で 研究していたのが、研究そのものがお仕事になる予感。もっとも、即戦力としてというよりも、年寄り（若いのの刺激） としての役割が期待されているふう。まあ、ようわからんが。なるようになるさ。とにかく、今週中…

１０月から、元のＲ＆Ｄ部門に戻ることになった。５年ぶりに本職が研究職に なってしまう。趣味で研究していたのに、、あるいみ困ったなあ。

入学１年以内に、研究計画書を書くことになっているので、その打ち合わせを行った。 記述スタイル 基本は叙述的でよい、itemizeは適宜ということ 副指導教員 田中先生 背景、ひつようせいの動機をかく、設計クライシスとかそういう類 研究で明らかになった結…

仕事・そのたで時間がとれないのが９月の常だがとりあえず 予定をたてよう。行事は主テーマの「研究計画書」を だすことだ、なんとなくできそうな雰囲気なので粛々とやるべし。本編のほうの当面の方向性は プロトコルの書き下し 現行（縦・横） 多重化関係 F…

さすがに、前の論文はふるかったので、最新のバークレーの 論文をみつけた Synthesizing FSMs According to co-bu chi Properties, G. Wang, A. Mishchenko, Robert K. Brayton and Alberto L. Sangiovanni-VincentelliどうもRobert K. Brayton先生が親玉ら…