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?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top