Bisimulation games to compare equivalent but not bisimilar BML models

Question

Two BML models M, w and N, w' are given: in M, w has with infinitely many R-transitions of finite length, and in N, w' has infinitely many R-transitions and also includes an infinite-length R-transition.

How can one use bisimulation games to prove that M, w and N, w' are equivalent but not bisimilar?

Answer 1

Non-bisimilarity. That the models you described are not bisimilar can be shown as follows. Pick an arbitrary $n \in \mathbb{N}$, and consider formula $$\varphi_n:= \Diamond^n \top \land \square^{n+1} \bot$$ that intuitively means that from the current state in a model, we can make $n$ steps but not $n+1$ steps.

Now, it is clear that no matter which $n$ you pick, $\varphi_n$ will be satisfied in $(M,w)$ on the chain of length $n$ (and will be false on longer chains). For each finite chain of length $n$ there will be a corresponding $\varphi_n$ true at the start of the chain (state $w$). At the same time, no matter how large $n$ is, $\varphi_n$ is not satisfied at the beginning of the infinite chain $(N,v)$. Thus, each finite chain has a formula that distinguishes it from the infinite chain. This implies, that $(M,w)$ and $(N,v)$ are not bisimilar.

Modal equivalence. To claim that $(M,w)$ and $(N,v)$ are modally equivalent we can indeed use modal games, where Spoiler chooses a move in one of the models, and Duplicator tries to match the move in another model. In the last round of the game, if the current states satisfy the same propositional variables, then Duplicator wins, else Spoiler wins. It is known that Duplicator has a winning strategy in an $n$-round modal game iff $(M,w)$ and $(N,v)$ satisfy the same modal formulas up to modal depth $n$.

With this in mind, you can assume towards a contradiction that $(M,w)$ and $(N,v)$ are not modally equivalent. Hence, there is a $\varphi$ of modal depth $n$ such that $(M,w) \models \varphi$ and $(N,v) \not \models \varphi$. After that, you show by induction that for each move of Spoiler there is a corresponding move of Duplicator (basically you need to go along a chain of appropriate length), and the game ends in states satisfying the same propositional variables. This gives you the desired contradiction.