程序代數(Process Algebra)

Process Algebra 理論

提出者	理論名稱	縮寫	論文連結	簡介
C. A. R. Hoare/Tony Hoare	Communicating Sequencing Process	CSP	Communicating Sequential Processes	1978年C. A．R．Hoare提出的通訊順序程序 CSP，是面向分散式系統的程式設計語言
Robin Milner	Calculus of Communicating Systems	CCS	--	1973至1980年間發明了通訊系統演算CCS，是用於描述通訊併發系統的代數理論
J.A. Bergstra, J.W. Klop	Algebra of Communicating Processes with Abstraction	ACP	[ACP]http://dspace.library.uu.nl/handle/1874/12719)	Bergstra等人1984年提出的 ACP理論針對反應式、並行式和分散式系統,描述了兩個系統之間的互動行為

CSP基礎知識

• 原版教材PDF獲取，點我
  
  注：目前已更新至2015版；
• 中文版可參考周巢塵院士翻譯的《通訊順序程序》。但是年代比較久遠，是90年代的版本了。

第一章

1、對確定性程序，如何判斷兩個程序等價？

答: 確定性程序，需要判斷兩者alphabet（字母表）和traces（跡）是否相等。即：

①\(\alpha P=\alpha Q\)

②\(traces( P) =traces( Q )\)

2、\(traces(\mu X: A \cdot F(x)) = ?\)

答: \(traces(\mu X: A \cdot F(x)) = \{s|\exists n≥0，x \in A，s \le traces(F(x))^{n}\}\)

3、證明：

（下述兩道證明題均是採用數學歸納法證明）

（1）\(traces(RUN_{A}) = A^{*}.\)

（注：\(A^{*}\) means the set of sequences with elements in A）

（2）\(traces(VMS) = \cup_{n≥0} \{s| s≤< coin,choc >^{n},n≥0\}.\)

第二章

1、Let \(\alpha P = \{a,c\},\quad and \quad P = (a → c → P), \quad \alpha Q = \{b,c\}\quad and \quad Q = (c → b → Q).\)

（1）\(P || Q = ?\)

答：

Also

Therefore

（2）Please prove that \(P|| Q \quad sat\quad 0 ≤ tr↓ a-tr↓ b ≤ 2.\)

答:

1.若 \(tr\) 未執行到迴圈階段，則 \(tr ↓ a = 1\) 或 \(0\)， \(tr↓ b = 0\) 滿足不等式；

2.若 \(tr\) 執行到迴圈並恰好完成若干次迴圈，則由於每次迴圈 \(a\) 的個數 \(=\quad b\) 的個數，所以\(tr ↓ a − tr ↓ b = 1\)。

3.若 \(tr\) 執行到某次迴圈中，由於本次迴圈前滿足 \(tr ↓ a - tr ↓ b= 1\)，

所以:

若執行 \(a → b → c → X\)，則 \(tr↓ a − tr ↓ b =2\) 或 \(1\)；

若執行 \(b → a → c → X\)，則 \(tr ↓ a- tr ↓ b=0\) 或 \(1\)；

綜上，\(0 ≤ tr↓ a- tr ↓ b≤ 2\)。

2、If P and Q never stop and if \(\alpha P \cap \alpha Q\) contains at most one element, then\((P || Q)\) never stops.

（1）請直觀解釋此結論的正確性。

答: 因為P和Q的字母表交集最多含有1個元素，所以不會觸發\((c → P)||(d → Q) = STOP \quad if c\ne d\)

（2）當 \(\alpha P \cap \alpha Q\) 含有 2 個或更多元素時，此結論不成立，舉例說明。

如\(\alpha P = \alpha Q = \{a, b\},\)

\(P = a \rightarrow b \rightarrow P;\)

\(Q = b \rightarrow a \rightarrow Q;\)

\(P || Q = STOP.\)

第三章

1、

（1）\(traces(P\sqcap Q) = ?\)

答: \(traces(P\sqcap Q)=traces(P) ∪ traces(Q)\)

（2）\(traces(P \square Q) = ?\)

答: \(traces(P \square Q)= traces(P)∪ traces(Q)\)

（3）\(refusals(P \sqcap Q) = ?\)

答: \(refusals(P\sqcap Q) = refusals(P) ∪ refusals(Q)\)

（4）\(refusals(P\square Q) = ?\)

答: \(refusals(P\square Q)=refusals(P) ∩ refusals(Q)\)

（5）令\(\alpha P = \alpha Q = \alpha P_{1} = \alpha Q_{1}= \{a,b,c\},\)

\(P_{1} = (a → b → STOP)\)

\(P_{2}= (b → c → STOP)\)

\(P = P_{1} \sqcap P_{2}\)

\(Q = P_{1}\square P_{2}\)

問：

①\(refusals(P) = ?\)

②\(refusals(Q) = ?\)

答：

\(refusals(P_{1}) = \{\{\},{b},{c},{b,c}\}\)

\(refusals(P_{2}) =\{\{\},{a},{c},{a,c}\}\)

\(refusals(P) = \{\{\},{a},{b},{c},{b,c},{a,c}\}\)

\(refusals(Q) =\{\{\},{c}\}\)

（6）\(refusals(P|| Q) = ?\)

答: \(refusals(P||Q)=\{X ∪ Y | X \in refusals(P) \wedge Y \in refusals(Q)\}\)

（7）\(refusals(P|||Q) = ?\)

答:\(refusals(P|||Q) =refusals(P\square Q) =refusals(P) \cap refusals(Q)\)

2.

（1）\(divergences(Chaos) = ?\)

答: \(divergences(Chaos) = A^*\)

（2）\(divergences(X: B → P(X)) = ?\)

