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

大分停滞している気もするが、とりあえず方向性を列挙 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 を借りた。 後者は形式検証にまつわる全てを…

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