vault backup: 2025-04-14 08:59:56

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
+**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.
+