From 0c758d98a240ed3730e80234c275dac7d196e528 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Wed, 30 Apr 2025 13:27:49 +0200 Subject: [PATCH] vault backup: 2025-04-30 13:27:49 --- .obsidian/workspace.json | 56 ++++++++---------- .../notes/12b - CCS cose varie.md | 4 +- .../notes/13 - Weak Bisimilarity.md | 10 ++-- Concurrent Systems/notes/14.md | 28 ++++----- .../images/Pasted image 20250415082906.png | Bin .../images/Pasted image 20250415090109.png | Bin .../images/Pasted image 20250428083727.png | Bin .../images/Pasted image 20250428084340.png | Bin .../images/Pasted image 20250428085410.png | Bin .../images/Pasted image 20250428085837.png | Bin .../images/Pasted image 20250428175449.png | Bin .../images/Pasted image 20250429082812.png | Bin .../images/Pasted image 20250429082905.png | Bin .../images/Pasted image 20250429083129.png | Bin .../images/Pasted image 20250429083455.png | Bin .../images/Pasted image 20250429083535.png | Bin .../images/Pasted image 20250429084358.png | Bin .../images/Pasted image 20250429084921.png | Bin .../images/Pasted image 20250429084950.png | Bin .../images/Pasted image 20250429085319.png | Bin .../images/Pasted image 20250429091029.png | Bin .../images/Pasted image 20250429091959.png | Bin .../images/Pasted image 20250429092055.png | Bin .../images/Pasted image 20250429092305.png | Bin .../images/Pasted image 20250429092543.png | Bin 25 files changed, 45 insertions(+), 53 deletions(-) rename Pasted image 20250415082906.png => Concurrent Systems/notes/images/Pasted image 20250415082906.png (100%) rename Pasted image 20250415090109.png => Concurrent Systems/notes/images/Pasted image 20250415090109.png (100%) rename Pasted image 20250428083727.png => Concurrent Systems/notes/images/Pasted image 20250428083727.png (100%) rename Pasted image 20250428084340.png => Concurrent Systems/notes/images/Pasted image 20250428084340.png (100%) rename Pasted image 20250428085410.png => Concurrent Systems/notes/images/Pasted image 20250428085410.png (100%) rename Pasted image 20250428085837.png => Concurrent Systems/notes/images/Pasted image 20250428085837.png (100%) rename Pasted image 20250428175449.png => Concurrent Systems/notes/images/Pasted image 20250428175449.png (100%) rename Pasted image 20250429082812.png => Concurrent Systems/notes/images/Pasted image 20250429082812.png (100%) rename Pasted image 20250429082905.png => Concurrent Systems/notes/images/Pasted image 20250429082905.png (100%) rename Pasted image 20250429083129.png => Concurrent Systems/notes/images/Pasted image 20250429083129.png (100%) rename Pasted image 20250429083455.png => Concurrent Systems/notes/images/Pasted image 20250429083455.png (100%) rename Pasted image 20250429083535.png => Concurrent Systems/notes/images/Pasted image 20250429083535.png (100%) rename Pasted image 20250429084358.png => Concurrent Systems/notes/images/Pasted image 20250429084358.png (100%) rename Pasted image 20250429084921.png => Concurrent Systems/notes/images/Pasted image 20250429084921.png (100%) rename Pasted image 20250429084950.png => Concurrent Systems/notes/images/Pasted image 20250429084950.png (100%) rename Pasted image 20250429085319.png => Concurrent Systems/notes/images/Pasted image 20250429085319.png (100%) rename Pasted image 20250429091029.png => Concurrent Systems/notes/images/Pasted image 20250429091029.png (100%) rename Pasted image 20250429091959.png => Concurrent Systems/notes/images/Pasted image 20250429091959.png (100%) rename Pasted image 20250429092055.png => Concurrent Systems/notes/images/Pasted image 20250429092055.png (100%) rename Pasted image 20250429092305.png => Concurrent Systems/notes/images/Pasted image 20250429092305.png (100%) rename Pasted image 20250429092543.png => Concurrent Systems/notes/images/Pasted image 20250429092543.png (100%) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index d853c81..03f87b5 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -6,7 +6,6 @@ { "id": "ceb8ca67f2b32f40", "type": "tabs", - "dimension": 44.62750716332378, "children": [ { "id": "ec8d1a91f1f0cc7e", @@ -14,34 +13,28 @@ "state": { "type": "markdown", "state": { - "file": "Concurrent Systems/notes/14.md", + "file": "Concurrent Systems/notes/13 - Weak Bisimilarity.md", "mode": "source", "source": false }, "icon": "lucide-file", - "title": "14" + "title": "13 - Weak Bisimilarity" } - } - ] - }, - { - "id": "23a71d5ae1bd9e0f", - "type": "tabs", - "dimension": 55.37249283667622, - "children": [ + }, { - "id": "ae2c5ab99ad6ca6a", + "id": "4151b8cc103dc898", "type": "leaf", "state": { "type": "pdf", "state": { - "file": "Concurrent Systems/slides/class 14.pdf" + "file": "Concurrent Systems/slides/class 13.pdf" }, "icon": "lucide-file-text", - "title": "class 14" + "title": "class 13" } } - ] + ], + "currentTab": 1 } ], "direction": "vertical" @@ -210,26 +203,25 @@ "companion:Toggle completion": false } }, - "active": "ae2c5ab99ad6ca6a", + "active": "4151b8cc103dc898", "lastOpenFiles": [ - "Pasted image 20250429092543.png", - "Pasted image 20250429092305.png", - "Pasted image 20250429092055.png", - "Pasted image 20250429091959.png", - "Concurrent Systems/slides/class 14.pdf", - "Concurrent Systems/notes/14.md", - "Pasted image 20250429091029.png", - "Pasted image 20250429085319.png", - "Pasted image 20250429084950.png", - "Pasted image 20250429084921.png", - "Pasted image 20250429084358.png", - "Pasted image 20250429083535.png", - "Pasted image 20250429083455.png", "Concurrent Systems/notes/13 - Weak Bisimilarity.md", - "Concurrent Systems/slides/class 13.pdf", - "Concurrent Systems/notes/12 - Calculus of communicating system.md", - "Concurrent Systems/slides/class 12.pdf", "Concurrent Systems/notes/12b - CCS cose varie.md", + "Concurrent Systems/notes/12 - Calculus of communicating system.md", + "Concurrent Systems/notes/14.md", + "Concurrent Systems/notes/images/Pasted image 20250415082906.png", + "Concurrent Systems/slides/class 14.pdf", + "Concurrent Systems/notes/images/Pasted image 20250429092543.png", + "Concurrent Systems/notes/images/Pasted image 20250429092305.png", + "Concurrent Systems/notes/images/Pasted image 20250429092055.png", + "Concurrent Systems/notes/images/Pasted image 20250429091959.png", + "Concurrent Systems/notes/images/Pasted image 20250429091029.png", + "Concurrent Systems/notes/images/Pasted image 20250429085319.png", + "Concurrent Systems/notes/images/Pasted image 20250429084950.png", + "Concurrent Systems/notes/images/Pasted image 20250429084921.png", + "Concurrent Systems/notes/images/Pasted image 20250429084358.png", + "Concurrent Systems/slides/class 13.pdf", + "Concurrent Systems/slides/class 12.pdf", "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", "HCIW/slides/HCI in the car.pdf", "Concurrent Systems/notes/10 - Implementing Consensus.md", diff --git a/Concurrent Systems/notes/12b - CCS cose varie.md b/Concurrent Systems/notes/12b - CCS cose varie.md index f375353..6f2e06e 100644 --- a/Concurrent Systems/notes/12b - CCS cose varie.md +++ b/Concurrent Systems/notes/12b - CCS cose varie.md @@ -10,7 +10,7 @@ $$S_{2}^{(2)} \triangleq v \cdot S_{1}^{(2)}$$ If we consider S(2) as the specification of the expected behavior of a binary semaphore and S(1) | S(1) as its concrete implementation, we can show that $$S^{(1)}|S^{(1)} \space \textasciitilde \space S^{2}$$ This means that the implementation and the specification do coincide. To show this equivalence, it suffices to show that following relation is a bisimulation: -![](../../Pasted%20image%2020250415082906.png) +![](images/Pasted%20image%2020250415082906.png) ## Restrictions **Proposition:** $a.P \textbackslash a ∼ 0$ @@ -50,7 +50,7 @@ One of the main aims of an equivalence notion between processes is to make equat **This feature on an equivalence makes it a *congruence*** Not all equivalences are necessarily congruences (even though most of them are). To properly define a congruence, we first need to define an execution context, and then what it means to run a process in a context. Intuitively: -![200](../../Pasted%20image%2020250415090109.png) +![200](images/Pasted%20image%2020250415090109.png) where C is a context (i.e., a process with a hole ☐), P is a process, and $C[P]$ denotes filling the hole with P diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md index 20ac799..70d5d1b 100644 --- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md +++ b/Concurrent Systems/notes/13 - Weak Bisimilarity.md @@ -27,7 +27,7 @@ $\approx$ is a 4. $\sim \subset \approx$ #### Examples of weakly bisimilar processes -![](../../Pasted%20image%2020250428083727.png) +![](images/Pasted%20image%2020250428083727.png) **Theorem:** given any process P and any sum M, N, then: 1. $P \approx \tau.{P}$ @@ -41,7 +41,7 @@ take the symmetric closure of the following relations, that can be easily shown 3. $S=\{ ((M+\alpha.P+\alpha.(N+\tau.P), M+\alpha.(N+\tau.P)) \} \cup Id$ #### Weak bisimilarity abstracts from any $\tau$ -![](../../Pasted%20image%2020250428084340.png) +![](images/Pasted%20image%2020250428084340.png) **There exists no weak bisimulation S that contains (P, Q).** *Proof:* @@ -71,7 +71,7 @@ A possible implementation of this specification is obtained by having two worker - For difficult works, they have to use the special machine. There is only one special and only one general machine that the workers have to share. -![](../../Pasted%20image%2020250428085410.png) +![](images/Pasted%20image%2020250428085410.png) where rg and rs are used to require the general/special machine, lg and ls are used to leave the general/special machine, and S and G implement a semaphore on the two different machines. @@ -83,7 +83,7 @@ i.e., that the specification and the implementation of the factory behave the sa Let N denote {rg,rs,lg,ls} and x,y ∊ {E,M,D} We can prove that the following relation is a weak bisimulation: -![](../../Pasted%20image%2020250428085837.png) +![](images/Pasted%20image%2020250428085837.png) This is a family of relations: - 3 pairs of the second form (one for every x) @@ -101,7 +101,7 @@ We want to model a lottery L where we can select any ball from a bag that contai The specification is: $$L \triangleq \tau.\bar{p_{1}}L+\tau.\bar{p_{2}}.L+\dots+\tau.\bar{p_{n}}.L$$ where $\tau$'s represent ball extractions and $\tilde{p_{i}}$ is the action that communicates with the value of the extracted ball. The LTS resulting from this specification is: -![](../../Pasted%20image%2020250428175449.png) +![](images/Pasted%20image%2020250428175449.png) We now build a system with n components, one for every ball. diff --git a/Concurrent Systems/notes/14.md b/Concurrent Systems/notes/14.md index f49d324..20dab58 100644 --- a/Concurrent Systems/notes/14.md +++ b/Concurrent Systems/notes/14.md @@ -7,19 +7,19 @@ Inference system = axioms + inference rules - completeness: whatever is bisimilar, it can be inferred #### Axioms & Rules for Strong Bisimilarity -![350](../../Pasted%20image%2020250429082812.png) +![350](images/Pasted%20image%2020250429082812.png) quite obvious. -![350](../../Pasted%20image%2020250429082905.png) +![350](images/Pasted%20image%2020250429082905.png) basically we can let the left or the right process evolve, leaving the other unchanged, or they can synchronize. -![350](../../Pasted%20image%2020250429083129.png) +![350](images/Pasted%20image%2020250429083129.png) - if a process does not perform any action, a restriction won't do anything - ... -![350](../../Pasted%20image%2020250429083455.png) +![350](images/Pasted%20image%2020250429083455.png) -![](../../Pasted%20image%2020250429083535.png) +![](images/Pasted%20image%2020250429083535.png) $P$ is in standard form if and only if $P \triangleq \sum_{i}\alpha_{i}P_{i}$ and $\forall_{i}P_{i}$ is in standard form. **Lemma:** $\forall P \exists P'$* in standard form such that $\vdash P = P'$ @@ -28,15 +28,15 @@ $P$ is in standard form if and only if $P \triangleq \sum_{i}\alpha_{i}P_{i}$ an **Base case:** $P \triangleq 0$. It suffices to consider $P' \triangleq 0$ and conclude reflexivity. **Inductive step:** we have to consider three cases. -![](../../Pasted%20image%2020250429084358.png) -![](../../Pasted%20image%2020250429084921.png) -![](../../Pasted%20image%2020250429084950.png) +![](images/Pasted%20image%2020250429084358.png) +![](images/Pasted%20image%2020250429084921.png) +![](images/Pasted%20image%2020250429084950.png) replacing one by one every continuation with its standard form, obtaining standard form. -![](../../Pasted%20image%2020250429085319.png) +![](images/Pasted%20image%2020250429085319.png) ### Axioms & Rules for Weak Bisimilarity -![](../../Pasted%20image%2020250429091029.png) +![](images/Pasted%20image%2020250429091029.png) #### Example A server for exchanging messages, in its minimal version, receives a request for sending messages and delivers the confirmation of the reception @@ -55,9 +55,9 @@ Let us consider the parallel of processes M and R, by using the axiom for parall By using the same axiom to the parallel of the three processes, we obtain $$\vdash S|(M|R)=send.(\overline{put}|(M|R))+put.(\overline{go}|R|S)+go.(\overline{rcv}|S|M)$$ By restricting *put* and *go*, and by using the second axiom for restriction, we have that: -![](../../Pasted%20image%2020250429091959.png) +![](images/Pasted%20image%2020250429091959.png) We now apply the third axiom for restriction to the three summands: -![](../../Pasted%20image%2020250429092055.png) -![](../../Pasted%20image%2020250429092305.png) -![](../../Pasted%20image%2020250429092543.png) +![](images/Pasted%20image%2020250429092055.png) +![](images/Pasted%20image%2020250429092305.png) +![](images/Pasted%20image%2020250429092543.png) diff --git a/Pasted image 20250415082906.png b/Concurrent Systems/notes/images/Pasted image 20250415082906.png similarity index 100% rename from Pasted image 20250415082906.png rename to Concurrent Systems/notes/images/Pasted image 20250415082906.png diff --git a/Pasted image 20250415090109.png b/Concurrent Systems/notes/images/Pasted image 20250415090109.png similarity index 100% rename from Pasted image 20250415090109.png rename to Concurrent Systems/notes/images/Pasted image 20250415090109.png diff --git a/Pasted image 20250428083727.png b/Concurrent Systems/notes/images/Pasted image 20250428083727.png similarity index 100% rename from Pasted image 20250428083727.png rename to Concurrent Systems/notes/images/Pasted image 20250428083727.png diff --git a/Pasted image 20250428084340.png b/Concurrent Systems/notes/images/Pasted image 20250428084340.png similarity index 100% rename from Pasted image 20250428084340.png rename to Concurrent Systems/notes/images/Pasted image 20250428084340.png diff --git a/Pasted image 20250428085410.png b/Concurrent Systems/notes/images/Pasted image 20250428085410.png similarity index 100% rename from Pasted image 20250428085410.png rename to Concurrent Systems/notes/images/Pasted image 20250428085410.png diff --git a/Pasted image 20250428085837.png b/Concurrent Systems/notes/images/Pasted image 20250428085837.png similarity index 100% rename from Pasted image 20250428085837.png rename to Concurrent Systems/notes/images/Pasted image 20250428085837.png diff --git a/Pasted image 20250428175449.png b/Concurrent Systems/notes/images/Pasted image 20250428175449.png similarity index 100% rename from Pasted image 20250428175449.png rename to Concurrent Systems/notes/images/Pasted image 20250428175449.png diff --git a/Pasted image 20250429082812.png b/Concurrent Systems/notes/images/Pasted image 20250429082812.png similarity index 100% rename from Pasted image 20250429082812.png rename to Concurrent Systems/notes/images/Pasted image 20250429082812.png diff --git a/Pasted image 20250429082905.png b/Concurrent Systems/notes/images/Pasted image 20250429082905.png similarity index 100% rename from Pasted image 20250429082905.png rename to Concurrent Systems/notes/images/Pasted image 20250429082905.png diff --git a/Pasted image 20250429083129.png b/Concurrent Systems/notes/images/Pasted image 20250429083129.png similarity index 100% rename from Pasted image 20250429083129.png rename to Concurrent Systems/notes/images/Pasted image 20250429083129.png diff --git a/Pasted image 20250429083455.png b/Concurrent Systems/notes/images/Pasted image 20250429083455.png similarity index 100% rename from Pasted image 20250429083455.png rename to Concurrent Systems/notes/images/Pasted image 20250429083455.png diff --git a/Pasted image 20250429083535.png b/Concurrent Systems/notes/images/Pasted image 20250429083535.png similarity index 100% rename from Pasted image 20250429083535.png rename to Concurrent Systems/notes/images/Pasted image 20250429083535.png diff --git a/Pasted image 20250429084358.png b/Concurrent Systems/notes/images/Pasted image 20250429084358.png similarity index 100% rename from Pasted image 20250429084358.png rename to Concurrent Systems/notes/images/Pasted image 20250429084358.png diff --git a/Pasted image 20250429084921.png b/Concurrent Systems/notes/images/Pasted image 20250429084921.png similarity index 100% rename from Pasted image 20250429084921.png rename to Concurrent Systems/notes/images/Pasted image 20250429084921.png diff --git a/Pasted image 20250429084950.png b/Concurrent Systems/notes/images/Pasted image 20250429084950.png similarity index 100% rename from Pasted image 20250429084950.png rename to Concurrent Systems/notes/images/Pasted image 20250429084950.png diff --git a/Pasted image 20250429085319.png b/Concurrent Systems/notes/images/Pasted image 20250429085319.png similarity index 100% rename from Pasted image 20250429085319.png rename to Concurrent Systems/notes/images/Pasted image 20250429085319.png diff --git a/Pasted image 20250429091029.png b/Concurrent Systems/notes/images/Pasted image 20250429091029.png similarity index 100% rename from Pasted image 20250429091029.png rename to Concurrent Systems/notes/images/Pasted image 20250429091029.png diff --git a/Pasted image 20250429091959.png b/Concurrent Systems/notes/images/Pasted image 20250429091959.png similarity index 100% rename from Pasted image 20250429091959.png rename to Concurrent Systems/notes/images/Pasted image 20250429091959.png diff --git a/Pasted image 20250429092055.png b/Concurrent Systems/notes/images/Pasted image 20250429092055.png similarity index 100% rename from Pasted image 20250429092055.png rename to Concurrent Systems/notes/images/Pasted image 20250429092055.png diff --git a/Pasted image 20250429092305.png b/Concurrent Systems/notes/images/Pasted image 20250429092305.png similarity index 100% rename from Pasted image 20250429092305.png rename to Concurrent Systems/notes/images/Pasted image 20250429092305.png diff --git a/Pasted image 20250429092543.png b/Concurrent Systems/notes/images/Pasted image 20250429092543.png similarity index 100% rename from Pasted image 20250429092543.png rename to Concurrent Systems/notes/images/Pasted image 20250429092543.png