4
$\begingroup$

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?

$\endgroup$
4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.