Hennessy-Milner logic
Hennessy-Milner logic は、プロセスの性質を表現するための論理式。ちょっと複雑な性質を表現するためには Recursive Hennessy-Milner logic を使うことになる*1。これに関する資料が少ないので一応。 id:syd_syd さんに非常に感謝。
π計算のモデルチェッカには Mobility Workbench(MWB) や Advanced Bisimulation Checker(ABC) があるが、 Recursive Hennessy-Milner logic が使えるのは MWB のみ。*2
例として、"これから先、このプロセスはずっと 'a をしない" みたいな性質は次のように書く。
(max Y(a).( (['x](x#a)) & ([x]Y(a)) & ([t]Y(a)) ) )(a)
これは、 "a でない送信をする、かつ、何かを受信したら次はまたこの論理式を満たす、かつ、τ遷移したら次はまたこの論理式を満たす" と読む感じ。 [t] と
また、"このプロセスはそのうち 'a する" という性質はこんな感じ。
(min Y(a).( (<'x>(x=a)) | (<x>Y(a)) | (<t>Y(a)) ) )(a)
読み方は、"このプロセスは今すぐ 'a をするか、何かを受信したら次にこの論理式を満たすか、τ遷移したら次はこの論理式を満たす" という感じか。
間違ってる可能性もあるのでご注意ください。
- -
やっぱり間違っていました。コメント欄を参照してください。 id:syd_syd さん、いつもありがとうございます。
