五种形式化

父页面：stages-and-gates

同一个骨架，五种透镜：

1. 自动机 / 识别器 —— 阶段（stage）= 状态，关口（gate）= 带守卫条件的转移（当且仅当判据 g 成立时 advance 才被启用）。这台机器识别出通过每一个关口的轨迹，而不生成它们 → recognizer-not-generator。
2. 霍尔逻辑 / 证明义务（最深刻的一种） —— {P} S₁ {Q}; {Q} S₂ {R}。中间断言 Q 就是关口：owner 写下断言，agent 提供一个满足该三元组的执行。关口 = 一项证明义务；阶段 = 那个（可能是神经网络式的）战术 → lcf-for-labor。
3. 选项 / 分层强化学习（Sutton） —— 一个选项（option） ⟨I, π, β⟩：起始集 I、内部策略 π（自由执行）、终止条件 β = 关口。一个阶段就是一个选项；分层强化学习（HRL）= 阶段套阶段（递归）。
4. 监督控制（Ramadge–Wonham） —— 关口会禁用可控的 advance，直到完成事件被观测到为止：在亮绿灯之前，commit 不可达。是否决，不是命令 → ramadge-wonham-supervisory-control。
5. 实物期权 / 分阶段融资 —— 层层加码的承诺 = 一个复合期权；每个关口买到的是资助下一阶段的权利（而非义务）。把一次大赌注，变成一串可随时中止的小期权。