### 导言：米尔纳的通信系统演算（CCS）简介
本文档旨在为“Aalborg大学计算机科学系BRICS部门的Semantics and Verification课程”提供支持材料，并可作为独立阅读材料或配合米尔纳教授的经典著作《通信系统演算》（CCS）一起使用。文档由Luca Aceto、Kim G. Larsen以及Anna Ingólfsdóttir共同编写，持续修订中，最新版本可在指定网址获取。读者如发现任何错误或有评论建议，可通过邮件与作者联系。
### 1. 反应系统是什么？
反应系统是计算领域中一类重要的概念模型，用于描述那些随着时间的变化而连续交互的系统。这类系统的典型例子包括操作系统、网络协议、数据库管理系统等。反应系统通常被建模为一系列状态转换，其中每个状态都表示了系统在某个时刻的行为特征。系统通过接收外部输入或事件触发来改变其当前状态，并产生相应的输出。
### 2. 进程代数
进程代数是一种数学形式化的语言，用于描述并发系统的结构和行为。它提供了一种方法来定义和操作进程，即可以独立执行的计算单元。进程代数的一个关键特点在于它能够精确地描述进程之间的交互方式，这使得它成为分析和验证复杂系统的重要工具之一。
### 3. CCS——通信系统演算
#### 3.1 CCS中的进程构造
CCS是一种基于进程代数的形式化语言，由英国计算机科学家罗宾·米尔纳于1980年提出。它提供了一系列基本运算符，用于构建复杂的并发系统模型。以下是一些基本的构造：
- **并行组合**：表示两个或多个进程同时执行。
- **选择**：允许根据接收到的消息选择下一步的操作。
- **前缀**：用于表示进程执行特定动作后进入的状态。
- **隐藏**：用于屏蔽某些内部通信，使其对外部观察者不可见。
- **递归**：允许定义无限循环的进程行为。
#### 3.2 进程的行为
进程的行为可以通过其可能的行为序列来描述，这些序列称为“轨迹”。此外，还有其他几种用于描述进程行为的方法，例如通过等价关系或者逻辑公式。
#### 3.3 CCS的正式定义
CCS的形式化定义涉及到一系列语法和语义规则，这些规则定义了如何构建合法的进程表达式，以及如何解释这些表达式的含义。米尔纳在原书中详细阐述了这些规则，并引入了一些重要的概念，如标记转换系统（LTS）。
### 4. 行为等价
#### 4.1 轨迹等价：第一次尝试
轨迹等价是一种简单的等价关系，它基于两个进程是否具有相同的可能行为轨迹。这种等价关系虽然直观，但过于粗糙，无法捕捉到更细粒度的行为差异。
#### 4.2 强双相似性
强双相似性是一种更精细的行为等价标准，它要求两个进程不仅具有相同的可能行为轨迹，而且对于每一步转换，两个进程都必须能够在相同的情况下做出相同的响应。换句话说，如果一个进程能执行某动作，则另一个进程也必须能够执行该动作，反之亦然。
#### 4.3 弱双相似性
弱双相似性是对强双相似性的扩展，它允许进程在某些情况下跳过τ动作（一种特殊的内部操作），从而更加灵活地比较进程的行为。
### 5. Hennessy-Milner逻辑
Hennessy-Milner逻辑（HML）是一种用于描述进程行为的命题逻辑。它提供了一种方法来表达有关进程行为的属性，如是否可以达到某个状态，或者是否始终会执行某个动作。
#### 5.1 带递归定义的Hennessy-Milner逻辑
带递归定义的HML扩展了原始的HML，允许在公式中使用递归定义。这种扩展增加了逻辑的表达能力，使其能够更自然地描述某些类型的复杂属性。
### 结论
米尔纳的CCS作为一种强大的形式化语言，在描述和分析并发系统方面发挥着重要作用。通过结合LTS和HML等工具，我们可以更准确地理解系统的动态行为，并有效地验证系统的正确性。
