diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 746087d..993556f 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -14,12 +14,12 @@ "state": { "type": "markdown", "state": { - "file": "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", + "file": "Concurrent Systems/notes/12 - bastaaaaaaaa.md", "mode": "source", "source": false }, "icon": "lucide-file", - "title": "11 - LTSs and Bisimulation" + "title": "12 - bastaaaaaaaa" } }, { @@ -67,8 +67,7 @@ "title": "class 11" } } - ], - "currentTab": 1 + ] } ], "direction": "vertical" @@ -125,8 +124,7 @@ } ], "direction": "horizontal", - "width": 309.5, - "collapsed": true + "width": 309.5 }, "right": { "id": "bc4b945ded1926e3", @@ -240,23 +238,23 @@ }, "active": "fbeaa35cc5a8abf1", "lastOpenFiles": [ - "Concurrent Systems/slides/class 11.pdf", - "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", "Concurrent Systems/slides/class 12.pdf", "Concurrent Systems/notes/12 - bastaaaaaaaa.md", - "Pasted image 20250414104010.png", - "Pasted image 20250414103800.png", - "Pasted image 20250414102733.png", - "Pasted image 20250414093017.png", - "Pasted image 20250414092202.png", - "Pasted image 20250414091528.png", - "Pasted image 20250414091521.png", - "Pasted image 20250414084615.png", - "Pasted image 20250414082824.png", + "Concurrent Systems/notes/images/Pasted image 20250414082824.png", + "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", + "Concurrent Systems/notes/images/Pasted image 20250414152300.png", + "Concurrent Systems/notes/images/Pasted image 20250414152247.png", + "Concurrent Systems/notes/images/Pasted image 20250414152234.png", + "Concurrent Systems/notes/images/Pasted image 20250414152221.png", + "Concurrent Systems/slides/class 11.pdf", + "Concurrent Systems/notes/images/Pasted image 20250414104010.png", + "Concurrent Systems/notes/images/Pasted image 20250414103800.png", + "Concurrent Systems/notes/images/Pasted image 20250414102733.png", + "Concurrent Systems/notes/images/Pasted image 20250414093017.png", + "Concurrent Systems/notes/images/Pasted image 20250414092202.png", "HCIW/notes/3 - Beacons.md", "HCIW/slides/Zooming interfaces.pdf", "HCIW/slides/Gestural interaction.pdf", - "Concurrent Systems/notes/images/Pasted image 20250408091924.png", "Concurrent Systems/notes/10 - Implementing Consensus.md", "Concurrent Systems/notes/2 - Fast mutex by Lamport.md", "Concurrent Systems/notes/4 - Semaphores.md", diff --git a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md index a4364c4..cfe5342 100644 --- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md +++ b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md @@ -56,14 +56,14 @@ To let p0 be simulated by q0, we should have that p1 is simulated by q1 or q2. If S contained one among (p1,q1) or (p1,q2), then it would not be a simulation: indeed, p1 can perform both a c (whereas q1 cannot) and a b (whereas q2 cannot). **Remark:** for proving equivalence, it is NOT enough to find a simulation of p by q and a simulation of q by p -![](../../Pasted%20image%2020250414082824.png) +![](images/Pasted%20image%2020250414082824.png) p0 is simulated by q0: $$S = {(p0, q0), (p1, q2), (p2, q3)}$$ q0 is simulated by p0: $$S′ ={(q0,p0),(q1,p1),(q2,p1),(q3,p2)}$$ However, p0 and q0 are not bisimilar: the transition q0 -> a -> q1 is not bisimulable by any transition from p0 (ndeed, p0 –a–> p1 does not suffice, because p1 can perform a b and so cannot be bisimilar to q1). #### Bisimulation is NOT isomorfism -![](../../Pasted%20image%2020250414084615.png) +![](images/Pasted%20image%2020250414084615.png) $S = \{(p0,q0), (p1,q1), (p2,q1), (p0,q2)\}$ $S^{−1} = \{(q0,p0), (q1,p1), (q1,p2), (q2,p0)\}$ @@ -101,10 +101,10 @@ So, (p', q') ∈ ∼ Let (p,q) ∈ S. Then, there exists a bisimulation that contains the pair (p, q); thus, (p, q) ∈ ∼. ## A syntax for LTSs -![](../../Pasted%20image%2020250414091521.png) +![](images/Pasted%20image%2020250414091521.png) -![](../../Pasted%20image%2020250414091528.png) +![](images/Pasted%20image%2020250414091528.png) The only ingredients we used to write down an LTS are: - sequential composition (of an action and a process) @@ -117,7 +117,7 @@ For every identifier (denoted with capital letters A,B,..), we shall assume a un Let us denote with P{b1/x1 . . . bn/xn} the process obtained from P by replacing name xi with name bi, for every i = 1,..., n. -![](../../Pasted%20image%2020250414092202.png) +![](images/Pasted%20image%2020250414092202.png) >[!def] >The set of non-deterministic processes is given by the following grammar: @@ -133,7 +133,9 @@ We shall usually omit tail occurrences of ‘.0’ and, for example, simply writ From the syntax to the LTS We have shown how it is possible, starting from an LTS, to generate a corresponding process It is also possible the inverse translation and then the two formalisms do coincide; the rules that have to be used in this translation are: -![](../../Pasted%20image%2020250414093017.png) - - -examples \ No newline at end of file +![](images/Pasted%20image%2020250414093017.png) +#### Examples +![](images/Pasted%20image%2020250414152221.png) +![](images/Pasted%20image%2020250414152234.png) +![](images/Pasted%20image%2020250414152247.png) +![](images/Pasted%20image%2020250414152300.png) diff --git a/Concurrent Systems/notes/12 - bastaaaaaaaa.md b/Concurrent Systems/notes/12 - bastaaaaaaaa.md index b9ddced..dce84dc 100644 --- a/Concurrent Systems/notes/12 - bastaaaaaaaa.md +++ b/Concurrent Systems/notes/12 - bastaaaaaaaa.md @@ -15,7 +15,7 @@ Given a set of names N (that denote events) When two processes synchronize, an external observer has no way of understanding what is happening in the system - synchronization is not observable from the outside; it produces a special ‘silent’ action, that we denote with τ -The set of actions we shall consider is: ![150](../../Pasted%20image%2020250414102733.png) +The set of actions we shall consider is: ![150](images/Pasted%20image%2020250414102733.png) It is also useful to force some processes of the system to synchronize between them (without the possibility of showing to the outside some actions) @@ -23,8 +23,8 @@ The restriction operator P\a restricts the scope of name a to process P (a is vi This is similar to local variables in a procedure of an imperative program -![](../../Pasted%20image%2020250414103800.png) +![](images/Pasted%20image%2020250414103800.png) -![](../../Pasted%20image%2020250414104010.png) +![](images/Pasted%20image%2020250414104010.png) fino alla 7 compresa... \ No newline at end of file diff --git a/Pasted image 20250414082824.png b/Concurrent Systems/notes/images/Pasted image 20250414082824.png similarity index 100% rename from Pasted image 20250414082824.png rename to Concurrent Systems/notes/images/Pasted image 20250414082824.png diff --git a/Pasted image 20250414084615.png b/Concurrent Systems/notes/images/Pasted image 20250414084615.png similarity index 100% rename from Pasted image 20250414084615.png rename to Concurrent Systems/notes/images/Pasted image 20250414084615.png diff --git a/Pasted image 20250414091521.png b/Concurrent Systems/notes/images/Pasted image 20250414091521.png similarity index 100% rename from Pasted image 20250414091521.png rename to Concurrent Systems/notes/images/Pasted image 20250414091521.png diff --git a/Pasted image 20250414091528.png b/Concurrent Systems/notes/images/Pasted image 20250414091528.png similarity index 100% rename from Pasted image 20250414091528.png rename to Concurrent Systems/notes/images/Pasted image 20250414091528.png diff --git a/Pasted image 20250414092202.png b/Concurrent Systems/notes/images/Pasted image 20250414092202.png similarity index 100% rename from Pasted image 20250414092202.png rename to Concurrent Systems/notes/images/Pasted image 20250414092202.png diff --git a/Pasted image 20250414093017.png b/Concurrent Systems/notes/images/Pasted image 20250414093017.png similarity index 100% rename from Pasted image 20250414093017.png rename to Concurrent Systems/notes/images/Pasted image 20250414093017.png diff --git a/Pasted image 20250414102733.png b/Concurrent Systems/notes/images/Pasted image 20250414102733.png similarity index 100% rename from Pasted image 20250414102733.png rename to Concurrent Systems/notes/images/Pasted image 20250414102733.png diff --git a/Pasted image 20250414103800.png b/Concurrent Systems/notes/images/Pasted image 20250414103800.png similarity index 100% rename from Pasted image 20250414103800.png rename to Concurrent Systems/notes/images/Pasted image 20250414103800.png diff --git a/Pasted image 20250414104010.png b/Concurrent Systems/notes/images/Pasted image 20250414104010.png similarity index 100% rename from Pasted image 20250414104010.png rename to Concurrent Systems/notes/images/Pasted image 20250414104010.png diff --git a/Concurrent Systems/notes/images/Pasted image 20250414152221.png b/Concurrent Systems/notes/images/Pasted image 20250414152221.png new file mode 100644 index 0000000..d0880b5 Binary files /dev/null and b/Concurrent Systems/notes/images/Pasted image 20250414152221.png differ diff --git a/Concurrent Systems/notes/images/Pasted image 20250414152234.png b/Concurrent Systems/notes/images/Pasted image 20250414152234.png new file mode 100644 index 0000000..e1057b0 Binary files /dev/null and b/Concurrent Systems/notes/images/Pasted image 20250414152234.png differ diff --git a/Concurrent Systems/notes/images/Pasted image 20250414152247.png b/Concurrent Systems/notes/images/Pasted image 20250414152247.png new file mode 100644 index 0000000..b0430fd Binary files /dev/null and b/Concurrent Systems/notes/images/Pasted image 20250414152247.png differ diff --git a/Concurrent Systems/notes/images/Pasted image 20250414152300.png b/Concurrent Systems/notes/images/Pasted image 20250414152300.png new file mode 100644 index 0000000..621d6bd Binary files /dev/null and b/Concurrent Systems/notes/images/Pasted image 20250414152300.png differ