反例与见证轨迹

证书相对于查询方向 ​

在模型检查公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。中，反例是证明全称性质失败的模型行为，witness 是证明存在性性质成立的行为。二者都必须由模型初态出发、逐步满足转移，并在逻辑语义下交付目标结论。

对安全公式 $AG\mathrm{\neg }bad$，反例是有限路径

前缀到达坏状态后，任何后缀都不能撤销违反。父指针即可重建这类证书。

对存在性 $EFgoal$，同一形状的路径是正向 witness。不能脱离公式把一条路径固定称为“反例”：它扮演的角色取决于被证实或否定的量词。

活性 lasso ​

无限路径无法完整打印。有限状态模型中的活性反例通常表示为 lasso

即有限 stem 加可重复 cycle。若规格为 $G(request\to Fgrant)$，cycle 可包含一个未兑现请求并永远不出现 grant。

循环首尾状态相同确保它能无限重复；只展示一段很长但不闭合的无响应前缀，仍可能在下一步授权，不能证明 liveness 失败。

带 Büchi 或公平条件时，cycle 还必须满足相应接受集合访问要求。任意图环不一定是合法反例。

一条互斥诊断轨迹 ​

两个进程初始都在 N，错误协议允许分别执行 check-free 后再无原子地写锁。反例可为：

(N,N,free)
--p1:check-free--> (T,N,free)
--p2:check-free--> (T,T,free)
--p1:enter-->      (C,T,p1)
--p2:enter-->      (C,C,p2)

每一步同时展示动作与关键状态变量，末状态满足双临界坏谓词。若只列动作名而隐藏 free 的读取结果，就难以看出竞态；若打印全部堆内存，又可能淹没因果链。

最短反例按转移数最少，不一定最有解释力。工具可做 cone-of-influence、变量切片或 trace minimization，但缩减后仍须保留一条可重放的合法路径。

CTL 见证不总是一条线 ​

$EFp$ 的见证是一条到 $p$ 的路径，$EGp$ 的见证是进入全 $p$ 循环的 lasso。然而 $AG(EFreset)$ 的完整证明要为每个可达状态提供某条恢复分支，天然更像子图或树，而不是单条路径。

同样，反驳 $A[\phi U\psi ]$ 可以用一条坏路径，证明它却要覆盖全部分支。工具输出单条样例成功执行，不能作为全称 CTL 公式的证明证书。

模型诊断不是根因证明 ​

反例证明模型违反规格，并给出一个行为见证。它不自动说明哪一行代码是根因，也不判断规格、环境假设或抽象是否错误。

抽象模型中的路径可能是 spurious：每一步抽象转移都存在，却没有一个一致具体执行实现整条路径。需要可行性检查把抽象状态约束沿路径合取，再决定是报告真实错误还是精化抽象。

反例也可能依赖模型人工边界，例如队列溢出状态。报告必须包含配置、边界与公平假设，否则读者无法判断能否在目标实现中复现。

证书检查接口 ​

可检查的安全路径至少含初态证明、每步转移输入和末端性质求值。SAT-based 工具可附模型赋值，PDR 可附归纳不变式；证明对象越独立，可信计算基越小。

隐私或状态巨大时可以投影输出，但内部验证仍需对完整状态确认合法性。把日志中看似相邻的事件拼成路径，若缺少隐藏状态连续性，不构成形式证书。

同一个性质可能有多条反例，搜索顺序决定首先返回哪条。按长度最短、按输入变化最少、按因果切片最小是不同优化目标，彼此不保证一致。工具若进行 trace reduction，应在缩减后重新执行每个 guard 和 update；仅删除“看起来无关”的步骤可能让后续状态不再可达，得到一份易读却无效的故事。

对于非确定环境，反例中的环境选择是见证的一部分。若部署假设禁止该输入或故障模式，应修改并验证环境模型，而不是从输出中手工删掉该分支。

反例重放还应固定初始状态、随机种子或调度决策；否则同一外部输入在非确定模型中可能走向另一条合法路径。可复现性是诊断质量，不替代原始路径的形式合法性检查。