【进程代数学习笔记】3：[CSP]进程与不确定性

前面一二章所学习的进程分裂或协作的方式有：选择（P∣QP|QP∣Q）：用于和环境交互，由环境（CSP里亦用进程表示）选择当前动作以决定进程接下来的分支。并发（P∣∣QP||QP∣∣Q）：用于进程间的协作，或用于为进程施加影响它的环境进程。如上面所述的，一条竖线表达的选择即是确定性（deterministic）选择，确定性选择是环境能把控的。与之相对地可以引入不确定性（nondeterm...

LauZyHou

1074人浏览 · 2019-10-18 23:57:26

LauZyHou · 2019-10-18 23:57:26 发布

前面一二章所学习的进程分裂或协作的方式有：

选择（ $P ∣ Q$ ）：用于和环境交互，由环境（CSP里亦用进程表示）选择当前动作以决定进程接下来的分支。
并发（ $P ∣ ∣ Q$ ）：用于进程间的协作，或用于为进程施加影响它的环境进程。

如上面所述的，一条竖线表达的选择即是确定性（deterministic）选择，确定性选择是环境能把控的。

与之相对地可以引入不确定性（nondeterministic）。不确定性指不仅无法控制，甚至无法被预测，这可以基于以下的考虑：

对环境无法充分了解（如天气的不确定）
刻意忽视决定选择的条件（如换零机coin的存储顺序决定出币序列）
量子力学中的不确定性（uncertainty principle）

总之，引入不确定性可以提高对物理系统的抽象程度。

1 不确定的或关系(Nondeterministic or)

1.1 简述

记 $\sqcap Q$ 是进程 $P$ 和进程 $Q$ 之间的不确定选择，这表示在 $P$ 和 $Q$ 中只选择其一，但遇到 $⊓\sqcap$ 符号时总是无法预测选择的是哪一个。

不确定的或关系 $\sqcap Q$ 实际使用场景很有限，一般用于表示在需求上只要实现 $P$ 或 $Q$ 其一即可。

1.2 例子

例如，由
$\to out2p \to out1p \to CH5A) \\ CH5B=(in3p \to out1p \to out2p \to CH5B)$
构造的
$\sqcap CH5B$
表示 $C H 5 E$ 是从 $C H 5 A$ 和 $C H 5 B$ 中选择其一实现，使用时出币的序列组合不变，只是使用前并不知道实现的是哪一个。

而
$\begin{aligned} CH5D =& (in3p \to ((out2p \to out1p \to CH5D) \\ & \sqcap (out1p \to out2p \to CH5D))) \end{aligned}$
则表示 $C H 5 D$ 每次出币的序列都是无法预测的，每次都会不确定地选择两种出币序列中的其一。

1.3 规则

相关规则见课本P83~84。其中值得注意的是，不确定选择不能在递归操作内部展开：
$\begin{aligned} P &= \mu \cdot X ((a \to X) \sqcap (b \to X)) \\ Q &= (\mu X \cdot (a \to X)) \sqcap (\mu X \cdot (b \to X)) \end{aligned}$
两进程不同，因为它们的traces不同，显然 $\subseteq traces(P)$ ，仅当 $a = b$ 时取到等号。

注意，不确定选择没有"单位元"（因为 $⊓\sqcap$ 是幂等的），不确定选择唯一的"零"是 $C H A O S$ （ $C H A O S$ 同时也是很多算子的"零"），这在7中给出。

2 通用选择(General choice)

2.1 简述

通用选择（ $\Box Q$ ）结合了确定性选择（ $P ∣ Q$ ）和不确定选择（ $P⊓QP\sqcap Q$ ）。具体是，当第一个动作相同时它是确定选择，当第一个动作不同时它是不确定选择：
$\begin{aligned} (c \to P) \Box (d \to Q) &= (c \to P \ | \ d \to Q) & if \ c \neq d \\ (c \to P) \Box (c \to Q) &= (c \to P) \sqcap (c \to Q) = c \to (P \sqcap Q) \end{aligned}$

2.2 规则

