ACP,CCS

研究 主テーマ

ACPもCCSもプロセス代数の一派で、どちらがどちらというわけではないのですが通信を伴わない動機並行動作を表現しようとするとACPの方が優れていて、そこからACP_drtなる離散時間版を展開したりしています。

どうもD論では、CCS,ACP,ACP_drtが入り乱れていて整合性がないという欠点が指導教官から指摘(d:id:henjin1go:20090714)されていましたが、これの収拾策をねっている。

  • コマンドは同一スレッドないのアクションの実行順（一応前順序かな）を規定していて、シナリオは複数スレッドにまたがるアクション間の順序制約を規定している。コマンドとシナリオの実行順序制約をあわせれば、可能な（許容される）プロセスの全容があきらかになる。
  • この辺まではCCSで計算をします。
  • いったん可能なプロセスがCCSでみつかると、そこからこれをACPとみなすと、CCS的な動作以外に通信を伴わない同期並行動作が付け加わります。ACPで表された可能な振る舞い（トレース）を列挙して、これをACP_drtに翻訳すれば、実装にちかいtimedなモデルに展開できます。

なので、今まではコマンドをACP_drtで形式化します。といっていたのは間違えで、

  • 実装(timtedなモデル)はACP_drtで形式化します
  • コマンドやシナリオは順序制約としてCCSで形式化します
  • CCSとACP_drtを結ぶのがACP