2.4 运行

为了推断同步网络系统的行为，我们需要对系统“运行”有一个形式化的描述。

把一个系统的状态赋值（state assignment）定义为对该系统中的每个进程分别赋值一个状态。同样地，消息赋值（message assignment）是对每个通道分别赋值一条消息（可以是空消息）。系统的运行定义为一个无限的序列：

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

其中，C_r是状态赋值，M_r和N_r是消息赋值。C_r代表r轮之后的系统状态，M_r和N_r则分别代表第r轮所发送和接收的消息（因为通道有可能丢失消息，所以它们有可能不同）。我们通常把C_r当成时刻r的状态赋值；也就是说，时刻r是指执行r轮之后的时间点。

设α和α′是一个系统的两次运行。如果在α和α′两次运行中，进程i有相同的状态序列、相同的输入消息序列和相同的输出消息序列，则称α和α′对于进程i是不可区分的（indistinguishable），记作α～iα′。如果在α和α′两次运行中，进程i直到第r轮都有相同的状态序列、相同的输入消息序列和相同的输出消息序列，则称α和α′对于进程i是r轮不可区分的。我们还可把这一结论扩展到两次运行处于两个不同同步网络系统中的情形。