モヤモヤの点検(1)

研究 主テーマ

どうももやもやしているところは以下

  • 順序制約演算(\nabla演算)をかける話とチャネル挿入の話の整理

順序制約\psiを充たすような、（最大の）全体の遷移系を求めるために\nabla_{\psi}を適用するというところまではOK.でも実際は遷移系としては、並行に動作する、LTSとして実現されてそれらの間のチャネル通信として、もとの全体の遷移系と同等な実装を得るわけであって、その間のギャップがもやもやの一つ。

  • FIFOを挿入するという話はOKで、それともとのLTSとの同等性を示すこと
  • 「全体遷移系→パーティショニング→個別LTS＋チャネル同期」という形にもってゆく
  • \nabla_{\psi}のケースは、たまたま演算とチャネルの挿入が、XXXXというみで結果が同等になるというはなしなのか？
  • 普通のLTSをバラバラにしてチャネルとプロトコル挿入がでてくるのか？
  • 普通のLTSをバラバラにすると、連動制約がでてきて、これとチャネルが関係するのか？
  • もともとチャネルを介して繋がるLTSを一つにするというパスもあるだろう

一般的にLTSを分解して連係制約を得るのは難しい問題であるが、パーティショニングということではなにかあるのか？