vault backup: 2025-05-05 09:49:15

.obsidian/workspace.json

@@ -213,6 +213,7 @@
   },
   "active": "cdcc59f1bf6d4ae1",
   "lastOpenFiles": [
+    "Pasted image 20250505094841.png",
     "Concurrent Systems/slides/class 15.pdf",
     "Concurrent Systems/notes/15 - A formal language for LTSs.md",
     "Pasted image 20250505090959.png",

Concurrent Systems/notes/15 - A formal language for LTSs.md

@@ -56,4 +56,18 @@ Hence, $\forall \phi'' \in L(P'), \space \phi'' \in L(Q'), \space i.e. \space L(
 
 By contradiction, let us assume that the inclusion is a proper, i.e. $L(P') \subset L(Q')$. Thus, $\exists \hat{\phi}:\hat{\phi}\in L(Q') \land \hat{\phi} \not \in L(P')$.
 
-Then, $\lnot \hat{\phi} \in L(P')$ and this would imply that $\lnot \hat{\phi} \in L(Q')$. This is a contradiction because $L(Q')$ cannot contain a formula and its negation.
+Then, $\lnot \hat{\phi} \in L(P')$ and this would imply that $\lnot \hat{\phi} \in L(Q')$. This is a contradiction because $L(Q')$ cannot contain a formula and its negation.
+
+### Proving unequivalences
+The Logic approach presented so far is very natural for proving unequivalences:
+- show one formula that is satisfied by a proc but not by the other
+
+It is not very effective for concretely proving equivalences:
+- e.g. to show that $P \sim Q$, we should check that every formula in L(P) belongs to L(Q) and conversely
+- the problem is that L(P) is infinite, for every P, it contains TT, TT^TT, TT^TT^TT, ...
+- even if we restrict to logical equivalence class, the situation does not change
+- EXAMPLE: consider process P2 ![50](../../Pasted%20image%2020250505094841.png)
+	- it satisfies ☐bFF, ☐cFF, ☐dFF, ...
+	- so L(P2) is infinite because so is the action set
+
+#### Sub-Logics