diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 8634176..d8b6a8a 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -192,7 +192,8 @@ } ], "direction": "horizontal", - "width": 364.5 + "width": 364.5, + "collapsed": true }, "left-ribbon": { "hiddenItems": { @@ -212,6 +213,7 @@ "lastOpenFiles": [ "Concurrent Systems/slides/class 11.pdf", "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", + "Pasted image 20250408093840.png", "Pasted image 20250408092853.png", "Pasted image 20250408091924.png", "Concurrent Systems/notes/10 - Implementing Consensus.md", @@ -254,7 +256,6 @@ "Concurrent Systems/slides/class 6.pdf", "Concurrent Systems/notes/images/Pasted image 20250325090735.png", "Concurrent Systems/slides/class 8.pdf", - "Concurrent Systems/notes/images/Pasted image 20250324091452.png", "Senza nome.canvas" ] } \ No newline at end of file diff --git a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md index e818512..5f78c9d 100644 --- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md +++ b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md @@ -37,3 +37,7 @@ In concurrency theory, we don’t use finite automata but Labeled Transition Sys We shall usually write s –a–> s′ instead of ⟨s,a,s′⟩ ∈ T. ### Bisimulation +Intuitively, two states are equivalent if they can perform the same actions that lead them in states where this property still holds +![](../../Pasted%20image%2020250408093840.png) +P0 and Q0 are different because, after an a, the former can decide to do b or c, whereas the latter must decide this before performing a. + diff --git a/Pasted image 20250408093840.png b/Pasted image 20250408093840.png new file mode 100644 index 0000000..e108569 Binary files /dev/null and b/Pasted image 20250408093840.png differ