From aeca70e82deeec90e53d354d216361a7c1ad9ddb Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 5 May 2025 09:02:04 +0200 Subject: [PATCH] vault backup: 2025-05-05 09:02:04 --- .obsidian/workspace.json | 3 +-- Concurrent Systems/notes/15 - A formal language for LTSs.md | 3 +++ 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index b4e3dae..8169318 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -213,9 +213,9 @@ }, "active": "cdcc59f1bf6d4ae1", "lastOpenFiles": [ - "Pasted image 20250505085454.png", "Concurrent Systems/slides/class 15.pdf", "Concurrent Systems/notes/15 - A formal language for LTSs.md", + "Pasted image 20250505085454.png", "Pasted image 20250505084741.png", "Pasted image 20250505084556.png", "Pasted image 20250505083948.png", @@ -236,7 +236,6 @@ "Concurrent Systems/slides/class 13.pdf", "Concurrent Systems/notes/images/Pasted image 20250415082906.png", "Concurrent Systems/slides/class 14.pdf", - "Concurrent Systems/notes/images/Pasted image 20250429092543.png", "Concurrent Systems/slides/class 12.pdf", "HCIW/slides/HCI in the car.pdf", "Concurrent Systems/slides/class 11.pdf", diff --git a/Concurrent Systems/notes/15 - A formal language for LTSs.md b/Concurrent Systems/notes/15 - A formal language for LTSs.md index 0056d32..047c942 100644 --- a/Concurrent Systems/notes/15 - A formal language for LTSs.md +++ b/Concurrent Systems/notes/15 - A formal language for LTSs.md @@ -32,3 +32,6 @@ However, this can never happen, whatever P’ be; hence, P |= ☐aFF holds true only if P cannot perform any action a ![](../../Pasted%20image%2020250505085454.png) + +Let us now define the set of formulae satisfied by a process as $$L(P) = \{ \phi \in Form:P \models \phi \}$$ +To simplify the proof, let us modify the set of formulae \ No newline at end of file