Process Algebra本(1)

とりあえず、薄くて安い本

をamazonでかって、読むことにした。

簡単そうであるがそうでもない。

とりあえず今日は

2.Basic Process Algebra　までを朝マクドで処理。

この本は、大学生(undergrad)向けとうたってはおりますが。。

• BPAには +と・しか基本演算子？として用意されてない
• trace等価性というのがあって、
• bisimulation等価は transitionシステムに対する等価なこと
• trace等価であるといってもbisimulation等価ではない。
• bisimulation等価性は簡単には証明できないが
  • axiomを導入して機械的にできる
  • axiomは　= と　bisimulationとの間の関係で
  • sound性や complete性について語っている
  • equality(=)関係が BPA上のbisimulation等価性を特徴づけるといっている。
    • equality(=)関係は、「s=tならば sBt」といういみで　soundである
    • equality(=)関係は、「sBtならばs=t」といいういみで completeである
  • complete性を証明するのに、axiomをTRSに書き下し
  • そのTRSの停止性やeualityを利用して証明しているらしい。

ううん、なんだか難しい。。それにやたら Appendixへの参照に飛ぶし。