状态机

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

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

计数器状态为整数 $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允许在操作时间线的过去插入或删除更新，并重新解释其后状态的数据结构模型。甚至允许编辑过去操作并重算其后的逻辑历史。这里的状态机提供语义骨架，不替代它们的竞争比、更新界或历史编辑接口。