I am working myself through the book on Modal Logic by J. van Benthem, and have a question regarding one of the questions in the book.
Specifically, it is question 1b of Chapter 3, in which we have to show that there is no bisimulation between the following two models:
We have to do this by giving a modal formula which is only true in one of the models. My idea was to use the formule $\Diamond\Diamond p$, which is clearly true in the model on the left, in the black point, but it is clearly not true in the black point on the right.
However, the book gives answers, and the formula they give is the following: $$\Box(\Box\bot\vee \Diamond\Box\bot)$$ I see why this formula works, but I do not really see why one would use this formula when there is a much easier solution available. So, this makes me think that there is something a bit wrong with my idea, but I cannot point out what it is.
Perhaps it is because their formula is true independent of the valuations of any proposition letter, but that is the only thing I can think of.
Any help is welcome!
I'm not looking at the book, so I can't be sure, but I think the point is this: the formula you gave shows that there is no bisimulation relating the black point to the black point. But it doesn't rule out the existence of any bisimulation.
The sentence given in the solution is true at every point in the model on the left, but it fails to be true at the black point in the model on the right. So it shows there can be no bisimulation between the two models.