 Given two LTSs, one may ask whether they satisfy the same formulas. The notion of bisimulation has become the standard measure for equivalence of Kripke models and Labeled Transition Systems. A bisimulation between the LTSs M = (W, R,V) and M′ = (W′,  R′, V′) is a binary relation Z between their states such that for all worlds x in M and for all worlds x′ in M′, if xZx′ then