まだまだカバーし切れていない、プロセス代数の要素がある。イントロ本以外にもクリーニ演算子＊ への拡張とか、もあるし。。。とりあえずmCLR2本にある基本演算はカバーしないとな。 Restriction: Blocking: Renaming: Commnication:

どうも細切れの時間と、本業と干渉がここのところ激しく検討が進まない。 指折り残について考えてみた。あれは結局、複数FSMを組み合わせた サブシステムとしてみたときに、ある性質ψを満たすためには、 不要なプロトコルがあるよということを指折り演算によ…

MacのTV広告の動画が、AppleのWebサイトで公開されている。 Macに模した青年と、Windows機に模したサラリーマンとの 掛け合い漫才風のものだ。これを一種の比較広告として、Appleの広告も地に落ちたと する意見もあるが、これがなんかちがう。米国サイトには…

形式的手法のサーベイをおこなっていると、やはり不動点は避けて通れない。 前出のKripke構造のところであったが。まずは least fixedpoint: greatest fixedponit: というのが難問だなあ。どうしてになるものの下限（下のぎりぎり）が最小不動点になるかな？…

年末ずっとやっていた、プロセス代数でワークフローシステムの定式化を 試みていたが、どうもうまく纏まらない。とくに、プロセス項同士の部分マッチというのが今100歩である、最初は 順序依存関係のマトリクスを作って、これにて比較を行うことを試みたが …