diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index 240b2ce..f6f0a23 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -6,19 +6,39 @@
       {
         "id": "ceb8ca67f2b32f40",
         "type": "tabs",
+        "dimension": 47.20630372492837,
+        "children": [
+          {
+            "id": "cdcc59f1bf6d4ae1",
+            "type": "leaf",
+            "state": {
+              "type": "markdown",
+              "state": {
+                "file": "Concurrent Systems/notes/15 - A formal language for LTSs.md",
+                "mode": "source",
+                "source": false
+              },
+              "icon": "lucide-file",
+              "title": "15 - A formal language for LTSs"
+            }
+          }
+        ]
+      },
+      {
+        "id": "62c727a144393fdc",
+        "type": "tabs",
+        "dimension": 52.79369627507163,
         "children": [
           {
             "id": "ec8d1a91f1f0cc7e",
             "type": "leaf",
             "state": {
-              "type": "markdown",
+              "type": "pdf",
               "state": {
-                "file": "Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md",
-                "mode": "source",
-                "source": false
+                "file": "Concurrent Systems/slides/class 15.pdf"
               },
-              "icon": "lucide-file",
-              "title": "14 Checking bisimilarity, an inference system"
+              "icon": "lucide-file-text",
+              "title": "class 15"
             }
           }
         ]
@@ -78,7 +98,8 @@
       }
     ],
     "direction": "horizontal",
-    "width": 309.5
+    "width": 309.5,
+    "collapsed": true
   },
   "right": {
     "id": "bc4b945ded1926e3",
@@ -190,8 +211,12 @@
       "companion:Toggle completion": false
     }
   },
-  "active": "ec8d1a91f1f0cc7e",
+  "active": "cdcc59f1bf6d4ae1",
   "lastOpenFiles": [
+    "Concurrent Systems/slides/class 15.pdf",
+    "Concurrent Systems/notes/15 - A formal language for LTSs.md",
+    "Pasted image 20250505083500.png",
+    "Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md",
     "Concurrent Systems/notes/12b - CCS cose varie.md",
     "Concurrent Systems/notes/12 - Calculus of communicating system.md",
     "Concurrent Systems/notes/10 - Implementing Consensus.md",
@@ -200,7 +225,6 @@
     "Concurrent Systems/notes/8 - Enhancing Liveness Properties.md",
     "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
     "Concurrent Systems/notes/13 - Weak Bisimilarity.md",
-    "Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md",
     "Pasted image 20250430192526.png",
     "Pasted image 20250430183304.png",
     "Pasted image 20250430175412.png",
@@ -212,7 +236,6 @@
     "Concurrent Systems/notes/images/Pasted image 20250429092305.png",
     "Concurrent Systems/notes/images/Pasted image 20250429092055.png",
     "Concurrent Systems/notes/images/Pasted image 20250429091959.png",
-    "Concurrent Systems/notes/images/Pasted image 20250429091029.png",
     "Concurrent Systems/slides/class 12.pdf",
     "HCIW/slides/HCI in the car.pdf",
     "Concurrent Systems/slides/class 11.pdf",
@@ -234,9 +257,7 @@
     "Concurrent Systems/notes/6 - Atomicity.md",
     "Concurrent Systems/notes/3a - Hardware primitives & Lamport Bakery algorithm.md",
     "Concurrent Systems/notes/1 - CS Basics.md",
-    "Concurrent Systems/notes/6a - Alternatives to Atomicity.md",
     "HCIW/slides/1 Interface and Interaction for IoT.pdf",
-    "Concurrent Systems/slides/class 4.pdf",
     "Senza nome.canvas"
   ]
 }
\ No newline at end of file
diff --git a/Concurrent Systems/notes/15 - A formal language for LTSs.md b/Concurrent Systems/notes/15 - A formal language for LTSs.md
new file mode 100644
index 0000000..b9692fd
--- /dev/null
+++ b/Concurrent Systems/notes/15 - A formal language for LTSs.md	
@@ -0,0 +1,13 @@
+(In)equivalences between systems hold because of different properties of the systems themselves.
+Logics = a formal way to express these properties.
+- satisfiability relation states when a process satisfies a property
+- enjoying the same properties coincides with being bisimilar
+
+#### Example
+![300](../../Pasted%20image%2020250505083500.png)
+These processes are not bisimilar as:
+- P1 can perform an action a followed by any b
+- P2, after every a, can always perform an action b
+- so there exists an a after which P1 cannot perform a b. But not for P2
+
+### Syntax and Satisfiability
diff --git a/Concurrent Systems/slides/class 15.pdf b/Concurrent Systems/slides/class 15.pdf
new file mode 100644
index 0000000..8b9b335
Binary files /dev/null and b/Concurrent Systems/slides/class 15.pdf differ
diff --git a/Pasted image 20250505083500.png b/Pasted image 20250505083500.png
new file mode 100644
index 0000000..45f7154
Binary files /dev/null and b/Pasted image 20250505083500.png differ