 It is readily seen that the two instances of LTSs above are bisimilar. A bisimulation Z between M and M′ can be given as: Z = {(x1,y1), (x1,y2), (x2,y3), (x2,y4)}. The states x1 and y1 satisfy exactly the same PDL formulas. So do the states x1 and y2, etc. 