Problem with definition of bisimilarity

Question

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?

Answer 1

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.