diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 89d64b1..ccfd31e 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -238,10 +238,10 @@ "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", "Pasted image 20250414092202.png", "Concurrent Systems/slides/class 12.pdf", "Pasted image 20250414091528.png", diff --git a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md index 7a08ad2..7dfd5e1 100644 --- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md +++ b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md @@ -118,4 +118,13 @@ Let us denote with P{b1/x1 . . . bn/xn} the process obtained from P by replacing ![](../../Pasted%20image%2020250414092202.png) -The set of non \ No newline at end of file +>[!def] +>The set of non-deterministic processes is given by the following grammar: +$$P::= \sum \alpha_{i}.P_{i} | A(a_{1}\dots a_{n})$$ +where I is a finite set of indices and $\alpha_{i} \in A$ for every $i \in I$. + +**Remark:** we now fuse together in a unique operator sequential composition and nondeterministic choice. +If the index set $I$ is empty, then $\sum_{i\in I} \alpha_{i}.P_{i}$ is the terminated process, that cannot perform any action; this process will be represented with the symbol **0**. + +We shall usually omit tail occurrences of ‘.0’ and, for example, simply write a.b instead of a.b.0 +