答: \(\{⟨x⟩\smallfrown s | x \in B \wedge s \in divergences(P(x))\}\)

（3）\(divergences(P \sqcap Q) = ?\)

答: \(divergences(P) ∪ divergences(Q)\)

（4）\(divergences(P\square Q) = ?\)

答: \(divergences(P) ∪ divergences(Q)\)

（5）\(divergences(P∥Q) = ?\)

答: \(\{s \smallfrown t|t \in (\alpha P ∪ \alpha Q) ^{*} \wedge
((s \upharpoonright\alpha P \in divergences( P )\wedge s \upharpoonright \alpha Q \in traces(Q)) ∨
(s \upharpoonright \alpha P \in traces(P) \wedge s\upharpoonright \alpha Q \in divergences(Q))\}\)

（6）\(divergences(P|||Q) = ?\)

答: \(\{u | \exists s, t • u \quad interleaves (s, t) \wedge ((s \in divergences(P) \wedge t \in traces(Q)) ∨ (s \in traces(P) \wedge t \in divergences(Q)))\}\)

3.

（1）\(failures(P) = ?\)

答: \(failures(P) =\{(s, X)| s \in traces(P) \wedge X \in refusals(P/s)\}\)

（2）P 與 Q 的定義如上述第三章的 1、（3）所定義：

問：\(failures(P) = ?\) \(failures(Q) = ?\)

（3）

①\(failures(P \sqcap Q) = ?\)

答: \(failures(P \sqcap Q) =failures(P)\cup failures(Q)\)

②\(failures(X: B → P(X)) = ?\)

答: \(\{(<>, X)| X \subseteq (\alpha P − B)\} ∪ \{(⟨x⟩ \smallfrown s, X)| x \in B \wedge (s, X) \in failures(P(x))\}\)

③\(failures(P ∥ Q) = ?\)

答: \(failures(P||Q) = \{(s, X \cup Y )|s \in (\alpha P ∪ \alpha Q) ^{*} \wedge (s \upharpoonright \alpha P, X) \in failures(P) \wedge (s\upharpoonright \alpha Q, Y ) \in failures(Q)\} \cup \{(s, X)|s \in divergences(P||Q)\}\)

④\(failures(P \square Q) = ?\)

答: \(\{(s, X)|(s, X) \in failures(P) ∩ failures(Q)) \vee (s \ne <>\wedge (s, X) \in failures(P) \cup failures(Q))\} \cup \{(s, X)| s \in divergences(P \square Q)\}\)

⑤\(failures(P|||Q) = ?\)

答: \(\{(s, X)| ∃t, u• (t, X) \in failures(P) \wedge (u, X) \in failures(Q) \} ∪ \{(s, X)| s \in divergences(P|||Q)\}\)

4.對非確定性程序，如何判斷兩個程序等價？

答:對非確定性程序而言，使用traces已經無法區分（如，第三章的 1、（3）所定義的兩程序\(P\)和\(Q\)：\(\alpha P=\alpha Q\),且\(traces(P)=traces(Q )\)）；進一步引入\(refusals\)，但是用\(refusals\)來判斷，具有侷限性。最終，通過\(alphabet\)、\(divergences\)和\(failures\)綜合判斷。

即：

①\(\alpha P=\alpha Q\)

②\(divergences(P)=divergences(Q)\)

③\(failures(P)=failures(Q)\)

CSP： Operational Semantics

1、如何從 CSP 通訊的操作語義角度理解 CSP 併發定義中要求公共事件須同步？

答：

A和B之間存在通訊的管道，可以傳送某種型別的訊息，B在接收到A的訊息之前，並不清楚A傳送的內容，只知道型別；

只有在A傳送的同時，B同步接收，雙方才可以通訊，因此公共事件須同步。

2、從 CSP 的操作語義的角度定義：

（1）\(failures(P) = ?\)

答: \(failures(P) ={}_{df}\{s,X|\exists P_{1},P_{2}\cdot P\stackrel{s}{ \implies}P1\wedge P_{1}\xrightarrow {*}P_2\wedge stable(P_2)\wedge \forall c\in X\cdot \lnot (P_2\rightarrow)\}\)

（2）\(divergences(P) = ?\)

答: \(divergences(P) = {}_{df}\{s|\exists P_{1}\cdot P\stackrel{s}{ \implies}{s} P_{1}\wedge \uparrow P_{1}\}\)

CCS： Bisimulation

1.CCS 中 Strong Bisimulation 是如何定義的？

A binary relation \(S \subseteq P × P\) over agents is a strong bisimulation if \((P, Q) \in S\) implies, for all \(\alpha \in Act\),

(1) Whenever \(P \xrightarrow {\alpha }P'\) then, for some \(Q'\) , \(Q\xrightarrow {\alpha}Q'\) and \((P' ,Q' ) \in S\)

(2) Whenever \(Q \xrightarrow {\alpha } Q'\) then, for some \(P'\) , \(P \xrightarrow {\alpha }P'\) and \((P', Q') \in S\)

Denoted by \(P \sim Q\).

2.CCS 中 Weak Bisimulation 是如何定義的？

A binary relation \(S \subseteq P × P\) over agents is a weak bisimulation if \((P, Q) \in S\) implies, for all \(\alpha \in Act\),

(1) Whenever \(P \xrightarrow {\alpha } P'\) then, for some \(Q'\) , \(Q \stackrel{ \hat\alpha }{ \implies}Q'\) and \((P' ,Q' ) \in S\)

(2) Whenever \(Q \xrightarrow {\alpha } Q'\) then, for some \(P'\) , \(P \stackrel{ \hat\alpha }{ \implies} P'\) and \((P', Q') \in S\)

Denoted by \(P \approx Q\).