vault backup: 2025-04-30 17:43:22

Concurrent Systems/notes/13 - Weak Bisimilarity.md

@@ -122,3 +122,19 @@ Weak bisimilarity $L \approx L_{i}$
 $$R \triangleq \{ (L, L_{i})\space|\space 0<i\leq n\} \space \cup \space \{\bar{p_{i}}.L,L'_{i} \space | \space 0<i<n  \}$$
 is a weak bisimulation, trust me bro.
 
+### EXAMPLE: Scheduler
+We have a set of processes Pi (for 0 < i ≤ n) that must repeatedly perform at certain
+task.
+
+A scheduler has to guarantee that processes cyclically start their task, starting from P1.
+Executions of different processes may overlap but the scheduler has to guarantee that
+every process Pi completes his performance before starting another one (with the
+same index i).
+
+Every process Pi requires to start its task via action $a_i$ and signals to the scheduler its
+termination via action $b_i$
+- the scheduler has to guarantee that the a’s cyclically occur, starting with $a_1$, and, for every i, the ai’s must alternate with the bi’s, starting with $a_i$.
+
+The specification is:
+if $i \in X$ then:
+$$Si,X=a_{i}.S_{(i \space mod \spac)}$$