 We say that two LTSs are bisimilar when there exists a bisimulation between them.  It is known since the beginning of PDL that in two bisimilar LTSs M and M′, for all worlds x in M and for all worlds x′ in M′, if xZx′ then for all PDL formulas A, x  ∈ V(A) iff x′  ∈ V′(A). Thus when two LTSs are bisimilar under the definition of bisimulation above, it is the case that, if xZx′ then