CTL とか(?)

モデル検査のための抽象化の話。超書きっぱなし。
かの Dams さんは、もともとの実装を完璧に真似たモデルを concrete transition model, 適当に抽象化したものを abstract transition model と呼ぶらしい。で、そのモデルの間の関係を考える。抽象化を行っても、持つ性質はできるだけ変わらないほうがいい。concrete なモデルと abstract なモデルが同じ論理式を満たすとき、その抽象化は strongly preserving であるというらしい。これは2つのモデルが strongly bisimilar であるということでいいんだろうか。Hennessy-Milner logic で区別できないプロセスは bisimilar だったはずだし。んで、weakly preserving ってのもあって、こっちは concreate なモデルが満たすすべての性質を abstract なモデルが満たす場合、らしい。
うーむ、abstract なモデルが満たす性質を concrete なモデルでも満たすことのほうが嬉しい気がするんだけどなぁ…。理解がたりん。