# 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?

You seem to be confusing the definition of bisimilarity with an algorithm for finding a bisimulation.

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.

This means that the structures are indeed bisimilar.

What you were trying to do is to find an algorithm for constructing a bisimulation, given the two different structures. If you try to proceed by taking the initial states, and moving through paths, then you indeed encounter a problem with cycles. (By the way, if the structures were trees, or DAGs, then your approach would work).

This is why algorithms for finding bisimulations typically take a different approach -- namely refinement: you start with a naive relation (e.g., everybody is bisimilar to everybody), and whenever you find a mismatch, you refine your relation.

Take a look at the "fixpoint" definition of bisimilarity here, and try to extract an algorithm from it.