进程代数(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 = ?\)

答：

\[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\).