From 85b15706902b20e17f8bc3ca4a76136abb84fbfd Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 14 Apr 2025 12:24:54 +0200 Subject: [PATCH] vault backup: 2025-04-14 12:24:54 --- Concurrent Systems/notes/11 - LTSs and Bisimulation.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md index 1df2007..a4364c4 100644 --- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md +++ b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md @@ -99,7 +99,7 @@ So, (p', q') ∈ ∼ **Theorem:** For every bisimulation S, it holds that S ⊆ ∼. *Proof:* Let (p,q) ∈ S. Then, there exists a bisimulation that contains the pair (p, q); thus, (p, q) ∈ ∼. -## La parte difficile +## A syntax for LTSs ![](../../Pasted%20image%2020250414091521.png) @@ -107,7 +107,7 @@ Let (p,q) ∈ S. Then, there exists a bisimulation that contains the pair (p, q) ![](../../Pasted%20image%2020250414091528.png) The only ingredients we used to write down an LTS are: -- sequential compsition (of an action and a process) +- sequential composition (of an action and a process) - non-deterministic choice (between a finite set of prefixed processes) - recursion