行程代數(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 | 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 = ?\)
答：
\[P||Q \]\[= (a → c → P)||(c → b → Q) \tag{by definition} \]\[= a → ((c → P)||(c → b → Q)) \tag{by L5A} \]\[= a → c → (P||(b → Q)) \]Also
\[P||(b → Q) \]\[= (a → (c → P)||(b → Q) \]\[|b → (P||Q)) [by L6] \]\[= (a → b → ((c → P)||Q) |b → (P||Q)) \tag{ by L5B} \]\[= (a → b → c → (P||(b → Q)) |b → a → c → (P||(b → Q))) \tag{by ?above} \]\[= μX ? (a → b → c → X|b → a → c → X) \]Therefore
\[(P||Q) = (a → c → μX(a → b → c → X|b → a → c → X)) \tag{by ?above} \]（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\).
轉載請註明出處，本文鏈接：https://www.uj5u.com/gongcheng/308423.html
標籤：其他