Given two kripke structures $M_1$ and $M_2$, if $M_1\leq_{sim}M_2$ and $M_2\leq_{sim}M_1$, then does $M_1\leq_{b-sim}M_2$ holds?

intuitively, I think that it's not true, since two simulations are achieved with two different relations; while a bisimulation is "stronger", in a sense that it's one relation that acts as two simulations. But I couldn't find a counter example to aforementioned claim.


1 Answer 1


Yes your intuition is correct. The fact is that the 2 relations can be disjoint when considering just one-sided simulation relations but for bisimulation we need 1 relation with symmetry which is stronger. One counterexample is: enter image description here

$M_1\leq_{sim}M_2$ with relation {(s0, t0),(s1, t2),(s2, t2) }

$M_2\leq_{sim}M_1$ with relation {(t0, s0),(t1, s1),(t2, s1), (t3, s2) }

However for a bisimulation relation we need the tuple (s1,t1) as no other state except s1 in M1 is such that $t_1\leq_{sim}s_i$. But then s_1 has a transition to itself where L(s1) = "red" but t_1 cannot match that behaviour in M_2. So M_1 and M_2 are not bisimulation equivalent.

They are however "simulation equivalent", where we define an equivalence relation between 2 LTS as ≃ = ≼ ∩ ≼-1


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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