diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index eac2cd9..8d3868b 100644 --- a/.obsidian/workspace.json +++ b/.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", diff --git a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md index 41fed35..6ce6c5e 100644 --- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md +++ b/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 + diff --git a/Pasted image 20250414091521.png b/Pasted image 20250414091521.png new file mode 100644 index 0000000..1aece0b Binary files /dev/null and b/Pasted image 20250414091521.png differ diff --git a/Pasted image 20250414091528.png b/Pasted image 20250414091528.png new file mode 100644 index 0000000..f3f0fd5 Binary files /dev/null and b/Pasted image 20250414091528.png differ