大疑問

あと充足性計算って、普通の遷移系の形式化ではなににあたる？trace containment?

全てのMのトレースをψに射影したものは、ψに受理される

模倣性とtrace containmentは関係し、模倣性はGameで計算できるから、充足性がgameで計算できるのは、自明だったりする。

HenzingerのAlternating Simulationと関係するのかしら、