Spécifications Formelles

写在前面：

本文章是根据法国国立高等电力技术、电子学、计算机、水力学与电信学校 (E.N.S.E.E.I.H.T.) 第九学期课程 “Spécifications Formelles” 及以下参考资料总结而来的课程笔记。碍于本人学识有限，部分叙述难免存在纰漏，请读者注意甄别。

参考资料：

• Lost N Found 博客：Transition System(变迁系统) 与 TLA+
• 知乎专栏：π-calculus

---

一、(Bi)Simulation

0 带标签的变迁系统

课程回顾：Transition System(变迁系统)

• 迹 (trace)
• 执行 (Exécutions)

相比于普通的变迁系统（三元组），带标签的变迁系统是一个四元组 $\langle S, L, I, R \rangle$，其中：

• $S$ 是这个系统的状态集。其可以是有限的，也可以是无限的。
• $L$ 是这个系统的字母表（alphabet），也即整个系统的标签集。
• $I$ 是这个系统的初始状态集，$I \subseteq S$。
• $R$ 用来描述这个系统各个状态间的关系，$R \subseteq S \times L \times S$。其中 $(s,l,s') \in R$ 表示在状态 $s$ 与状态 $s'$ 之前存在一个带有标签的事件 $l$，即 $(s,l,s') \triangleq (s \xrightarrow{l} s') \in R$

其中，我们可以将事件分为两类：

• 可观察事件：由普通的标签表示，如 $s_1 \xrightarrow{a} s_2 \xrightarrow{b} s_3$
• 不可观察的内部事件：由特殊标签 $\tau$ 表示。对于观察者而言，其类似于一个黑箱，黑箱内部的标签抽象为 $\tau$。例如 $s_1 \xrightarrow{a} s_4 \quad \triangleq \quad s_1 \xrightarrow{\tau} s_2 \xrightarrow{\tau} s_3 \xrightarrow{a} s_4$

几种特殊的关系：

• $s \Rightarrow s' \quad \triangleq \quad s \xrightarrow{\tau} s_1 \xrightarrow{\tau} ... \xrightarrow{\tau} s'$
• $s \xRightarrow{a} s' \quad \triangleq \quad s \Rightarrow s_1 \xrightarrow{a} s_2 \Rightarrow s'$

1 Strong Simulation

定义

假设存在两个带标签的变迁系统（S.T.E.）：$\mathcal{S}=\langle S,L,I,R\rangle$ 和 $\mathcal{S'}=\langle S',L,I',R'\rangle$。其中，它们有相同的标签集 $\mathcal{L}$：

【定义 1】我们定义一个关系 $Simu \subseteq \mathcal{S} \times \mathcal{S'}$，是 $\mathcal{S'}$ 关于 $\mathcal{S}$ 的强模拟（Strong-Simulation）关系，当且仅当

\begin{align} & \forall s_1 , s_2 \in \mathcal{S}, l \in L, s' \in \mathcal{S'} . \langle s_1 , s_1' \rangle \in Simu \land s_1 \xrightarrow{l} s_2 (\in R)\\ \Rightarrow\\ & \exist s_2'.\langle s_2,s_2' \rangle \in Simu \land s_1' \xrightarrow{l} s_2' (\in R') \end{align}

如图所示，$Simu$ 关系将 $S$ 的状态与 $S'$ 状态联系起来成为可能。这两个系统可以做相同（或更多）的事情，即至少以相同的方式相同多的事件。

