MaudeでCCS 拡張編 (2) Hennessy-Milner logic でチェックしてみる

Maude Formal

http://www.agusa.i.is.nagoya-u.ac.jp/person/sydney/ccs-abort.maude ←今日のエントリで使っているMaudeのソースコード

ものぐさなので ちゃんと解説を書くのがめんどいのです…

問題

abort 演算子のチェックのために

  eq context = ('AbtTest =def (('a : 'b . 0 abort 'fail_a . 0  + 'd . 'e . 0 | ~ 'd . 0) \ 'd)) & 
               ('Check =def 'a . 'fail_a . 0) .

というプロセスを件の「MaudeでCCS」を使って定義した。 ここで 'AbtTest は

  1. 'a をやったら 'b をやる。 この場合 'd が選択されなかったので 'e.0 は消える
  2. 'd をやったら 'e をやる。 'a をやらなかったので abort 演算子が働いて 'fail_a をやる

という振る舞い…のはず。

これを Hennessy-Milner logic という様相論理の意味を使って確認する。

HML については Wikipedia とかを参照のこと

基本的なことをチェック

red in MODAL-LOGIC : ''AbtTest.Qid |= << ''fail_a.Act >> tt .
red in MODAL-LOGIC : ''AbtTest.Qid |= << ''a.Act >> tt .
red in MODAL-LOGIC : ''AbtTest.Qid |= << ''e.Act >> tt .
red in MODAL-LOGIC : (''AbtTest.Qid |= (<< ''fail_a.Act >> tt) /\  (<< ''a.Act >> tt)  /\  (<< ''e.Act >> tt)) .

'fail_a 、'a 、 'e で遷移する経路が一つ以上あることを確認する。 どれも true に書き換えられた。 OK。

red in MODAL-LOGIC : ''AbtTest.Qid |= << ''a.Act >> << ''e.Act >> tt .
red in MODAL-LOGIC : ''AbtTest.Qid |= [[ ''a.Act ]] [[ ''e.Act ]] ff .

'a で遷移した後 'e で遷移するパスが存在しないことを確認する。 上は false 下は true となった(下は 上の否定形)。 OK。

abort演算子のチェック その1

red in MODAL-LOGIC : ''AbtTest.Qid |= << ''a.Act >> << ''fail_a.Act >> tt .

'a で遷移したらかならず 'fail_a で遷移するパスがあるという論理式。 'aが選ばれたらabort部分はなくなるのでそんなパスはないはず。 実際falseとなった。 OK。 

red in MODAL-LOGIC : ''Check.Qid |= << ''a.Act >> << ''fail_a.Act >> tt .

念のため、この論理式がまっとうであることを確認。 この論理式は 'Check = 'a . 'fail_a . 0 というプロセスでは true となった。

abort演算子のチェック その2

red in MODAL-LOGIC : ''AbtTest.Qid |= [[ ''e.Act ]] << ''fail_a.Act >> tt .

'e で遷移したら('dで遷移したら)、 そこから かならず 'fail_a で遷移する経路が一つ以上ある。これは abort動作でやって欲しいこと。 trueとなった。 OK。

ビバ様相論理。