予備審査関係

研究 主テーマ

少しづつ進んでいるが、後退しているかも。

縦・横チェーンの結果の連動性？の説明が、口述的であったのをどうにか形式化
しようと試みた。

合成結果R0の動作が、明らかに連動するSpecの動作にtrace containmentされること
を示めせば、良いだろう（ほんとうか？）

  • 手頃なプロセス代数処理系がないのでCWB-NC(Concurrent Work Bench New Century)を使う
  • やりたいのは、チェーン挿入結果の遷移系R0が連動動作することを示すこと。
  • チェーン挿入結果の遷移系R0のアクションxをx1.xに書換え付加的なx1系のアクションを挿入。
  • 明らかに（目視で）連動していると見える遷移系Specを用意し、Specでは'x系アクションで記述
  • R0とSpecの並行結合ををとって、もともとのアクションx∈Internalsを隠蔽してSysを得る
    • Sys = (R0 | Sys) \ Internals
  • R0からx1系のアクションのみを残したZ0を得て
  • Z0とSysの間のtrace透過性を(eq -S trace Z0 Sys)にて検査。
  • Specはたまたま見つければそれで十分
  • Z0とSysは、Sys側がデッドロックに陥る遷移枝を持つのでbisimulation関係ではないことに注意。

CWB-NCって結構使えるかも。