形式陈述

分布式配置是某一时刻的全局状态，通常由每个进程局部状态、信道中的消息或共享对象状态组成。算法的一步把一个配置按某个可用动作转到下一配置；初始配置集合和转移关系共同定义状态空间。异步模型中的配置是数学快照，不要求系统能在现实中瞬时观测全部状态。

直觉

虽然每个进程只知道局部信息，分析者可以把所有局部状态和在途消息拼成一个全局节点，再研究可能的执行路径。

例子与边界

消息已发送但未接收时，它属于信道状态。两个局部状态相同的配置若在途消息不同，未来行为可能不同。崩溃标志、定时器和随机币是否纳入配置取决于模型；遗漏会破坏 Markov 或状态机描述。

推论与应用

配置图用于共识不可能性、可达性、模型检查、自稳定和协议不变量证明。

参考资料

• Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann, 1996，Chs. 1–25。
• Hagit Attiya and Jennifer Welch, Distributed Computing: Fundamentals, Simulations, and Advanced Topics, 2nd ed., Wiley, 2004，Chs. 1–18。