形式陈述

状态机可写成 $(S,I,\to)$$(S,I,\to )$，其中 $S$$S$ 是状态集，$I\subseteq S$$I\subseteq S$ 是初始状态集，$\to\subseteq S\times S$$\to \subseteq S\times S$ 是转移关系。执行是序列 $s_0,s_1,\ldots$$s_0,s_1,\dots$，满足 $s_0\in I$$s_0\in I$ 且每步 $s_i\to s_{i+1}$$s_i\to s_{i+1}$。

直觉

状态概括对未来行为有影响的全部历史；转移描述一次允许的原子变化。并发系统可通过交错或偏序组合多个局部状态机。

例子与边界

互斥锁可有 unlocked 与 locked 状态。若遗漏影响未来的隐藏信息，所选“状态”就不充分，模型可能错误地合并不同执行历史。

推论与应用

安全性、活性、共识协议、模型检查和状态机复制都以转移系统表示行为。

参考资料

• Nancy A. Lynch, Distributed Algorithms, Chapter 8.
• Leslie Lamport, Specifying Systems, Chapters 1–2.