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

.obsidian/workspace.json

@@ -238,14 +238,16 @@
       "companion:Toggle completion": false
     }
   },
-  "active": "fbeaa35cc5a8abf1",
+  "active": "364a7591f14f033a",
   "lastOpenFiles": [
-    "Concurrent Systems/slides/class 11.pdf",
     "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
+    "Concurrent Systems/slides/class 11.pdf",
+    "Concurrent Systems/slides/class 12.pdf",
+    "Pasted image 20250414091528.png",
+    "Pasted image 20250414091521.png",
     "Pasted image 20250414084615.png",
     "Pasted image 20250414082824.png",
     "Concurrent Systems/notes/12.md",
-    "Concurrent Systems/slides/class 12.pdf",
     "HCIW/notes/3 - Beacons.md",
     "HCIW/slides/Zooming interfaces.pdf",
     "HCIW/slides/Gestural interaction.pdf",
@@ -268,8 +270,6 @@
     "Concurrent Systems/notes/images/Pasted image 20250405000438.png",
     "Pasted image 20250405000428.png",
     "Concurrent Systems/a.md",
-    "Concurrent Systems/notes/images/Pasted image 20250404235033.png",
-    "Concurrent Systems/notes/images/Pasted image 20250304093223.png",
     "Concurrent Systems/notes/9 - Consensus.md",
     "Concurrent Systems/notes/8 - Enhancing Liveness Properties.md",
     "Concurrent Systems/notes/7- MUTEX-free concurrency.md",

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

@@ -100,3 +100,13 @@ So, (p', q') ∈ ∼
 *Proof:*
 Let (p,q) ∈ S. Then, there exists a bisimulation that contains the pair (p, q); thus, (p, q) ∈ ∼.
 
+![](../../Pasted%20image%2020250414091521.png)
+
+
+![](../../Pasted%20image%2020250414091528.png)
+
+The only ingredients we used to write down an LTS are:
+- sequential compsition (of an action and a process)
+- non-deterministic choice (between a finite set of prefixed processes)
+- recursion
+