4.1.1 线性时序逻辑（LTL）：路径量化与未来算子（◇, □）

文档摘要

4.1.1 线性时序逻辑（LTL）：路径量化与未来算子（◇, □）在形式化验证的深水区里，时间不是钟表上匀速滑落的沙粒，而是系统状态演进所刻下的不可逆足迹。当我们在嵌入式控制器中调试一个航空电子系统的状态机，当我们在芯片级验证中追踪一个缓存一致性协议的每一步跃迁，当我们在分布式数据库中审计一个跨分区事务的可见性边界——我们真正追问的，从来不是“当前状态是否合法”，而是：“从现在起，是否永远不会再进入死锁？是否必然在有限步内达成共识？是否在任何可能的调度路径上，都不会发生未授权的数据泄露？” 这正是线性时序逻辑（Linear Temporal Logic, LTL）存在的根本理由：它不是对静态断言的装饰，而是对无限行为轨迹（infinite path）施加的、可计算的、可判定的逻辑约束。