From 9817d4249d6ce4896816db89f9a7f870a3bb4636 Mon Sep 17 00:00:00 2001
From: Marco Realacci <marco@marcorealacci.me>
Date: Wed, 30 Apr 2025 17:43:22 +0200
Subject: [PATCH] vault backup: 2025-04-30 17:43:22

---
 .../notes/13 - Weak Bisimilarity.md              | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md
index 7a9a7a0..83e71bb 100644
--- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md	
+++ b/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)}$$
\ No newline at end of file