Peledの弟子筋のGunterの"Compositional Message Sequence Charts"をよんだ。

いわゆるITUのMSC(HMSC)は、メッセージのsend/recvがランデブー的であるという制限により記述自由度が低いという文句にたいして、sendもrecvも待たなくて良い（遅延可能）というふうに拡張したものを提唱(Compositional MSC:CMSCと呼ぶ)

この条件緩和により、イベントの出現に関する非決定性が生じる。

left-closedという性質を導入することにより、

"relalizable HCMSC"というのが、初期ステートから展開する全ての有限パスが、left-closed CMSCであるという定義がなされる。

最後に、任意のFSMによるプロトコル記述から、HCMSC記述を自動的に生成する手順を明何している。この手順んは一意ではなくて、cutpointという集合をより小さく見つける能力に依存しているらしいくて、この集合を発見するのは NP-hardということ。

さて次は本丸をのぞくぞ。。。