AGに関する妄想。

研究 主テーマ

Assume/Guaranteeという考え方がすごく気に入ってしまった。
仕事＞研究よりの興味ではあるんですが。

  • A/Gにより検証付きIPを作る
  • A/Gによる、余分なプロトコルの削減？（指折り算の代替として）
  • A/GでMSCのコマンドをモデル化すると、全体でのMCが不要になる？？？方式！

３番目に大きな期待。

A/G自体は組み合わせ爆発に対抗する１手段で、Modular Reasoningと関連する。
それで、Clarke本(Model Checking (Cyber Physical Systems Series))なんかを読んで、Modular Reasoningに関して調査してみた。
すると、

  • ACTLのクラスでないと分割の議論ができない？
  • ACTLならば、simulation relation (biでない)が成り立ち
  • それにより分割（たぶんプロパティの）が可能となり
  • assumeたるほげ

この文献がやくにたつのかなあ？

@article{pasareanu1999agm,
  title={{Assume-guarantee model checking of software: A comparative case study}},
  author={Pasareanu, C.S. and Dwyer, M.B. and Huth, M.},
  journal={Theoretical and Practical Aspects of SPIN Model Checking},
  volume={1680},
  pages={168--183},
  year={1999},
  publisher={Springer}
}

(assume,guarantee)=$(\phi,\psi)$をLTLとおもって$\phi\rightarrow \psi$にて表現する。
$\phi$に書けるのはLTLだけ、$\psi$に書けるのはLTLとACTL

Synthesized environments can be used in model checking of (stutter-closed [1])
guarantees ψ written in LTL or ACTL.

ということで、どうもAssume側のLTLからdeterministic automatonを生成してMCに供するという
ことをするらしい。つまり"システム||LTL($\phi$由来)から合成された環境"に対して$\psi$をチェックする

【重要】つながるIP間のAssume側とGuarantee側のマッチングには simulation relationを用いたpreorderで計算。