因为 $S T O P$ 中没有开始动作，认为 $S T O P$ 是通用选择的单位元：
$\Box STOP = P$
通用选择的一般描述，应对所选的首个动作分情形讨论：
$\begin{aligned} (x:A \to P(x)) \Box & (y:B \to Q(y)) = \\ & (z:(A \cup B) \to \\ &(if \ z \in (A-B) \ then \ P(z) \\ & else \ if \ z \in (B-A) \ then \ Q(z) \\ & else \ if \ z \in (A \cap B) \ then \ (P(z) \cap Q(z)) \\ & )) \end{aligned}$
通用选择的after操作，应对所经过的trace分情形讨论：
$\begin{aligned} (P \Box Q)/s &= P/s & if \ s \in traces(P) - traces(Q) \\ & = Q/s & if \ s \in traces(Q) - traces(P) \\ &= (P/s) \sqcap(Q/s) & if \ s \in traces(P) \cap traces(Q) \end{aligned}$

3 Refusal

3.1 简述

由于使用traces无法区分不确定选择和通用选择：
$\Box Q) = traces(P \sqcap Q) = traces(P) \cup traces(Q)$
引入refusals操作，定义为与 $P$ 并发时，使 $P$ 在首个动作上即发生死锁的所有动作集合 $X$ 的幂集：
$2^X=refusals(P)$
注意，引入Refusal同引入Trace一样，都可作为观测进程行为的重要手段，特别是在6中定义存在不确定性的进程的规范时尤为重要。

3.2 规则

相关规则在课本P89~90，只记录些关键部分：

L1： $refusals(STOP_A)=2^A$
L3： $\to P(x)) = \{X|X \subseteq (\alpha P-B)\}$
L4： $\sqcap Q) = refusals(P) \cup refusals(Q)$
L5： $\Box Q) = refusals(P) \cap refusals(Q)$
L6： $\ || \ Q) = \{X \cup Y \ | \ X \in refusals(P) \wedge Y \in refusals(Q)\}$

4 隐藏(Concealment)

4.1 简述

与投影（ $↾\upharpoonright$ ）操作相对立，隐藏（ $∖\setminus$ ）会将进程中指定集合里的动作从字母表中移除：
$α(P∖C)=(αP)−C\alpha(P \setminus C) = (\alpha P) - C$

注意区分，进程的隐藏使用的是反斜杠（ $∖\setminus$ ），而迹的after操作使用的是正斜杠（ $/$ ）。

同样可以定义与之相对的，将进程的字母表扩展：
$\alpha (P_{+B}) = \alpha P \cup B \\ P_{+B} = (P \ || \ STOP_B) \ \ \ 当B \cap \alpha P = \phi$
扩展后的进程实际还是只执行了之前那些动作，至于字母表中新加进来的动作，仍不在执行序列中：
$traces(P_{+B}) = traces(P)$

4.2 规则

隐藏相关规则见课本P92~93，两条基本的规则如下：

L4： $STOPA∖C=STOPA−CSTOP_A \setminus C = STOP_{A-C}$
L8：若 $\cap C = \phi$ ，则 $\to P(x)) \setminus C = (x:B \to (P(x) \setminus C))$
L9：若 $B$ 是 $C$ 的有限非空子集，则 $\to P(x)) \setminus C = \sqcap_{x\in B}(P(x) \setminus C)$
这条是说对每个 $\in B$ 求其接下来进程在 $C$ 上的隐藏，再合起来做不确定选择。

隐藏（ $∖\setminus$ ）和投影（ $↾\upharpoonright$ ）操作的关系，可从traces里得出：
$\setminus C) = \{t \upharpoonright (\alpha P-C) \ | \ t \in traces(P)\}$

5 Interleaving

5.1 简述

Interleaving（ $∣ ∣ ∣$ ）描述一种最单纯的并发关系，即若干进程可以以任意次序各自推进，同一时刻只能推进一个进程的一个动作，动作之间互不影响。

如两个 $\to choc \to VMS)$ 的interleaving是：
$\begin{aligned} VMS|||VMS = (coin \to \mu X \cdot ( & coin \to choc \to X \\ & | \ choc \to coin \to X)) \end{aligned}$

5.2 规则

Interleaving的"单位元"是 $S T O P$ ，“零"是 $R U N$ ，对” $⊓\sqcap$ “满足分配律，但对” $□\Box$ "不满足分配律。

