状态机

状态应是对未来行为充分的历史摘要：一旦当前状态和后续输入相同，模型允许的未来不应再依赖已被状态遗忘的历史。无标签关系适合只研究可达性和轨迹；动作标签说明“哪一步发生了”；输入输出函数则同时保留外部调用与可观察结果。确定性表示同一状态和命令给出唯一后继与输出，非确定性则保留多种允许演化，用来表示环境、调度、随机选择或抽象尚未决定的细节。

若只观察是否占用，互斥锁可有 unlocked 与 locked 两个状态；若还要检查释放者合法性，就须细化成 owned(P)、owned(Q) 等状态。历史“P 获锁”与“Q 获锁”都投影成 locked，但下一步 unlock(P) 在两者中的合法性不同。这个具体差别说明：状态是否充分，取决于要保留的操作接口，不能只看图是否简洁。

计数器状态为整数 $n$，可定义 $\delta (n,\mathtt{inc})=(n+1,\mathtt{ok})$，以及 $\delta (n,\mathtt{read})=(n,n)$；若还需限制溢出，位宽必须纳入状态。协议若只记录“当前 leader”却不记录任期，会把来自不同历史的同名 leader 合并，无法判断旧消息是否合法。有限状态机可穷举可达图；无限状态机通常需归纳不变量或有限抽象。并非每条执行都必须无限：终止程序产生有限最大执行，持续服务则通常研究无限执行。

状态集合理路集合Set由成员完全决定的数学对象；成员关系给出集合的内容，额外结构须另行指定。与转移关系理路关系Relation · Binary relation带源集与目标集的二元关系，其底层关系图是 A×B 的子集。给出最一般的无标号状态机骨架，动作和输入输出再按观察需求逐层加入。轨迹与路径语义理路轨迹与路径语义Trace semantics · Path semantics · Execution traces以状态路径和可观察动作轨迹描述有限、无限与最大行为，并说明投影和隐藏会遗忘什么。从最大执行提取可观察行为；若还要解释状态命题，可在其上建立Kripke 结构理路Kripke 结构Kripke structure · Kripke transition structure以状态转移和原子命题标记解释分支时间性质的状态模型。。这些语义对象支撑模型检查理路模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。与安全—活性理路安全性与活性Safety and liveness · Correctness properties把系统正确性分为坏事永不发生与好事最终发生两类性质。证明：安全性常归约为所有可达状态都满足某个归纳不变式理路不变式与归纳不变式Invariant · Inductive invariant · Strengthened invariant区分所有可达状态上成立的性质与由初始性和一步闭包直接证明的归纳不变式。。

状态机复制理路状态机复制State machine replication · SMR让多个副本按同一确定顺序执行命令，从而实现容错服务。让多个副本按同一命令序列运行，要求输入输出转移确定。若命令处理过程中直接读取各自墙钟，即使命令序列相同，副本也可能写入不同时间戳；应把约定的时间值作为共同命令输入，或明确采用能协调非确定性的复制机制。分布式系统则把局部状态机与信道状态组合成全局状态机。

算法序列也可产生状态转移，但评价目标不同。在线算法理路在线算法模型Online algorithm model输入逐步揭示，算法必须在未知未来时作出通常不可撤回的决策。在请求到达后立刻选择动作并与离线最优比较，动态数据结构则按 update/query 操作序列报告成本；追溯数据结构理路追溯数据结构retroactive data structure · retroactivity允许在操作时间线的过去插入或删除更新，并重新解释其后状态的数据结构模型。甚至允许编辑过去操作并重算其后的逻辑历史。这里的状态机提供语义骨架，不替代它们的竞争比、更新界或历史编辑接口。