IPSJ対策の現状 - henjin1goの日記

★主なレビューワの指摘事項

シナリオ動作でなくて、「動作シナリオ」を定義すること
シナリオ図をプロセス代数で定式化
シナリオ合成の入出力の明確化
各種定義の厳密化

★作戦

動作シナリオは、st(X),en(X)を用いた順序制約として定義する
シナリオ図のプロセス代数での定義
1. $\nabla$ 演算の再帰方程式への導入(SOSを用いて)
2. $\nabla$ 演算の望ましい性質（有界性等）の定義
3. 縦チェーン・横チェーンを $\nabla$ 演算で形式化し、「望ましい性質」を満たすことを提示
4. 「望ましい性質」をもつ $\nabla$ 演算は、組み合わせると「こんな性質」を持つ
5. シナリオ図は縦・横チェーンが連携した $\nabla$ 演算システムに対応
シナリオ合成の入出力の明確化
1. シナリオ図(制約システム)＋コマンドの並列結合=合成後の再帰方程式
2. シナリオ図は「こんな性質」をもつから、演算適用の交換性？が成り立つ
3. いろいろグリグリできる
順序制約でいろいろぐりぐりする
1. シナリオマージは制約システムのマージ
2. シナリオ図の書き方により、本来充足不能のシステムもありうる。
3. 簡単な実装（maude)

実は、プロセス代数では同期通信の強要( $\partial_H . \Gamma$ による)による再帰方程式の合成演算が、safety-gameにより説明されることがわかっている（ref個人通信)。 $\nabla$ 演算による再帰方程式の合成演算も、NoGOODの定義が違うだけで同じ枠組みでかたれます。

じゃあ何が違うのか？ $\nabla$ 演算のほうが同期通信を含有します。えっへん。