# Problem with definition of bisimilarity

In my model checking class we have defined a bisimulation like this:

Let $$K=(S,S_0,Act,R,L)$$ and $$K'=(S',S'_0,Act,R',L')$$ be two kripke structures. A relation $$B \subseteq S \times S'$$ is called bisimulation if $$\,\forall (s, s') \in B$$ following points are true:

1. $$L(s) = L(s')$$
2. $$\forall \,t \in S, a \in Act: (s,a,t) \in R => \exists \, t' \in S': (s',a,t') \in R' \, \land (t,t') \in B$$
3. $$\forall \,t' \in S', a \in Act: (s',a,t') \in R' => \exists \, t \in S: (s,a,t) \in R \, \land (t,t') \in B$$

Two states $$s \in S, s' \in S'$$ are called bisimilar iff. there is a bisimulation $$B$$ with $$(s,s') \in B$$.

$$K$$ and $$K'$$ are called bisimilar if:

1. $$\forall \, s \in S_0 \, \exists \, s' \in S': s \sim s'$$
2. $$\forall \, s' \in S_0' \, \exists \, s \in S: s \sim s'$$

My problem is that this definition is defined recursively. Take for example this two structures:

$$\hskip2in$$

Of course these structures are bisimilar since they are the same but to show that $$(s_0, s'_0) \in B$$ I have to show that $$(t, t') \in B$$ and now I'm in an endless recursion.

Have I misunderstood something about the definition?

In your examples, the states are indeed bisimilar, and the relation is the set $$\{(A,A)\}$$ It is easy to verify that it satisfies the desired properties.