满足强模拟关系的两个系统 $\mathcal{S}(i\in I,s\in S)$ 和 $\mathcal{S'}(i' \in I', s' \in S')$ 中的状态 $s,s'$（包括初始状态 $i.i'$）可以用如下形式表示：

$\langle s,s' \rangle \in Simu \\ \forall i \in I. \exist i' \in I'. \langle i,i' \rangle \in Simu$

例一

【对于关系 $\mathcal{S} \times \mathcal{S'}$】

如上图，当 $\langle s_0,s_0' \rangle \in Simu$ 时，$\mathcal{S'}$ 可以模拟 $\mathcal{S}$ 。我们可以确定如下的关系 $R$（并不唯一）：

$R \triangleq \{ \langle s_0,s_0' \rangle, \langle s_1,s_1' \rangle, \langle s_2,s_1' \rangle, \langle s_3,s_2' \rangle, \langle s_4,s_3' \rangle\}$

• 该关系集合中包含初始状态对 $\langle s_0,s_0' \rangle$；
• 满足强模拟关系的定义

我们也可以根据以上的关系集合 $R$ 作出如下所示的图：

【对于关系 $\mathcal{S'} \times \mathcal{S}$】

下面我们考虑关系 $\mathcal{S'} \times \mathcal{S}$，当 $\langle s_0',s_0 \rangle \in Simu$ 时：

可以发现，在【定义 1】中描述了 $\exist s_2'.\langle s_2,s_2' \rangle \in Simu \land s_1' \xrightarrow{l} s_2'$。在关系 $\mathcal{S'} \times \mathcal{S}$ 中，我们考虑 $\langle s_1',s_1 \rangle$ 或 $\langle s_1',s_2 \rangle$，二者只能取其一。无论选取 $\mathcal{S}$ 中的哪一个分支，都有另一个分支的状态被“丢弃”。

所以，关系 $\mathcal{S'} \times \mathcal{S}$ 并不是强模拟关系，但是他们之中有符合强模拟关系的子系统。

性质

算术性质

我们将考虑关于系统 $S \times S$ 的如下关系：

• 空关系：空关系 $\varnothing$ 也是强模拟关系。

• 自反性：任何系统都与它自身存在强模拟关系。

• 传递性：如果关系 $R \subseteq S \times S'$ 和 $R' \subseteq S' \times S''$ 是两个模拟关系，那么 $S \times S''$ 也存在模拟关系：

  $R;R' \triangleq \{\langle s,s'' \rangle \mid \exist x' \in S.\langle s,s' \rangle \in R \land \langle s',s'' \rangle \in R'\}$

• 并集：如果关系 $R$ 和 $R'$ 都是模拟关系，那么他们的并集 $R \cup R'$ 也是模拟关系。

• 克莱尼（Kleene）闭包：如果关系 $R$ 是模拟关系，那么其克莱尼闭包 $R^*$ 也是模拟关系：

  $R^* \triangleq \bigcup_{i \in \mathbb{N}}R^i, \text{其中} R^i \triangleq \underline{ R;\cdots;R} \text{ (i个R)}$

最大强模拟

我们通过在同一个字母表 $\mathcal{L}$ 上定义 $S'$ 对于 $S$ 的最大模拟（Plus grande simulation）关系。存在这种关系的原因在于：

• 两个模拟关系的并集可以组成一个更大的模拟关系；
• 他们之间的所有模拟关系都以 $S \times S'$ 为界；

如果 $S$ 与 $S'$ 都是有限的系统，那么：

• 最大模拟关系是可以计算的；
• 任何关于「$s'$ 能否模拟 $s$」的问题都可以通过转化成最大模拟关系来解决。

我们用 $S \prec S'$ 来表示这种关系。

【组合性（Compositionalité）】

对于两个在同一个字母表 $L$ 上定义的 T.S.E. 系统 $S$ 和 $S'$，我们假设它们之间存在强模拟关系。对于任何包含子系统 $S$ 的系统 $\mathcal{G}$，$\mathcal{G}[S']$ 都可以模拟 $\mathcal{G}[S]$。

$S \xleftrightarrow {simu} S' \quad \xRightarrow{得出} \quad \mathcal{G}[S] \xleftrightarrow {simu} \mathcal{G}[S']$

【迹】

对于两个在同一个字母表 $L$ 上定义的 T.S.E. 系统 $S$ 和 $S'$，我们假设它们之间存在强模拟关系。我们可以得出：

$Prefix(Exec(S)) \subseteq Prefix(Exec(S')) \\ Prefix(Trace(S)) \subseteq Prefix(Trace(S'))$

证明模拟关系

对于两个有限的系统 $S$ 和 $S'$，我们可以：

• 计算系统 $S$ 和 $S'$ 之间的最大强模拟关系；
• 检查是否包含初始状态。

【定义 2】

对于两个在同一个字母表 $L$ 上定义的 T.S.E. 系统 $S$ 和 $S'$， $S'$ 对 $S$ 的最大强模拟是以下关系 $R_{i,i \in \mathbb{N}}$ 的极限（递减）：

$\begin{cases} R_0 & \triangleq \quad S \times S'\\ R_{i+1} & \triangleq \quad R_i \cap \mathcal{F}(R_i) \end{cases}$

其中，

\begin{align} \mathcal{F}(R_i) \triangleq & \{ \langle s_1, s_1' \rangle \mid \forall l \in L. \forall s_2 \in S. \\ & (s_1 \xrightarrow{l} s_2 \Rightarrow \exist s_2' \in S'.s_1' \xrightarrow{l} s_2' \land \langle s_2,s_2'\rangle \in R) \} \end{align}

例一

与之前的例子相同，我们来证明 $\mathcal{S} \times \mathcal{S'}$ 是强模拟的。

根据【定义 2】，我们可以迭代计算出如下的最大强模拟关系 $R_{i,i \in \mathbb{N}}$

\begin{align} R_0 \quad = \quad & S \times S' \\ = \quad & \{ \langle s_0, s_0' \rangle , \langle s_0, s_1' \rangle , \langle s_0, s_2' \rangle , \langle s_0, s_3' \rangle \\ & ,\langle s_1, s_0' \rangle , \langle s_1, s_1' \rangle , \langle s_1, s_2' \rangle , \langle s_1, s_3' \rangle \\ & ,\langle s_2, s_0' \rangle , \langle s_2, s_1' \rangle , \langle s_2, s_2' \rangle , \langle s_2, s_3' \rangle \\ & ,\langle s_3, s_0' \rangle , \langle s_3, s_1' \rangle , \langle s_3, s_2' \rangle , \langle s_3, s_3' \rangle \} \\ & ,\langle s_4, s_0' \rangle , \langle s_4, s_1' \rangle , \langle s_4, s_2' \rangle , \langle s_4, s_3' \rangle \} \\ R_1 \quad = \quad & \{ \langle s_0, s_0' \rangle , \langle s_1, s_1' \rangle , \langle s_1, s_2' \rangle \\ & ,\langle s_2, s_1' \rangle \\ & , \langle s_3, s_1' \rangle , \langle s_3, s_2' \rangle \} \\ & ,\langle s_4, s_0' \rangle , \langle s_4, s_1' \rangle , \langle s_4, s_2' \rangle , \langle s_4, s_3' \rangle \} \\ R_2 \quad = \quad & R_1 \end{align}

所以，$R_2$ 是关系 $\mathcal{S} \times \mathcal{S'}$ 上的最大强模拟，我们有：

\begin{align} s_0 \prec & \; s_0' \\ s_1,s_3 \prec & \; s_1',s_2' \\ s_2 \prec & \; s_1' \\ s_4 \prec & \; s_0',s_1',s_2',s_3' \\ \end{align}

【树状形式】我们更希望使用树状形式更直观地显示最大强模拟 $R_i$ 的推理。

提醒 ⚠️：在下图中

• 我们可以使用类似自动机的“概念”来消费这个字母表 $L$，即下图中圆圈中的字母 $l_i \in L$；
• 在 S.T.E. 系统 $S$ 中，有一个状态 $s_i$ 通过消费字母 $l_i$ 迁移到系统 $s_j$，即 $s_i \xrightarrow{l_i} s_j$；
• 在另一个有着相同字母表 $L$ 的 S.T.E. 系统 $S'$ 中，有 $s_n' \xrightarrow{l_i} s_m'$；
• 我们可以写出如下的关系：$s_i \prec s_n'$，并将其放在左子树，其余部分则在右子树。
• 重复以上步骤，直到 “$\prec$ 关系” 不再改变。

2 Strong Bi-Simulation

定义

双模拟（BiSimulation）系统之间的一种基本关系，用来表示两个系统之间的等价性。但是以下条件不能推导出 BiSimulation 关系：

$\mathcal{S} \text{ simulate } \mathcal{S'} \land \mathcal{S'} \text{ simulate } \mathcal{S} \quad \not\equiv \quad \mathcal{S} \text{ Bi-Simulate } \mathcal{S'}$

下面我们给出强双模拟的定义：

【定义 3】

对于两个系统 $\mathcal{S}$ 和 $\mathcal{S'}$，我们在 $(\mathcal{S} \times \mathcal{S'}) \cup (\mathcal{S'} \times \mathcal{S})$ 上定义双模拟关系 $R$ ，使得：

• $R$ 是 $(\mathcal{S} \times \mathcal{S'}) \cup (\mathcal{S'} \times \mathcal{S})$ 上的强模拟关系；
• $R$ 是一种对称关系；
• 实际上，两个存在双模拟关系的系统在同一时间做相同的事情。

例二

我们考虑以下两个系统：

一个可能的（强）双模拟关系为：

$R \quad \triangleq \quad \{\langle s_0, s_0' \rangle, \langle s_1, s_0' \rangle, \langle s_2, s_1' \rangle, \langle s_0', s_0 \rangle, \langle s_0', s_1 \rangle, \langle s_1', s_2 \rangle\}$

有上述结果可以看出，双模拟关系是对称的。

例三

我们再考虑另外两个系统：

我们可以找到如下（强）模拟关系：

• $\mathcal{S'} \text{ simulate } \mathcal{S}$：

  $R_1 \quad \triangleq \quad \{\langle s_0, s_0' \rangle, \langle s_1, s_1' \rangle, \langle s_2, s_1' \rangle, \langle s_3, s_2' \rangle \}$

• $\mathcal{S} \text{ simulate } \mathcal{S'}$：

  $R_2 \quad \triangleq \quad \{\langle s_0', s_0 \rangle, \langle s_1', s_2 \rangle, \langle s_2', s_3 \rangle \}$

• 但是 $\mathcal{S}$ 和 $\mathcal{S'}$ 并不是（强）双模拟关系

性质

算数性质

• 双模拟（BiSimulation）有着模拟（Simulation）的所有算数性质；
• 此外，任何双模拟都是对称的（即 $R_i = R_i^{-1}$），它是一个等价的关系。

最大强双模拟

我们通过在同一个字母表 $\mathcal{L}$ 上定义 $S$ 和 $S'$ 之间的最大强双模拟（Plus grande BiSimulation）关系。存在这种关系的原因在于：

• 两个双模拟关系的并集可以组成一个更大的双模拟关系；
• 他们之间的所有双模拟关系都以 $(S \times S') \cup (S' \times S)$ 为界；

如果 $S$ 与 $S'$ 都是有限的系统，那么：

• 最大双模拟关系是可以计算的；
• 任何关于「$s'$ 与 $s$ 是否是双模拟关系」的问题都可以通过转化成最大双模拟关系来解决。

我们用 $S \sim S'$ 来表示这种关系。

【组合性（Compositionalité）】

对于两个在同一个字母表 $L$ 上定义的 T.S.E. 系统 $S$ 和 $S'$，我们假设它们之间存在强模拟关系。对于任何包含子系统 $S$ 的系统 $\mathcal{G}$，$\mathcal{G}[S']$ 都可以模拟 $\mathcal{G}[S]$。

$S \sim S' \quad \xRightarrow{得出} \quad \mathcal{G}[S] \sim \mathcal{G}[S']$

【迹】

对于两个在同一个字母表 $L$ 上定义的 T.S.E. 系统 $S$ 和 $S'$，我们假设它们之间存在强模拟关系。我们可以得出：

$Exec(S)=Exec(S') \\ Trace(S)=Trace(S')$

证明模拟关系

与之前的模拟关系类似，对于两个有限的系统 $S$ 和 $S'$，我们可以：

• 计算系统 $S$ 和 $S'$ 之间的最大双模拟关系；
• 检查是否包含初始状态。

【定义 4】

对于两个在同一个字母表 $L$ 上定义的 T.S.E. 系统 $S$ 和 $S'$， $S'$ 对 $S$ 的最大双模拟是以下关系 $R_{i,i \in \mathbb{N}}$ 的极限（递减）：

$\begin{cases} R_0 & \triangleq \quad (S \times S') \cup (S' \times S)\\ R_{i+1} & \triangleq \quad R_i \cap \mathcal{F}(R_i) \cap \mathcal{F}(R_i)^{-1} \end{cases}$

其中，

\begin{align} \mathcal{F}(R_i) \triangleq & \{ \langle s_1, s_1' \rangle \mid \forall l \in L. \forall s_2 \in S \cup S'. \\ & (s_1 \xrightarrow{l} s_2 \Rightarrow \exist s_2' \in S \cup S'.s_1' \xrightarrow{l} s_2' \land \langle s_2,s_2'\rangle \in R_i) \} \end{align}

例三

与之前的【例三】相同，我们来证明 $R = (\mathcal{S} \times \mathcal{S'}) \cup (\mathcal{S'} \times \mathcal{S})$ 是强双模拟的。

根据【定义 4】，我们可以迭代计算出如下的最大强模拟关系 $R_{i,i \in \mathbb{N}}$

\begin{align} R_0 \quad = \quad & (\mathcal{S} \times \mathcal{S'}) \cup (\mathcal{S'} \times \mathcal{S}) \\ R_1 \quad = \quad & \{ \langle s_0, s_0' \rangle , \langle s_0', s_0 \rangle , \langle s_1, s_2' \rangle , \langle s_2', s_1 \rangle , \langle s_2, s_1' \rangle , \langle s_1', s_2 \rangle , \langle s_3, s_2' \rangle , \langle s_2', s_3 \rangle \} \\ R_2 \quad = \quad & \{ \langle s_1, s_2' \rangle , \langle s_2', s_1 \rangle , \langle s_2, s_1' \rangle , \langle s_1', s_2 \rangle , \langle s_3, s_2' \rangle , \langle s_2', s_3 \rangle \} \\ R_3 \quad = \quad & R_2 \end{align}

所以，$R_3$ 是关系 $(\mathcal{S} \times \mathcal{S'}) \cup (\mathcal{S'} \times \mathcal{S})$ 上的最大双模拟，我们有：

3 Weak Simulation

前面我们提到过，事件分为两类：

• 可观察事件：由普通的标签表示，如 $s_1 \xrightarrow{a} s_2 \xrightarrow{b} s_3$
• 不可观察的内部事件：由特殊标签 $\tau$ 表示。对于观察者而言，其类似于一个黑箱，黑箱内部的标签抽象为 $\tau$。例如 $s_1 \xrightarrow{a} s_4 \quad \triangleq \quad s_1 \xrightarrow{\tau} s_2 \xrightarrow{\tau} s_3 \xrightarrow{a} s_4$

在之前的强模拟关系中，我们假设所有的事件都是可观察事件，即标签 $l \in L$ 为普通标签。

但是，对于一个用户可观察事件来讲，其中可能包含若干个不可观察事件。

例如一个加法，

• 从用户的角度观察到的事件为 $x + y = z$；
• 但是从机器的角度，还有“取址”等操作。但是对于用户来讲，“取址”操作是不可见的。

所以，强模拟关系在系统描述中限制太多。相对的，我们提出了弱模拟关系（Weak Simulation）。

定义

假设存在两个带标签的变迁系统（S.T.E.）：$\mathcal{S}=\langle S,L,I,R\rangle$ 和 $\mathcal{S'}=\langle S',L,I',R'\rangle$。其中，它们有相同的标签集 $\mathcal{L}$：

【定义 5】我们定义一个关系 $Simu \subseteq \mathcal{S} \times \mathcal{S'}$，是 $\mathcal{S'}$ 关于 $\mathcal{S}$ 的弱模拟（Weak-Simulation）关系，当且仅当

\begin{align} \forall s_1 , s_2 \in \mathcal{S}, l \in L, s' \in \mathcal{S'} . \\ & (\langle s_1 , s_1' \rangle \in Simu \land s_1 \xrightarrow{l} s_2 (\in R) \\ & \Rightarrow \\ & \exist s_2'.\langle s_2,s_2' \rangle \in Simu \land s_1' \xRightarrow{l} s_2' (\in R')) \\ \land \quad & \\ & (\langle s_1 , s_1' \rangle \in Simu \land s_1 \xrightarrow{\tau} s_2 (\in R) \\ & \Rightarrow \\ & \exist s_2'.\langle s_2,s_2' \rangle \in Simu \land s_1' \Rightarrow s_2' (\in R')) \\ \end{align}

如图所示，$Simu$ 关系将 $S$ 的状态与 $S'$ 状态联系起来成为可能。

满足弱模拟关系的两个系统 $\mathcal{S}(i\in I,s\in S)$ 和 $\mathcal{S'}(i' \in I', s' \in S')$ 中的状态 $s,s'$（包括初始状态 $i.i'$）可以用如下形式表示：

$\langle s,s' \rangle \in Simu \\ \forall i \in I. \exist i' \in I'. \langle i,i' \rangle \in Simu$

例四

假设有如下两个系统 $\mathcal{S}$ 和 $\mathcal{S'}$：

\begin{align} \mathcal{S}: \quad & \to s_0 \xrightarrow{a} s_1 \xrightarrow{b} s_2 \\ \mathcal{S'}: \quad & \to s_0' \xrightarrow{\tau} s_1' \xrightarrow{a} s_2' \xrightarrow{\tau} s_3' \xrightarrow{b} s_4'\\ \end{align}

• $\mathcal{S'}$ 弱模拟于 $\mathcal{S}$：

  $R \triangleq \{ \langle s_0, s_0' \rangle, \langle s_1, s_2' \rangle, \langle s_2, s_4' \rangle \}$

  注意 ⚠️：该结果并不唯一，比如我们可以添加 $\langle s_1, s_3' \rangle$ 对。

• 相反地，$\mathcal{S}$ 弱模拟于 $\mathcal{S'}$：

  $R \triangleq \{ \langle s_0', s_0 \rangle, \langle s_1', s_0 \rangle, \langle s_2', s_1 \rangle , \langle s_3', s_1 \rangle , \langle s_4', s_2 \rangle\}$

• 事实上，$\mathcal{S}$ 和 $\mathcal{S'}$ 在这里是弱双模拟（Weak BiSimulation）的。

例五

假设有如下两个系统 $\mathcal{S}$，$\mathcal{S'}$ 和 $\mathcal{S''}$：

• $\mathcal{S''}$ 弱模拟于 $\mathcal{S'}$：

  $R \triangleq \{ \langle s_0', s_0'' \rangle, \langle s_1', s_0'' \rangle, \langle s_2', s_2'' \rangle, \langle s_3', s_1'' \rangle \}$

• $\mathcal{S'}$ 弱模拟于 $\mathcal{S}$：

  $R \triangleq \{ \langle s_0, s_0' \rangle, \langle s_1, s_1' \rangle, \langle s_2, s_0' \rangle, \langle s_3, s_3' \rangle, \langle s_4, s_2' \rangle \}$

性质

• 弱模拟（Weak-Simulation）有着与强模拟（Strong-Simulation）相同的算数性质；

• 类似的，弱模拟（Weak-Simulation）也存在最大弱模拟关系（plus grande simulation faible）；

• 弱模拟的组合性要比之前的强模拟低得多。在一般情况下，不能使用另一个弱模拟的子系统来替换原来的子系统。即

  $S \xleftrightarrow {weak-simu} S' \quad \not\xRightarrow{不能得出结论} \quad \mathcal{G}[S] \xleftrightarrow {weak-simu} \mathcal{G}[S']$

• 关于迹（Trace）：我们将 $\tau$ 统一转化成 $\epsilon$；

• 【最大弱模拟】可以按照与[最大强模拟](# 最大强模拟)相同的规则计算，并使用【定义 6】替换定义 2。

4 Weak Bi-Simulation

定义

下面我们给出弱双模拟（Weak Bi-Simulation）的定义：

【定义 6】对于两个系统 $\mathcal{S}$ 和 $\mathcal{S'}$，我们在 $(\mathcal{S} \times \mathcal{S'}) \cup (\mathcal{S'} \times \mathcal{S})$ 上定义弱双模拟关系 $R$ ，使得：

• $R$ 是 $(\mathcal{S} \times \mathcal{S'}) \cup (\mathcal{S'} \times \mathcal{S})$ 上的强模拟关系；
• $R$ 是一种对称关系；
• 我们用 【$S \approx S'$】 来表示这种关系。

例六

假设有如下两个定义在相同字母表 $L$ 的 S.T.E. 系统 $\mathcal{S}$ 和 $\mathcal{S'}$：

\begin{align} \mathcal{S}: \quad & \to s_0 \xrightarrow{a} s_1 \\ \mathcal{S'}: \quad & \to s_0' \xrightarrow{\tau} s_1' \xrightarrow{a} s_2' \\ \end{align}

$\mathcal{S}$ 与 $\mathcal{S'}$ 是弱双模拟的，模拟关系如下所示：

$R \triangleq \{ \langle s_0, s_0' \rangle, \langle s_0', s_0 \rangle, \langle s_0, s_1' \rangle, \langle s_1', s_0 \rangle, \langle s_1, s_2' \rangle, \langle s_2', s_1 \rangle \}$

例七

假设有如下两个定义在相同字母表 $L$ 的 S.T.E. 系统 $\mathcal{S}$ 和 $\mathcal{S'}$：

$\mathcal{S}$ 与 $\mathcal{S'}$ 是弱双模拟的，我们可以以树的形式证明：

• 证明 $s_0 \approx s_0'$：

  

• 证明 $s_1 \approx s_1'$：

  

• …

二、CCS

0 前情

随着计算机网络的出现和广泛应用，一个问题由此显现：通信系统与我们大多数人熟悉的计算系统有着根本的不同；用来建模传统计算系统的工具未能捕捉到分布式世界中许多计算的相关特性（缺少相关的模型）。
所以有些人便开始寻找更有用、更现实的方式来描述 Communicating Systems，这便是：process calculus （或者叫： process algèbres）。

CSS (Calculus of Communicating System) 就是其中的一种理论基础。

1 相关性质

Syntax

• 事件语言 $L$ 包含成对的称为动作 $\mathcal{A}$ 的互补事件 $\overline{\mathcal{A}}$，以及 $\tau$ 事件：

  $L \triangleq \{ \tau \} \cup \mathcal{A} \cup \overline{\mathcal{A}}$

  其中：

  • $\mathcal{A}$ 是一个动作（Action）集，其对应接收消息的事件（Event）；
  • $\overline{\mathcal{A}} \triangleq \{ \overline{a} \mid a \in \mathcal{A}\}$ 是事件集 $\mathcal{A}$ 的互补事件集合，其对应发送消息的事件（Event）。

• CSS 术语（Termes）由如下语法描述：

  • $\mathcal{P} ::= 0$：表示已经结束的过程 $\mathcal{P}$（非活动进程）；

  • $\mathcal{P} ::= l.\mathcal{P}_1$：表示一个过程的前缀（Prefix），我们先执行事件 $l \in L$，然后执行$\mathcal{P}_1$；

  • $\mathcal{P} ::= \mathcal{P}_1 \parallel \mathcal{P}_2$：并行结构，表示两个 $\mathcal{P}_i$ 同步地执行；

    （1）我们先找到 $\parallel$ 两端的过程 $\mathcal{P}$ 中事件字母表 $L$ 中相交的集合 $\Theta$

    （2）当 $\parallel$ 两端的任意一个过程 $\mathcal{P}$ 执行到 $\Theta$ 中的元素 $l_\theta$时，都会检查是否其他过程也可以执行该元素 $l_\theta$；

    （3）如果可以，则两端的过程同时执行元素 $l_\theta$；

    （4）如果不可以，则暂停本端执行，直到另一端执行到该元素 $l_\theta$。

    【例子】$b.a.c.0 \parallel d.e.a.0, \qquad \Theta = \{a\}$

        graph TD
    b.a.c.0//d.e.a.0 --b--> a.c.0//d.e.a.0
    b.a.c.0//d.e.a.0 --d--> b.a.c.0//e.a.0
    
    a.c.0//d.e.a.0 --d-->a.c.0//e.a.0
    a.c.0//e.a.0 --e--> a.c.0//a.0
    a.c.0//a.0 --a-->c.0
    a.c.0//a.0 --a-->0
    c.0 --c--> 0
    
    b.a.c.0//e.a.0 --b--> a.c.0//e.a.0
    b.a.c.0//e.a.0 --e--> b.a.c.0//a.0
    b.a.c.0//a.0 --b--> a.c.0//a.0

  • $\mathcal{P} ::= \mathcal{P}_1 + \mathcal{P}_2$：选择结构，表示在两个 $\mathcal{P}_i$ 中选择一个执行；

  • $\mathcal{P_1}_1 ::= \mathcal{v}\text{a}.\mathcal{P}$：给 $\mathcal{P}_1$ 声明一个局部“canal”。

• 如下语法描述了使用方程组形式来定义过程（可以是递归形式的）：

  $\{ X_i \triangleq E_i\}$

  其中，$E_i$ 是过程 $X_i$ 中涉及变量的 CCS 术语（Termes）。

  • 此约束允许存在唯一解；
  • CCS 的过程就是 $X_i$；
  • 这个定义是被“保护的”，其定义的形式如下

• CCS 程序 $\mathcal{G}$ 是一组过程 $\mathcal{P}$ 的定义：

  • $\mathcal{G} \quad ::= \quad \mathcal{D} \mid \mathcal{DG}$
  • $\mathcal{D} \quad ::= \quad X \triangleq \mathcal{P}$
  • $\mathcal{P} \quad ::= \quad 0 \mid l.\mathcal{P} \mid \mathcal{P} \parallel \mathcal{P} \mid \mathcal{P} + \mathcal{P} \mid v\text{a}.\mathcal{P}$
  • $\mathcal{P}' \quad ::= \quad X \mid 0 \mid l.\mathcal{P}' \mid \mathcal{P}'\parallel \mathcal{P}' \mid \mathcal{P}' + \mathcal{P}' \mid v\text{a}.\mathcal{P}'$

• 正确的定义：

  $X \triangleq a.X \qquad X \triangleq a.0 \parallel b.X \qquad X \triangleq a.(b.0 \parallel X)$

• 错误的定义：

  $X \triangleq X \qquad X \triangleq a.0 + (b.0 \parallel X)$

例一

假设有如下两个定义在相同字母表 $L$ 的 S.T.E. 系统 $\mathcal{S}$ 和 $\mathcal{S'}$：

它们可以通过以下两个 CCS 过程表示：

• $\mathcal{P}' \triangleq a.(b.0 + \tau .c.0)$
• $\mathcal{P} \triangleq a.(\tau .c.0 + b.0) + a.c.0$

例二

我们模拟一下投币式自动售货机：我们可以用 20 分买到茶（tea）和咖啡（coffee）；用 40 分买到卡布奇诺（cappuccino）。售货机只接收 10 分和 20 分的硬币。我们对售货机 $Machine$ 进行建模：

• $Machine \triangleq 20.Service_1 + 10.10.Service_1$
• $Service_1 \triangleq \overline{_{coffee}}.Machine + \overline{_{tea}}.Machine + 20.Service_2 + 10.10.Service_2$
• $Service_2 \triangleq \overline{_{cappuccino}}.Machine$

同样的，我们也可以对用户进行建模，假设用户 $User$ 用了两个 10 分的硬币买了一杯咖啡：

• $User \triangleq \overline{10}. \overline{10}. coffee.0$

Semantic

• 我们为 CCS 定义了一个操作语义 (Semantic)，即我们对于每个 CCS 过程定义了一个 S.T.E.。
• 为了简化转换的描述，我们确定了某些等价项（例如，$A+B \equiv B+A$）。这种等价关系实际上是对CCS 运算符的同余 (Congruence)。

同余 Congruence

对于一个给定的 process algèbres 来说，同余 (Congruence) 是一个与该 process algèbres 的算子相换的等价物。

【定义 5】CCS 的过程 (Process) 之间的等价 $\cong$是同余的，当且仅当，对于所有过程，如 $P \cong Q$，我们有：

• $a.P \cong a.Q$
• $P+M \cong Q+M$ 或 $M+P \cong M+Q$
• $P \parallel M \cong Q \parallel M$ 或 $M \parallel P \cong M \parallel Q$
• $v\text{a}.P \cong v\text{a}.Q$

结构同余 Structural Congruence

【定义 6】结构同余 $P \equiv Q$ 是由以下规则决定的。它符合【定义 5】的条件：

• 通过 $\alpha - \text{conversion}$ 改变“canal”名称：如果 $b$ 没有出现在 $P$ 中，那么 $v\text{a}.P \equiv v\text{b}.P[a \leftarrow b]$
• “$+$” 满足交换律和结合率：$P+Q \equiv Q+P$ 和 $P+(Q+R) \equiv (P+Q)+R \equiv P+Q+R$
• “$\parallel$” 的阿贝尔幺半群定律 (Abelian monoid law)：$P \parallel 0 \equiv P$、$P \parallel Q \equiv Q \parallel P$、$P \parallel (Q \parallel R) \equiv (Q \parallel P) \parallel R \equiv Q \parallel P \parallel R$
• $v\text{a}.0 \equiv 0$、$v\text{a}.v\text{b}.P \equiv v\text{b}.v\text{a}.P$