第 5 章 线性时序逻辑 本章介绍 (命题) 线性时序逻辑 (Linear Temporal Logic, LTL), 一种适合描述 LT 性 质的逻辑形式化方法. 本章首先定义线性时序逻辑的语法和语义, 并通过一些例子说明如 何用线性时序逻辑描述重要的系统性质. 然后聚焦于 LTL 的基于 Büchi 自动机的模型检 验算法. 该算法可以用来回答以下问题: 给定一个迁移系统 TS 和 LTL 公式 φ, 如何检验 φ 是否在迁移系统 TS 中成立? 5.1 线性时序逻辑述要 对于反应系统, 正确性依赖于系统执行 (不仅依赖于计算的输入和输出) 以及公平性问 题. 对于处理这些问题, 时序逻辑具有形式化方法的优越性. 时序逻辑用一种允许引用反应 系统的无穷行为的模态扩充命题逻辑或谓词逻辑的概念. 为表达关于执行中的状态标记之 间的关系的性质, 即 LT 性质, 时序逻辑提供了非常直观而又具有数学严谨性的记法. 古代 的哲学等领域就曾研究时序逻辑及相关的模态逻辑. 20 世纪 70 年代末, Pnueli 提出把时 序逻辑应用到复杂计算机系统验证上. 本章将集中讨论命题时序逻辑, 即命题逻辑的时序模态扩充. 这些逻辑应与那些在谓 词逻辑之上施加时序模态的一阶 (或高阶) 时序逻辑区分. 本书假设读者在某种程度上熟悉 命题逻辑的基本原理. 在附录 A 的 A.3 节中, 可以找到本书所用记号的简介和汇总. 大多 数时序逻辑中的基本时序模态包括以下运算符: . 终将 (未来终究要) □ 总是 (现在和未来总是) 在时序逻辑中, 时间的底层特性可以是线性的或分支的. 在线性时间观点中, 时间的每一时 刻都有单一的后继时刻; 而在分支时间观点中, 有一个树状分支结构, 时间在其中会被分裂 为可选的方向. 本章考虑 LTL, 它是一种基于线性时间观点的时序逻辑. 第 6 章介绍 CTL (计算树逻辑), 它是一种基于分支时间观点的逻辑. 一些模型检验工具将 LTL (或略有不同 的 LTL) 用作性质准述语言. 模型检验器 SPIN 是这些自动验证工具中的典型. LTL 的优 点之一是不需要任何新机制就能施加公平性假设 (像强公平性和弱公平性等): 典型的公平 性假设都可在 LTL 中描述. 可用 LTL 的算法在公平性约束下验证 LTL 公式. 但这不适用 于 CTL. 在详细介绍 LTL 之前, 为了避免读者产生任何可能的困惑, 先简要说明形容词 “时序 的”. 虽然它使人想起反应系统中的实时行为, 但这只在抽象意义下是正确的. 时序逻辑允 许描述事件的相对顺序. 例如 “司机一旦踩下刹车, 汽车就停下来”, 或 “消息在发出后收 到”. 但是, 时序逻辑不支持任何涉及事件准确计时的方法. 不能描述事实: 在刹车和实际停 车之间至少有 3μs 的最小延迟. 在迁移系统中, 时序逻辑的基本模态不能给出迁移的持续 158 模型检验原理 时间或状态的逗留时间. 这些模态只是允许描述在执行期间状态标记出现的顺序, 或允许 估计某些状态标记在一个 (或所有) 系统执行中无限经常地出现. 于是, 可以说时序逻辑中 的模态是时间抽象的. 本章要讨论的 LTL 可为一类同步系统表示计时, 这类系统中所有组件都以步骤锁定 方式行进. 在这种设置下, 一个迁移对应单个时间单位的推进. 现在的时刻对应当前状 态, 而下一时刻对应直接后继状态, 因而底层时间域是离散的. 换言之, 就是设想在时间点 0, 1, 2, 可观察到系统行为. 第 9 章将讨论如何利用连续时间域来处理异步系统中的实 时约束, 将介绍 CTL 的时控版本, 称作时控 CTL. 表 5.1 总结了本书所讨论的主要时序逻 辑的不同点. 表 5.1 本书中的时序逻辑分类 逻 辑 线性时间 分支时间 实时要求 (基于路径的) (基于状态的) (连续时间域) LTL √ CTL √ 时控 CTL √ √ 5.1.1 语法 本节描述语法规则, 根据这些规则可以构造 LTL 公式. LTL 公式的基本要素是原子命 题 (状态标记 a 2 AP), 例如合取 ^ 和取非 : 这样的布尔联结词, 以及两个基本时序模态 (读作 “下一步”) 和 U (读作 “直到”). 原子命题 a 2 AP 在迁移系统中表示状态标记 a. 通常情况下, 原子 (命题) 就是关于控制变量之值 (如程序图中的位置) 或程序变量之值的 断言, 如 x > 5 或 x . y. 模态 是一元前缀运算符, 需要一个 LTL 公式作为操作数. 如 果 φ 在下一 “步” 成立, 则公式 φ 在当前时刻成立. 模态 U 是一个二元中缀运算符, 需 要两个 LTL 公式作为操作数. 如果存在未来的某一刻 φ2 成立, 而 φ1 一直成立到未来这一 时刻, 则公式 φ1 U φ2 在当前时刻成立. 定义 5.1 LTL 的语法 原子命题集合 AP 上的 LTL 公式根据以下语法à构造: φ ::= true a φ1 ^ φ2 :φ φ φ1 U φ2 其中 a 2 AP. ■ 本书在大多数情况下不明确给出命题集合 AP, 因为它可从上下文得到或者可以定义 为 LTL 公式中的原子命题的集合. 运算符的优先级如下. 一元运算符比二元运算符更优先. : 和 具有同样的优先级. 时序运算符 U 优先于 ^、_ 和 !. 适当的时候可以省略括号, 例如, 可以用 :φ1 U φ2 代 替 (:φ1) U ( φ2). 运算符 U 是右结合的, 例如, φ1 U φ2 U φ3 表示 φ1 U (φ2 U φ3). à 就是使用更灵活的巴科斯范式 (Backus Naur Form, BNF). 具体地说, 把非终止符看作派生词 (公式) 和规则中的标 记. 此外, 还使用在语法中未出现的括号, 例如在 a∧(b U c) 中. 这种简化的记法通常被称为抽象语法, 用于确定某些逻辑 (或 其他演算项) 的形成语法. 第 5 章 线性时序逻辑 159 使用布尔联结词 ^ 和 :, 就可实现命题逻辑的全部能力. 其他布尔联结词, 如析取 _、 蕴涵 !、等价 $ 和奇偶运算符 (异或运算符) , 可按如下方法导出: φ1 _ φ2 def = :(:φ1 ^ :φ2) φ1 ! φ2 def = :φ1 _ φ2 φ1 $ φ2 def = (φ1 ! φ2) ^ (φ2 ! φ1) φ1 φ2 def = (φ1 ^ :φ2) _ (φ2 ^ :φ1) ... U 运算符也可表示时序模态 . (“终将”, 将来某一时刻) 和 □ (“总是”, 从现在到永远总 是), 方法如下: .φ def = true U φ □φ def = :.:φ 因此, 可以得到 . 和 □ 如下的直观意义. .φ 确保 φ 最终将取真. □φ 成立当且仅当 :φ 不会终将成立. 这相当于 φ 从现在开始总是成立. 图 5.1 时序模态的直观语义 图 5.1 给出了当模态的操作数出自原子命题 fa, bg 时, 时序模态的直观含义. 左边列出 了一些 LTL 公式, 而右边描述了状态序列 (即路径). 通过组合时序模态 . 和 □, 可得到新时序模态. 例如, □.a (“总是终将 a”) 描述以下 (路径) 性质: 对于任何时刻 j, 存在时刻 i . j, 此刻访问的是 a 状态. 这相当于无限次访问 a 状态. 双模态 .□a 表示从某一时刻 j 开始, 只访问 a 状态. 所以: □.φ的含义是 “无限经常 φ” .□φ的含义是 “终将总是 φ” 在给出 LTL 正式的语义之前, 先看一些例子. 160 模型检验原理 例 5.1 互斥问题的性质 考虑两个并发进程 P1 和 P2 的互斥问题. 进程 Pi 由 3 个位置组成: à 非关键节段; á 当进程要进入关键节段时进入的等待节段; . 关键节段. 令命题 waiti 和 criti 分别表示 进程 Pi 处于等待节段和关键节段. P1 和 P2 永不同时进入关键节段, 该安全性质可用 LTL 公式描述为 □(:crit1 _ :crit2) 这个公式表明, 总是 (□) 至少有一个进程不在关键节段 (:criti). 每一进程 Pi 无限经常地处于关键节段, 这一活性要求可由 LTL 公式描述为 (□.crit1) ^ (□.crit2) 弱化的形式, 即每一等待进程终将进入关键节段 (即无饥饿). 可以通过使用额外的命题 waiti 描述为 (□.wait1 ! □.crit1) ^ (□.wait2 ! □.crit2) 利用原子命题 waiti 和 criti, 这些公式最终仅与位置 (即程序计数器的值) 相关. 然而命题 也与程序变量相关. 例如, 可以用二进制信号 y 解决互斥问题, 公式 □((y = 0) ! crit1 _ crit2) 表明只要信号 y 的值为 0, 就有一个进程处于关键节段. ■ 例 5.2 哲学家就餐问题的性质 哲学家就餐问题 (见例 3.2) 的无死锁性质, 可用 LTL 公式描述为 □:( ^ 0.i<n waiti ^ ^ 0.i<n occupiedi) 此处, 假设有 n 位哲学家和 n 只筷子, 下标为 0 到 n .. 1. 原子命题 waiti 意味着哲学家 i 已经手握一只筷子, 正在等待他左面或右面的筷子. 同样, occupiedi 表示第 i 只筷子正被 占用. ■ 例 5.3 交通灯问题的性质 对于有 “绿灯”“红灯” 和 “黄灯” 3 个阶段的交通灯, 活性性质 □.green 表示交通灯 可以无限次变成绿灯. 通过表示任一阶段的前驱阶段的 LTL 公式的合取, 可得到关于交通 灯的周期及次序的描述. 例如, 规定 “一旦处于红灯阶段, 交通灯不能立即变成绿灯”, 可由 LTL 公式描述为 □(red ! : green) 规定 “一旦处于红灯阶段, 总是在变为黄灯一段时间后终将变为绿灯” 可以表示为 □(red ! (red U (yellow ^ (yellow U green)))) ■ 第 5 章 线性时序逻辑 161 类似于 “每个请求终将得到响应” 的进程性质可以用下面的公式描述: □(request ! .response) 注记 5.1 公式的长度 令 jφj 表示 LTL 公式 φ 的长度, 它等于 φ 中运算符的个数. 对 φ 的结构使用归纳法, 可以很容易地定义它. 例如, 公式 true 和 a 2 AP 的长度为 0, 公式 a _ b 和 a _ :b 的长 度为 2, 公式 ( a) U (a ^ :b) 的长度为 4. 在本书中, 多半需要渐近大小 Θ(jφj). 因此, 无 论在确定长度时是否考虑导出的布尔运算符 _、! 等, 以及是否考虑导出的时序模态 . 和 □, 都没有关系. ■ 5.1.2 语义 LTL 公式表示路径 (事实上是它们的迹) 的性质. 这意味着一个路径可以满足或不满 足一个 LTL 公式. 为了精准地表述一个路径何时满足 LTL 公式, 按如下方法进行. 首先, LTL 公式 φ 的语义定义为语言 Words(φ), 它包含了字母表 2AP 上所有满足 φ 的无限单 词. 也就是说, 给每个 LTL 公式关联唯一一个 LT 性质. 然后, 把语义扩展为对迁移系统的 路径和状态的解释. 定义 5.2 LTL 的语义 (单词上的解释) 令 φ 为 AP 上的一个 LTL 公式. φ 诱导的 LT 性质为 Words(φ) = nσ 2 (2AP)ω j σ j= φo 其中, 满足关系 j= (2AP)ω LTL 是具有图 5.2 所示性质的最小关系. ■ σ |= true σ |= a iff a ∈ A0 (即 A0 |= a) σ |= φ1 ∧ φ2 iff σ |= φ1 且 σ |= φ2 σ |= .φ iff σ .|= φ σ |= .φ iff σ[1..] = A1A2A3 · · · |= φà σ |= φ1 U φ2 iff .j . 0. σ[j..] |= φ2 且 .0 . i < j. σ[i..] |= φ1 图 5.2 2AP 上的无限单词的 LTL 语义 (可满足关系 |=) 此处, 对于 σ = A0A1A2 2 (2AP)ω, σ[j..] = AjAj+1Aj+2 是 σ 的从第 j +1 个符 号 Aj 开始的后缀. 注意, 在 LTL 公式语义的定义中, 单词片段 σ[j..] 不能用 Aj 代替. 例如, 对于公式 (a U b), 为了能够在下一步中得到子式 a U b 的真值, 只能考虑后缀 A1A2A3 . 对于导出运算符 . 和 □, 预期的结果为 σ j= .φ iff 9j . 0. σ[j..] j= φ σ j= □φ iff 8j . 0. σ[j..] j= φ à 在形式语言中, [1..] 表示从 1 开始递增. [i..] 和 [j..] 等的含义与之类似. 162 模型检验原理 从 . 的定义和 U 的语义可直接得到关于 . 的命题. 由 σ j= □φ = :.:φ iff :9j . 0. σ[j..] j= :φ iff :9j . 0. σ[j..] 6j= φ iff 8j . 0. σ[j..] j= φ 可得关于 □ 的命题. 现在可导出 . 和 □ 的组合的语义: σ j= □.φ iff ∞9 j. σ[j..] j= φ σ j= .□φ iff ∞8 j. σ[j..] j= φ 其中, ∞9 j 表示 “对无限多个 j 2 N”, 即 8i . 0. 9j . i; 而 ∞8 j 表示 “对几乎所有 j 2 N”, 即 9i . 0. 8j . i. 下面证明第一个命题, 第二个命题的证明与之类似. σ j= □.φ iff 8i . 0. σ[i..] j= .φ iff 8i . 0. 9j . i. σ[j..] j= φ iff ∞9 j. σ[j..] j= φ 接下来, 确定 LTL 公式对于迁移系统的语义. 根据 LT 性质的可满足关系 (见定义 3.7), 如果所有从 s 开始的路径都满足 φ, 则 LTL 公式 φ 在状态 s 处成立. 如果迁移系统 TS 满足 LT 性质 Words(φ), 即, 如果 TS 的所有起始路径 (从初始状态 s0 2 I 开始的路 径) 都满足 φ, 则称 TS 满足 φ. 不失一般性, 可假设迁移系统 TS 没有终止状态 (若有, 则可引入陷阱状态). 因此, 可 假设所有路径和迹是无限的. 作此假设仅为简化问题, 对于有限路径也可定义 LTL 语义. 注意, 语义与 TS 是否有限无关. 只有对于 5.2 节的模型检验算法才要求 TS 是有限的. 像对待 LT 性质一样, 在对 AP′ 上的迁移系统 TS 定义 TS j= φ 时, 假设 φ 是原子命 题在 AP = AP′ 中的 LTL 公式 (此处可以更自由一些, 准许 AP AP′). 定义 5.3 LTL 在路径和状态上的语义 令 TS=(S, Act,!, I, AP,L) 是没有终止状态的迁移系统, 令 φ 是 AP 上的 LTL 公式. . 对于 TS 的无限路径片段 π, 满足关系定义为 π j= φ iff trace(π) j= φ . 对于状态 s 2 S, 满足关系 j= 定义为 s j= φ iff 8π 2 Paths(s). π j= φ . 若 Traces(TS) Words(φ), 则称 TS 满足 φ, 记作 TS j= φ. ■ 由定义 5.3 可直接得出 TS j= φ iff Traces(TS) Words(φ) (* 定义 5.3 *) iff TS j= Words(φ) (* LT 性质中 j= 的定义 *) iff 8π 2 Paths(TS), π j= φ (* Words(φ) 的定义 *) iff 8s0 2 I, s0 j= φ (* 定义 5.3 中状态的 j= *) 第 5 章 线性时序逻辑 163 因此, TS = φ 当且仅当对于 TS 的所有初始状态 s0 都有 s0 j= φ. 例 5.4 LTL 的语义 考虑由图 5.3 描述的迁移系统, 命题集为 AP = fa, bg. 图 5.3 关于 LTL 语义的例子 例如, 因为所有状态都用 a 标记, 所以 TS 的迹是满足对所有 i . 0 都有 a 2 Ai 的 单词 A0A1A2 , 因此 TS j= □a. 还可得 si j= □a, i = 1, 2, 3. 而且因为 s2 j= a ^ b 且 s2 是 s1 的唯一后继, 所以 s1 j= (a ^ b). 由 s3 2 Post(s2), s3 2 Post(s3), s3 6j= a ^ b 得 s2 6j= (a ^ b), s3 6j= (a ^ b). 因为 s3 是一个初始状态且 s3 6j= (a ^ b), 所以 TS 6j= (a ^ b). 另一个例子是 TS j= □(:b ! □(a ^ :b)) 它成立是因为 s3 是唯一一个 :b 状态, 而且到达 s3 后再也不能离开 s3, 同时 a ^ :b 在 s3 处成立. 但是, TS 6j= b U (a ^ :b) 这是因为起始路径 (s1s2)ω 不会访问 a ^ :b 成立的状态. 注意, 起始路径 (s1s2).sω3 满足 b U (a ^ :b). ■ 注记 5.2 否定的语义 对于路径, π j= φ 当且仅当 π 6j= :φ. 这是因为 Words(:φ) = (2AP)ω n Words(φ) 然而, 命题 TS 6j= φ 和 TS j= :φ 一般是不等价的. 而是 TS j= :φ 蕴涵 TS 6j= φ. 注意, TS 6j= φ iff Traces(TS) . Words(φ) iff Traces(TS) n Words(φ) 6= . iff Traces(TS) \ Words(:φ) 6= . 因此, 一个迁移系统 (或是一个状态) 可能既不满足 φ 也不满足 :φ. 这是因为, 有可能存在 路径 π1 和 π2 使得 π1 j= φ 和 π2 j= :φ (因此 π2 6j= φ). 此时, TS 6j= φ 且 TS 6j= :φ 成立. 为演示这种效果, 考虑图 5.4 中描绘的迁移系统. 令 AP = fag. 因为起始路径 s0(s2)ω 6j= .a, 所以 TS 6j= .a; 另一方面, 因为起始路径 s0(s1)ω j= .a, 所以 s0(s1)ω 6j= :.a, 因此 TS 6j= :.a. ■ 164 模型检验原理 图 5.4 满足 TS .|= .a 和 TS .|= ..a 的迁移系统 5.1.3 准述性质 例 5.5 重访基于信号的互斥 考虑图 5.5 所描绘的迁移系统 TSSem, 它给出了互斥问题的一个基于信号的解决方案. 图 5.5 基于信号的互斥算法的迁移系统 每个形如 hc1, , i 的状态都用 crit1 标记, 而每个形如 h, c2, i 的状态都用 crit2 标记. 则有 TSSem j= □(:crit1 _ :crit2) 且 TSSem j= □.crit1 _ □.crit2 其中, 第一个 LTL 公式代表互斥性质, 第二个 LTL 公式表示两个进程中至少有一个无限次 进入关键节段. 然而 TSSem 6j= □.crit1 ^ □.crit2 因为缺少任何公平性假设, 不能保证进程 P1 能够无限次进入关键节段. 它有可能一次也不 能进入 (P2 也有类似的情况). 同样的讨论可应用到证明 TSSem 6j= □.wait1 ! □.crit1 上. 这是因为, 原则上, 进程 P1 一旦开始等待, 可能就会总也得不到它的机会. ■ 例 5.6 模 4 计数器 模 4 计数器可以由一个顺序电路 C 表示, 每当第 4 个周期时输出 1, 其余周期输出 0. C 没有输入位, 有一个输出位 y 和两个寄存器 r1、r2. 寄存器的赋值 [r1 = c1, r2 = c2] 可 用数值 i = 2 r1 +r2 确定. i 的值每一周期增加 1 (模 4). 用如下方法构造 C, 恰好当 i = 0 第 5 章 线性时序逻辑 165 (因此, r1 = r2 = 0) 时输出位 y 置位. 迁移关系和输出函数由 δr1 = r1 r2, δr2 = :r1, λy = :r1 ^ :r2 给出. 图 5.6 给出了电路图和迁移系统 TSC. 图 5.6 模 4 计数器 令 AP = fr1, r2, yg. 下面的命题可以从 TSC 直接推出: TSC j= □(y $ :r1 ^ :r2) TSC j= □(r1 ! ( y _ y)) TSC j= □(y ! ( :y ^ :y)) 如果假定只有输出变量 y (而不是寄存器的值) 可以由观察者感知, 那么 AP 的一个合适选 择是 AP = fyg. 至少每 4 个周期输出 1 的性质在 TSC 中成立, 即, 有 TSC j= □ (y _ y _ y _ y) 这些输出是周期性产生的, 每当第 4 个周期时输出 1, 这个事实表示为 TSC j= □(y ! ( :y ^ :y ^ :y)) ■ 例 5.7 通信通道 考虑两个通信进程间的一个单向通道、一个发送器 S 和一个接收器 R. 发送器 S 配 置一个输出缓冲区 S.out, 接收器 R 配置一个输入缓冲区 R.in. 如果发送器 S 发送消息 m 给 R, 它就把消息插入它的输出缓冲区 S.out 中. 输出缓冲区和输入缓冲区是通过一个单 向通道连接的. 接收器 R 接收消息, 并删除其输入缓冲区 R.in 中的消息. 在这里, 不考虑 缓冲区的容量. 所考虑系统的示意图如下: 166 模型检验原理 在下面的 LTL 描述中, 使用原子命题 m 2 S.out 和 m 2 R.in, 其中 m 是任意消息. 利用 LTL 公式将下列非形式化要求形式化: . 只要消息 m 在 S 的输出缓冲区中, m 终将被接收器用掉. 该要求可公式化为 □(m 2 S.out ! .(m 2 R.in)) 路径 s1s2s3 也满足上述性质, 其中 s1 j= m 2 S.out, s2 j= m /2 S.out, s2 j= m /2 R.in, 且 s3 j= m 2 R.in. 然而, 这样的路径表示一种诡异的行为, 即 S 的输出缓冲 区中的消息 m (状态 s1) 丢失 (状态 s2) 后, 仍到达 R 的输入缓冲区 (状态 s3). 事 实上, 如果可靠 FIFO 通道满足以下 (更强的) 条件, 则这样的行为就是不可能的: □(m 2 S.out ! (m 2 S.out U m 2 R.in)) 该条件说明: 直到接收器 R 用掉 m, 消息 m 一直停留在 S.out 中. 因为在一个 FIFO 通道中, 读和写不能同时发生, 所以可以将该要求公式化为 □(m 2 S.out ! (m 2 S.out U m 2 R.in)) . 如果假设没有消息在 S.out 中出现两次, 那么 FIFO 通道的异步行为能确保性质 “消息不能同时出现在两个缓冲区中” 成立. 该要求可公式化为 □:(m 2 S.out ^ m 2 R.in) . FIFO 通道的特点是: 根据先进先出的原则, 它们是保序的. 即, 如果 S 先把消息 m 送入其输出缓冲区 S.out, 然后送入 m′, 则 R 将会在 m′ 之前收到 m. 该要求可公 式化为 □m 2 S.out ^ :m′ 2 S.out ^ .(m′ 2 S.out) ! .(m 2 R.in ^ :m′ 2 R.in ^ .(m′ 2 R.in)) 注意, 为确保在 m 之后把 m′ 放入 S.out, 前提中需要 :m′ 2 S.out. 仅有 .(m′ 2 S.out), 则不能排除当 m 进入 S.out 时 m′ 已在发送缓冲区中的情形. 以上公式针对的是固定消息 m 和 m′. 为使上述性质能够针对所有消息, 要在所有消 息 m 和 m′ 上使用合取. 只要消息的字母是有限的, 就可以获得一个 LTL 公式. ■ 例 5.8 动态领袖选举 (本例取自文献 [69].) 在当前的分布式系统中, 一些服务是由专用进程提供的, 例如地 址的分配和登记、分布式数据库系统中的查询协调、时钟分布、令牌环网中令牌丢失后的 再生、移动网络中拓扑更新后的初始化、负载平衡等. 系统中的许多进程通常都有提供这 些服务的潜在可能. 然而, 为了确保相容性, 通常情况下, 任何时候都只允许一个进程实际 提供指定的服务, 这个进程 (称为领袖) 实际上是选出的. 有时随便选个进程就可以了; 但 是对于其他服务, 选出最有能力完成服务的进程是非常重要的. 在这里, 撇开特定能力, 并 使用以进程 ID 为基础的排序, 意思是: 进程的 ID 越大, 它的能力越强. 假设以某种通信手段连接起来的进程的个数是一个有限数 N > 0. 像前面的例子一样, 进程之间的通信是异步的. 用图形描述为