你每天都在和自动机打交道——路口的红绿灯就是最朴素的一台。它只有几个固定状态，按规则循环切换，全程不需要人盯着。

上一页说自动机像一台只认规则的机器——读符号、改状态、定接受。但「机器」太模糊，数学上必须钉死成五个具体对象。这就是五元组 M = (Q, Σ, δ, q₀, F) 的来历。

中心是自动机整体，向外伸出状态集、字母表、转移函数三条主干，看它们如何拼装与依赖。

前面学过有限自动机——它能判断输入串能不能被接受。但高铁调度只说『关门→发车』，不说『3分钟内必须发车』，系统怎么知道你没晚点？

前面看到，普通自动机无法表达「30 分钟内必须响应」这类实时约束。时间自动机通过给状态挂上「时钟」、在边上加「时间守卫」来解决——下面拆开它的六元组结构。

图为「灯自动熄灭」示例：圆圈是位置，圈内写不变式，边上标「动作·守卫·时钟复位」。

时间自动机每次推进都要经过这五个环节，缺一不可。

时间自动机告诉我们「单步跑得对不对」，但模型检测真正要问的是：系统无限运行下去，是否永远满足某条性质。从有限到无限这一跨，就是Büchi自动机登场的理由。

前面看到，Büchi自动机是为处理无穷序列而设计的——状态机永远不停机。那它正式长什么样？结构上和NFA几乎一样，差异全藏在接受条件里。

看两条无穷路径：一条反复经过 q1（接受态）→接受；另一条陷入 q2 陷阱 →拒绝。

都扩展了有穷自动机，但方向正交：一个加时钟，一个加接受条件。容易误以为'升级版'，实则解决不同问题。

上一节我们认识了时间自动机和Büchi自动机，它们能精确描述系统的行为。但「描述清楚」和「保证正确」之间，还有一步关键跨越——形式化验证。

形式化验证用数学方法证明系统正确，但这「数学证明」其实是三大流派的合称。

四阶段循环流程，从左到右是执行顺序；右下回环表示验证失败后回到规约重新刻画性质。

前面我们用自动机优雅地建模系统——但真实工业系统往往是几十个模块并发、数百个时钟同时演化。模型再美，验证器一旦启动就卡死了。这就是形式化验证最出名也最难啃的硬骨头。

上页我们走完了形式化验证的整体流程，但真正实现「自动检验」的技术内核，是模型检测。它要回答两个根本问题：怎么把系统写出来，怎么把需求写出来。

模型检测的核心套路：把系统与性质都变成自动机，再看它们的乘积能否走出一条「坏路径」。

左右两栏对照：左侧 BMC 用固定深度 k 展开路径，右侧 IC3/PDR 用归纳不变量无限逼近。

两种时序逻辑因路径视角不同，表达力与检测复杂度各异，初学者极易混淆。

前面我们分别讨论了时间自动机与 LTL 模型检测，但如何把两者结合起来跑一个真实系统？M3C 正是这样一个把时间自动机网络建模与 LTL 属性验证集成在一起的检测平台。

从左到右看M3C的四级流水线：箭头表示数据如何在模块间传递，每个模块负责不同的处理阶段。

M3C 仲裁器的 UPPAAL 描述：声明、模板、组装、性质规约四件套。

urgent 通道瞬时同步、guard/assign 组合边、`-->` 与 `A[]` 规约——UPPAAL 把时间自动机网络变成可被搜索的状态图。

从模型文件到验证结论，M3C 检测流程分为六个阶段。

处理无限输入流时，Büchi自动机的接受条件与标准DFA的本质区别在于？

• ✓时钟扩展处理实时，Büchi处理持续运行
• ✓时序逻辑是提问语言，模型检测是自动答题机
• ✓状态爆炸是天花板，偏序与抽象是绕行术
• ✓M3C把建模-验证-反例做成工程闭环

先独立想 1 分钟再看参考答案，思考过程比结论更重要。