两进程使用Interleaving结合：
$\to P) \ ||| \ (y \to Q) = (x \to (P ||| (y \to Q)) \ \Box \ y\to ((x \to P) ||| Q)))$
注意refusals无法区分Interleaving和通用选择：
$\Box Q) = refusals(P) \cap refusals(Q)$

6 规范(specification)

6.1 简述

在本章学习中，引入的 $r e f u s a l s$ 操作和之前的 $t r a c e s$ 操作共同描述进程的规范：
$\ sat \ S(tr,ref)$

即是说：
$∀tr,ref⋅tr∈traces(P)∧ref∈refusals(P/tr)⇒S(tr,ref)\forall tr,ref \cdot tr \in traces(P) \wedge ref \in refusals(P/tr) \Rightarrow S(tr,ref)$

6.2 例子

为了付了款的用户不会得不到巧克力，支付的硬币比吐出的巧克力多时，不能拒绝吐出巧克力：
$\downarrow choc < tr \downarrow coin \Rightarrow choc \notin ref)$

为了商家能持续盈利，吐出的巧克力和支付的硬币一样多时，不能拒绝支付硬币：
$\downarrow choc = tr \downarrow coin \Rightarrow coin \notin ref)$

7 发散(Divergence)

7.1 $C H A O S$ 进程

定义混乱的、最不确定的进程 $C H A O S$ ，以下算子对 $C H A O S$ 是严格的，也即 $C H A O S$ 是以下算子的"零"（即结合后的进程仍是 $C H A O S$ ）：
$μX\sqcap, \ / s, \ ||, \ f, \ \Box, \ \setminus C, \ |||, \ \mu X$
$C H A O S$ 进程的特殊行为，在描述规范的 $t r a c e s$ 和 $r e f u s a l s$ 操作上，既表现出 $R U N$ 的特性又表现出 $S T O P$ 的特性：
$traces(CHAOS_A) = traces(RUN_A) = A^* \\ refusals(CHAOS_A) = refusals(STOP_A) = 2^A$

7.2 $d i v e r g e n c e s$ 操作

进程 $P$ 的 $d i v e r g e n c e s$ 操作得到的是其 $t r a c e s$ 操作的子集，仅保留那些经过后会使进程变成混乱的 $C H A O S$ 进程的迹：
$\{ s \ | \ s \in traces(P) \wedge (P/s)=CHAOS_{\alpha P}\}$
从7.1可以看到， $r e f u s a l s$ 操作无法区分 $S T O P$ 和 $C H A O S$ ，而 $d i v e r g e n c e s$ 操作可将其区分：
$\phi \\ divergences(CHAOS) = A^*$
但无法区分" $⊓\sqcap$ “和” $□\Box$ "算子：
$\sqcap Q) = divergences(P \Box Q) =divergences(P) \cup divergences(Q)$

8 整理

整理一下各个操作在特殊进程上的操作结果：

进程\操作	$t r a c e s ()$	$r e f u s a l s ()$	$d i v e r g e n c e s ()$
$QP\ \vert \ Q$	$\cup traces(Q)$	$\cap refusals(Q)$	$\cup divergences(Q)$
$\ \vert\vert \ Q$	课本P53-L1	课本P90-L6	课本P108-L8
$\ \sqcap \ Q$	$\cup traces(Q)$	$\cup refusals(Q)$	$\cup divergences(Q)$
$\ \Box \ Q$	$\cup traces(Q)$	$\cap refusals(Q)$	$\cup divergences(Q)$
$\ \vert\vert\vert \ Q$	课本P101-L1	$\cap refusals(Q)$	课本P108-L9
$STOP_A$	${⟨⟩}\{ \langle \rangle \}$	$2^A$	$ϕ\phi$
$RUN_A$	$A^*$
$CHAOS_A$	$A^*$	$2^A$	$A^*$

其中， $2^A$ 指 $A$ 的幂集，即 $A$ 的所有子集组成的集合。注意和 $A^*$ （见第一篇2.4）的区分。其实也就是要注意， $t r a c e s ()$ 和 $d i v e r g e n c e s ()$ 操作得到的都是迹集合，而 $r e f u s a l s ()$ 操作得到的是动作集合。