To find a temporal bisimulation between $w,w'$ given $w\leftrightsquigarrow w'$ where $\mathfrak M,\mathfrak M'$ (finite) are generated by $w,w'$

Question

Let $\mathfrak M$ and $\mathfrak M'$ be finite rooted models for basic temporal logic with $F$ and $P$. Let $w$ and $w'$ be the roots of $\mathfrak M$ and $\mathfrak M'$ respectively. Prove that if $w$ and $w'$ satisfy the same basic temporal formulae with $F$ and $P$, then there exists a basic temporal bisimulation that relates $w$ and $w'$.

In other words, we want to show that $w \leftrightsquigarrow w'$ (modal equivalence) in the basic temporal language gives rise to a basic temporal bisimulation. All conventions are as per Blackburn's Modal Logic textbook.

A (temporal) bisimulation is a relation $Z\subseteq W\times W'$ which satisfies five properties:

1. $wZw' \implies (w\in V(p)\Leftrightarrow w'\in V'(p))$
2. $wZw',wRv \implies \exists v'\in W' (w'R'v' \land vZv')$
3. $wZw',w'Rv' \implies \exists v\in W (wRv \land vZv')$
4. $wZw',vRw \implies \exists v'\in W'(v'R'w' \land vzv')$
5. $wZw',v'Rw' \implies \exists v\in W(vRw \land vzv')$

That being said, the challenge is to produce such a relation in our case! We only want to construct $Z$ so that $wZw'$ - what happens to other worlds, we don't care in particular (right?).

Also since we are in the temporal language, note that I am using $R$ to denote the relation associated with $F$, and $R^{-1}$ to denote the relation associated with $P$.

The strategy that I feel is best in this situation, is to produce formulae, the truth of which at $w$ (and hence $w'$) would help us come up with the above five properties. I don't think there's any other way to use modal equivalence - since all it says is that the same formulae are true at $w,w'$.

I was able to show the first property! $w\leftrightsquigarrow w' \implies (w\in V(p) \Leftrightarrow w' \in V'(p))$, by the definition of modal equivalence ($p$ holds at one world, iff $p$ also holds at the other). That hints at the fact that the required bisimulation might be the modal equivalence relation $\leftrightsquigarrow$ itself!

Unfortunately, I am unable to take these thoughts further to complete the proof - I do not know what formulae to come up with, which would help me deduce Properties 2-5.

I would appreciate any help and ideas! Thank you so much.

Answer 1

This is the other direction of the Hennessy–Milner theorem, and the crucial condition here is that $\mathfrak{M}$ and $\mathfrak{M}^\prime$ are finite.

I will show only the proof for properties 1 and 2, and the remaining ones can be proved in the similar manner. Also, cheating alert: I will use the proof by contradiction.

Let $M_w = (W^M, R^M, V^M)$ and $N_{s} = (W^N, R^N, V^N)$ be finite models such that $M_w \leftrightsquigarrow N_s$. Also, let $Z = \{(v,t) \mid M_v \leftrightsquigarrow N_t\}$. We need to show that $Z$ is a bisimulation.

1. Assume that $vZt$. By the definition of $Z$, this implies that $v$ and $t$ agree on propositional variables.

2. Assume that $vZt$ and $v R^M u$ for some $u \in W^M$. Suppose towards a contradiction that there is no $r \in W^N$ such that $tZr$ and $t R^N r$. This means that for each $r$ such that $tR^Nr$, there is a modal formula $\varphi_r$ such that $N_r \models \varphi_r$ and $M_u \not \models \varphi_r$. Since $N$ is finite, we can collect all these $\varphi_r$ in one disjunction: $\varphi := \bigvee_{tR^nr} \varphi_r$. Finally, we have that $M_v \not \models \square \varphi$ and $N_t \models \square \varphi$, which contradicts our assumption.