diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index e4a5aea..bf23ca8 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -213,6 +213,9 @@ }, "active": "ec8d1a91f1f0cc7e", "lastOpenFiles": [ + "Pasted image 20250429092305.png", + "Pasted image 20250429092055.png", + "Pasted image 20250429091959.png", "Concurrent Systems/slides/class 14.pdf", "Concurrent Systems/notes/14.md", "Pasted image 20250429091029.png", @@ -223,8 +226,6 @@ "Pasted image 20250429083535.png", "Pasted image 20250429083455.png", "Pasted image 20250429083129.png", - "Pasted image 20250429082905.png", - "Pasted image 20250429082812.png", "Concurrent Systems/notes/13 - Weak Bisimilarity.md", "Concurrent Systems/slides/class 13.pdf", "Concurrent Systems/notes/12 - Calculus of communicating system.md", diff --git a/Concurrent Systems/notes/14.md b/Concurrent Systems/notes/14.md index 95c203d..6ca3f48 100644 --- a/Concurrent Systems/notes/14.md +++ b/Concurrent Systems/notes/14.md @@ -53,4 +53,11 @@ exercise: prove the weak bisimilarity Let us consider the parallel of processes M and R, by using the axiom for parallel, we have $$\vdash M|R=put.(\overline{go}|R)+go.(M|\overline{rcv})$$ By using the same axiom to the parallel of the three processes, we obtain -$$\vdash S|(M|R)=send.(\overline{put}|(M|R))+put.(\overline{go})$$ \ No newline at end of file +$$\vdash S|(M|R)=send.(\overline{put}|(M|R))+put.(\overline{go}|R|S)+go.(\overline{rcv}|S|M)$$ +By restricting *put* and *go*, and by using the second axiom for restriction, we have that: +![](../../Pasted%20image%2020250429091959.png) + +We now apply the third axiom for restriction to the three summands: +![](../../Pasted%20image%2020250429092055.png) +![](../../Pasted%20image%2020250429092305.png) + diff --git a/Pasted image 20250429091959.png b/Pasted image 20250429091959.png new file mode 100644 index 0000000..1fd6c91 Binary files /dev/null and b/Pasted image 20250429091959.png differ diff --git a/Pasted image 20250429092055.png b/Pasted image 20250429092055.png new file mode 100644 index 0000000..ebdb70e Binary files /dev/null and b/Pasted image 20250429092055.png differ diff --git a/Pasted image 20250429092305.png b/Pasted image 20250429092305.png new file mode 100644 index 0000000..fa18e82 Binary files /dev/null and b/Pasted image 20250429092305.png differ