diff --git a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md index 67fd42d..27438b6 100644 --- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md +++ b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md @@ -72,4 +72,12 @@ $S^{−1} = \{(q0,p0), (q1,p1), (q1,p2), (q2,p0)\}$ >Bisimilarity is an equivalence relation *Proof:* -Reflexivity: we have to show that q ∼ q, for every q. Consider the following relation \ No newline at end of file +**Reflexivity:** we have to show that q ∼ q, for every q. Consider the following relation $S ={(p,p):p∈Q}$ and observe that it is a bisimulation (the inverse is S itself). + +**Symmetry:** we have to show that p ~ q implies q ~ p, for every p, q. +By hypothesis, there exists a bisimulation S that contains the pair (p, q). By definition of bisimulation, $S^{-1}$ is a simulation; hence, $(q, p) \in S^{-1}$ and, consequently, q ~ p. + +**Transitivity:** we have to show that `p ~ q` and `q ~ r` imply `p ~ r` for all p, r, q. Let's consider the following relation: $S = \{(x, y): \exists y : (x, y) \in S_{1} \land(y,z)\in S_{2}\}$ + +where S1 and S2 are bisimulations, then we have to show that S is a bisimulation. +