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

最新文章

  1. 用MVC做支付宝手机网页支付问题
  2. 在tomcat下部署工程
  3. Codeforces Round #216 (Div. 2) B. Valera and Contest
  4. [C++] memset 和sizeof 的使用注意
  5. CSS hack的写法
  6. JVM-对象
  7. eclipse 恢复被删除的文件
  8. Kubuntu（14.04）共享wifi（热点）
  9. C++红旗之更短形式：500多字符且无法遵守原题规则
  10. Linux 下源码安装JDK
  11. python爬虫如何爬知乎的话题？
  12. Web前端 前端相关书籍推荐
  13. node.js读写文件
  14. linux命令logger使用
  15. IC卡T0协议中的过程字与状态字
  16. Phone List HDU1671
  17. 学习笔记21—PS换图片背景
  18. css特效博客
  19. 前端（慕课网）笔记二：http协议
  20. Springboot2.x 集成redis

热门文章

  1. Docker for windows安装与使用
  2. ES6继承和ES5继承是完全一样的么?
  3. SQL 练习27
  4. SQL 练习26
  5. 在JavaScript中安全访问嵌套对象
  6. 如何在github上传本地项目代码
  7. 【转】springcloud底层原理
  8. springmvc学习日志四
  9. 使用Eclipse搭建SSM框架（Spring + Spring MVC + Mybatis）
  10. Flink的CheckPoint