ループのあるPA

研究 主テーマ

久しぶりに PA本
Introduction to Process Algebra (Texts in Theoretical Computer Science. An EATCS Series)
を読む。

"4.Recursion"に進むが難しい。

ACP(Algebra of Communicating Processes)がfiniteな動作しか記述できない
ので、普通の状態遷移に現れるループを取り扱えないということがわかる。

そこでRecursionという拡張をしましょうという話。

"Guarded Recursion"というものが定義され（guardedは関数定義風のtermが
とある形式を満たすことが条件)る。Guarded recursionで定義された
specification Eに対して、recursion変数Xに対して なるプロセスが
定義されて、これがループのある状態遷移グラフのstateに相当するもの
になる。

はホニャララを満たすプロセス（つまり集合）なので
とかをつかって記述できるプロセスグラフは、ずいぶん
様子が違うことになる。

大事な定理は、

  • 定理4.2.1 guarded recursionで拡張されたACPは、ACPの保守的な拡張である
  • 定理4.2.2 双模倣はguarded recursion付きACPに対してcongruence(一致・合同)である。

ということらしい。
次は regular processに拡張されていくらしい。