From ea8f9c9de658d035056388ba2eb995d45d042600 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 14 Apr 2025 09:04:56 +0200 Subject: [PATCH] vault backup: 2025-04-14 09:04:56 --- .../notes/11 - LTSs and Bisimulation.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md index 27438b6..c6a75bc 100644 --- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md +++ b/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′)∈∼$$