2.7 随机化

我们不要求进程是确定性的，有时候，允许它们基于某一给定的概率分布进行随机选择也是很有用的。由于基本的同步网络系统模型不允许这一点，我们对其进行扩展，即除了消息生成函数和状态迁移函数之外，又引进一个随机函数来表示随机选择步骤。用形式化描述就是在每一节点i的自动机描述中增加一个rand_i部分；对于每个状态s，rand_i(s)是states_i的某个子集上的一个概率分布。现在，在每轮运行中，首先用随机函数rand_i选出新的状态，然后按常规应用msgs_i和trans_i函数。

在随机化算法中，运行的形式化描述不仅包括状态赋值和消息赋值，还包括关于随机函数的信息。特别地，系统的一次运行被定义为一个无界序列：

C ₀,D₁,M₁,N₁,C₁,D₂,M₂,N₂,C₂,…

其中，C_r和D_r是状态赋值，M_r和N_r是消息赋值。D_r表示第r轮随机选择后进程的新状态。

对随机系统计算内容的声明通常是概率化的，断言某些结果至少有一定的出现概率。当做出这样的声明时，一般认为它对所有输入和所有故障模式（如果系统存在故障）都成立。为了对输入和故障模式建模，通常假设一个称为“对手”的假想实体控制输入的选择和故障的发生，那么概率性声明断言系统在与任意合法对手的竞争中表现良好。对这些情况的处理超出了本书的范围，我们只在需要时提供特殊情况定义。