diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 836497b..a569f6b 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -28,12 +28,12 @@ "state": { "type": "markdown", "state": { - "file": "Concurrent Systems/notes/13 -.md", + "file": "Concurrent Systems/notes/13 - CCS cose varie.md", "mode": "source", "source": false }, "icon": "lucide-file", - "title": "13 -" + "title": "13 - CCS cose varie" } } ], @@ -229,9 +229,9 @@ "active": "9d3f25b0eb9b478f", "lastOpenFiles": [ "Concurrent Systems/slides/class 12.pdf", - "Concurrent Systems/notes/13 -.md", - "Pasted image 20250415082906.png", + "Concurrent Systems/notes/13 - CCS cose varie.md", "Concurrent Systems/notes/12 - Calculus of communicating system.md", + "Pasted image 20250415082906.png", "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", "Concurrent Systems/notes/images/Pasted image 20250414164549.png", "Concurrent Systems/notes/images/Pasted image 20250414181443.png", diff --git a/Concurrent Systems/notes/13 -.md b/Concurrent Systems/notes/13 - CCS cose varie.md similarity index 82% rename from Concurrent Systems/notes/13 -.md rename to Concurrent Systems/notes/13 - CCS cose varie.md index c638f11..de7f6f7 100644 --- a/Concurrent Systems/notes/13 -.md +++ b/Concurrent Systems/notes/13 - CCS cose varie.md @@ -13,7 +13,7 @@ This means that the implementation and the specification do coincide. To show th ![](../../Pasted%20image%2020250415082906.png) ## Restrictions -**Proposition:** a.P\a ∼ 0 +**Proposition:** $a.P \textbackslash a ∼ 0$ *Proof:* - S = {(a.P\a , 0)} is a bisimulation @@ -21,6 +21,11 @@ Which challenges can (a.P)\a have? - a.P can only perform a (and become P) - however, because of restriction, a.P\a is stuck - No challenge from a.P\a, nor from 0 à bisimilar! + No challenge from a.P\a, nor from 0 -> bisimilar! -**Proposition:** \ No newline at end of file +**Proposition:** $\bar{a}.P \textbackslash a ∼ 0$ +*Proof is similar.* + +## Idempotency of Sum +**Proposition:** $α.P+α.P+M ∼ α.P+M$ +*Proof:*