vault backup: 2025-04-14 09:04:56

Concurrent Systems/notes/11 - LTSs and Bisimulation.md

@@ -80,4 +80,15 @@ By hypothesis, there exists a bisimulation S that contains the pair (p, q). By d
 **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.
+- let $(x, y) \in S$ and x -a-> x'
+- if $(x, z)$ belongs to S, then, by definition, there exists y such that $(x, y) \in S_{1}$ and $(y, z) \in S_{2}$
+- since S1 is a bisimulation, there exists y -a-> y' such that $(x', y') \in S_{1}$
+- since S2 is a bisimulation, there exists z -a-> z' such that $(y', z') \in S_{2}$
+- hence, from x -a-> x', we found z -a-> z' such that $(x', z') \in S$, because there exists a y' such that $(x', y') \in S_{1}$ and $(y',z') \in S_{2}$.
+
+**Theorem:** ∼ is a bisimulation.
+*Proof:*
+The proof is done by showing that ∼ is a simulation.
+
+By definition of similarity, we have to show that $$∀(p,q)∈∼ ∀p –a–> p′ ∃q –a–> q′ s.t.(p′,q′)∈∼$$