vault backup: 2025-04-08 09:37:21

.obsidian/workspace.json

@@ -13,12 +13,12 @@
             "state": {
               "type": "markdown",
               "state": {
-                "file": "Concurrent Systems/notes/11 - non so cosa faremo oggi.md",
+                "file": "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
                 "mode": "source",
                 "source": false
               },
               "icon": "lucide-file",
-              "title": "11 - non so cosa faremo oggi"
+              "title": "11 - LTSs and Bisimulation"
             }
           }
         ]
@@ -192,8 +192,7 @@
       }
     ],
     "direction": "horizontal",
-    "width": 364.5,
-    "collapsed": true
+    "width": 364.5
   },
   "left-ribbon": {
     "hiddenItems": {
@@ -212,7 +211,7 @@
   "active": "40e3ec35e1961dd0",
   "lastOpenFiles": [
     "Concurrent Systems/slides/class 11.pdf",
-    "Concurrent Systems/notes/11 - non so cosa faremo oggi.md",
+    "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
     "Pasted image 20250408092853.png",
     "Pasted image 20250408091924.png",
     "Concurrent Systems/notes/10 - Implementing Consensus.md",

Concurrent Systems/notes/11 - LTSs and Bisimulation.md

@@ -29,7 +29,11 @@ In concurrency theory, we don’t use finite automata but Labeled Transition Sys
 - automata fix one starting state, whereas in an LTS every state can be considered as initial (this corresponds to different possible behaviors of the process)
 - automata rely on final states for describing the language accepted, whereas in LTS this notion is not very informative
 
-Fix a set of action names (or, simply, actions), written N.
 >[!note] LTS formal definition
+>Fix a set of action names (or, simply, actions), written N.
+>
 >A Labeled Transition System (LTS) is a pair (Q, T), where Q is the set of states and T is the transition relation (T ⊆ Q × N × Q).
 
+We shall usually write s –a–> s′ instead of ⟨s,a,s′⟩ ∈ T.
+
+### Bisimulation