精读笔记

Problem Setting

论文标题：A remark on diagnosability verification（arXiv preprint / 2026-06-09）。

这篇文章处理的是 LFSA 中 diagnosability / co-diagnosability verification 的“前提条件是否可去除”问题。它不是在提出一个更快 verifier，而是在指出一个被引用的 polynomial-time decentralized diagnosability verification 结果在三个层面上站不住：正确性前提、deadlock 处理、复杂性 claim。

真正困难点在于 diagnosability 的反例本质上是关于“故障后是否存在任意长、观测不可区分的非故障行为”的问题。Yoo-Lafortune 类型 verifier 通过 product / parallel composition 把这种不可区分性转成 cycle detection；但 cycle detection 只有在系统不会提前 deadlock、也不会在不可观测事件上无限打转时才与原语义吻合。否则 verifier 看到的 cycle 未必对应定义中需要的无限可延展 ambiguous behavior。

以前方法卡住的位置不是图搜索本身，而是图结构和诊断语义之间的 adequacy：parallel composition 默认把同步/异步可延展性当作无害，但 deadlock 和 unobservable divergence 正好破坏了这种对应关系。关键矛盾是：为了得到 polynomial-time cycle check，需要把语言语义压缩成有限图上的环；但这种压缩依赖 liveness 和 divergence-freeness，否则图上的环可能是 verification artifact。

Motivation

作者瞄准的是 Moreira et al. 2011 中三个过强表述。第一，原文声称移除了 liveness 和 absence of unobservable cycles 的假设；第二，原文认为可以 WLOG 给 deadlock state 加不可观测 self-loop 使系统 live；第三，原文把 decentralized co-diagnosability verification 称为 polynomial-time。

核心观察是：这些 claim 都不是小的技术疏漏，而是触及 verifier 方法成立的语义基础。若一个 verifier 源自 Yoo-Lafortune 的 construction，那么它的 cycle criterion 不是自由成立的；它需要系统行为可以无限延展且不会被不可观测内部循环污染。缺口在于 Moreira et al. 把不同文献中的 co-diagnosability 定义混在一起使用：[2][3] 对 terminating traces 的处理更强，允许某种 completion 不改变其定义；但 [1] 采用的是 Sampath-style diagnosability 的直接扩展，不能自动继承这种 WLOG 变换。

所以这篇 note 的动机不是“改进算法”，而是把隐藏在 verification construction 后面的 semantic assumptions 拉回台面。

Core Idea

核心思想很直接：用最小反例证明 parallel-composition verifier 的 cycle condition 在 arbitrary LFSA 上不是 diagnosability 的充要条件。作者构造的 LFSA 同时包含一个 dead state 和一个不可观测自环。按 [1] 的 Def. 1，该系统是 {f}-diagnosable；但按照 [1] 的 GN/GF construction，其 GN || GF 中存在满足条件 C 的 reachable cycle，于是 verifier 会错误给出 non-diagnosable。由于 diagnosability 是 co-diagnosability 在 m=1 时的特例，这个反例也直接否定了 decentralized algorithm 的无前提正确性。

这改变的不是建模能力，而是对已有建模方式的边界刻画：parallel composition 并不天然表达“存在一对无限、观测等价、一个含故障一个不含故障的轨迹”。它只是在特定假设下把这个二阶语言性质降成图上环性质。若 deadlock 或 unobservable divergence 存在，图上的环可能来自构造中的非语义同步，而不是来自真正的不可诊断行为。

与 prior 的本质区别在于，Zhang 主张 arbitrary LFSA 上需要 concurrent-composition-style 方法来验证强 detectability / diagnosability 的否定，而不是沿用依赖 liveness/divergence-freeness 的 verifier 再声称无前提。

Method

1. 反例攻击 assumption-free claim：作者使用一个三状态 LFSA，其中 x1 是 dead state，x2 有不可观测 u-self-loop，fault f 与 u 都标记为空观测。该系统在 [1] 的定义下仍是 diagnosable，但 [1] verifier 的 GN || GF 产生含 F-component 的 reachable cycle，触发 non-diagnosability 判据。这一步解决的是“算法是否真的无前提正确”的问题，核心变化是把抽象前提争论转成单 agent 的可检查失败。

2. 反驳 deadlock completion 的 WLOG：若在 dead state x1 上添加不可观测 u 自环，新系统变成 non-diagnosable。原因是原本终止的 fault behavior 被人为延展成无限不可观测 behavior，从而改变了 diagnosability 的量词结构。这一步说明 completion 不是 harmless preprocessing，而是改变 specification。

3. 区分不同 co-diagnosability 定义：文中指出 [2][3] 的定义直接把 deadlocking terminating trace 纳入 diagnosable 条件，因此在那些定义下加 self-loop 可能不改变性质；但 [1] 的定义不同，不能借用这个处理。这一步是在解决“为何其他文献看似允许该操作”的概念混淆。

4. 复杂性反驳：文中引用 co-diagnosability verification 在 deadlock-free 和 divergence-free LFSA 上已 PSPACE-hard，因此若 [1] 的一般 decentralized co-diagnosability verifier 真是 polynomial-time，除非 P=PSPACE，否则不可能成立。这一步不依赖具体反例，而是从复杂性上否定 claim 的可置信度。

Key Insight / Why It Works

这篇 note 最重要的 insight 是：diagnosability verifier 的 cycle criterion 不是纯图论事实，而是语义-图论 correspondence；deadlock-freeness 和 divergence-freeness 正是保证 correspondence 的桥。没有这些桥，cycle detection 会过近似 non-diagnosability。

为什么反例有效？因为它击中 verifier 的脆弱点：fault branch 可以在 dead state 停止，non-fault branch 可以通过不可观测循环继续，parallel composition 会组合出一个看似可无限维持 ambiguity 的结构。但 diagnosability 定义中对故障后延展性的要求并不等价于这个构造里的环。换言之，verifier 把“构造图中存在 F-component cycle”误读成“原系统存在不可诊断的无限行为”。在非 live / 有不可观测 divergence 的系统中，这个推理断裂。

最核心贡献是语义纠偏，而不是新算法。加 self-loop 的讨论同样关键：很多 DES verification 工具会把 deadlock completion 当作工程预处理，但这里说明该预处理对 diagnosability 不是语义透明的。它可能把 finite trace 的诊断问题变成 infinite trace 的诊断问题，从而直接改变性质。

复杂性部分的判断也很硬：如果 co-diagnosability 已在更受限模型上 PSPACE-hard，那么所谓 polynomial-time 一般算法基本只能来自两个可能：要么问题定义不同，要么算法不正确/复杂度计算错误。这里更像后者。不存在什么 scaling 或 engineering 增益；这篇文章的价值完全来自形式语义和复杂性边界的校准。

Relation To Prior Work

最接近的路线是 Sampath et al. 的 diagnosability 定义、Yoo-Lafortune 的 polynomial-time diagnosability verifier，以及 Moreira et al. 对 decentralized co-diagnosability 的扩展。Zhang 的 note 不是替代这些路线，而是指出其中某个扩展版本错误继承了前提。

与 Yoo-Lafortune verifier 的关系：Yoo-Lafortune 方法在 deadlock-free 和 divergence-free 假设下用 verifier/product construction 做 polynomial-time 判定；这些假设是方法正确性的组成部分，不是可选工程条件。Moreira et al. 的错误在于把该 construction 扩到 decentralized setting 后声称移除这些假设。

与 Qiu-Kumar、Wang-Yoo-Lafortune 的关系：这些工作的 co-diagnosability notion 与 Moreira et al. 使用的 notion 不同，尤其对 deadlocking terminating traces 的处理不同。因此不能用它们的定义来支持 [1] 中的 WLOG liveness assumption。

与 Zhang 自己的 concurrent composition 系列工作的关系：这篇 note 明显站在后者谱系上，即 arbitrary LFSA 的 state/event inference、detectability、diagnosability 需要更精细的 concurrent-composition construction 来表达性质否定，而不是依赖 classical parallel verifier。实质新增信息是：用一个极小 LFSA 把旧 verifier 的失败机制具体化，并把它和 PSPACE-hardness claim 对齐。

Dataset / Evaluation

没有 dataset，也没有实验 evaluation；这是合理的，因为论文性质是 formal remark / correction。核心 claim 不需要 benchmark 支撑，而需要反例和复杂性证据。

评价覆盖范围很窄但命中要害：反例只覆盖单 agent diagnosability，却足以否定 decentralized co-diagnosability verifier 的无前提正确性，因为 m=1 是其特例。复杂性引用覆盖更强：即使限制在 deadlock-free、divergence-free LFSA，co-diagnosability verification 仍 PSPACE-hard，因此 polynomial-time claim 不可能通过更多工程优化来修复。

文中未充分说明的是：对于多 agent 情况，Moreira et al. 未明确定义的 GN,1 || GN,2 || GF 若存在其他解释，是否所有解释都失败。作者没有系统穷尽这些解释。但这不削弱主要结论，因为单 agent 反例已经足够。

Limitation

这篇文章的限制在于它是 correction note，不是完整理论重构。它没有给出 arbitrary LFSA co-diagnosability verification 的完整算法描述，只指向已有 concurrent-composition 方法。若读者期待可直接替换 [1] verifier 的完整 construction，这里信息不够。

第二，反例依赖同时出现 deadlock 与 unobservable cycle。它强力说明“不能无前提”，但没有细分只有 deadlock、只有 divergence、或不同 fault/event labeling 下 verifier 失败的完整边界。哪些最小条件足以恢复 correctness，文中未充分说明。

第三，对复杂度的讨论是下界式反驳，不是 tight characterization。它说明 polynomial-time unlikely，但没有给出在不同 agent 数、观测投影结构、fault classes 固定时的参数化复杂性。

第四，文章对 [1] 中算法复杂度为何被误算没有展开。是 product construction 的状态空间指数依赖 agent 数，还是 co-diagnosability 本身的 quantifier structure 导致 PSPACE-hard，文中只给出结论性判断。对熟悉复杂性的人足够，但作为纠错文仍略短。

Takeaway

• 1. Diagnosability verifier 的正确性不能只看 product graph 是否有 cycle；必须先确认该 cycle 与原系统的无限 ambiguous behavior 语义等价。
• deadlock-freeness 和 divergence-freeness不是装饰性假设。
• 2. 给 dead state 加不可观测 self-loop 不是普适 WLOG。
• 它在某些把 terminating trace 特判为 diagnosable 的定义下可能安全，但在 Sampath-style diagnosability 及其直接 decentralized extension 下会改变性质。

一句话总结

这篇 note 在 diagnosability verification 文献中的位置是一次精准纠错：它说明 Moreira et al. 的 polynomial-time decentralized verifier 并未真正摆脱 liveness/divergence-freeness 假设，deadlock completion 会改变诊断语义，而一般 co-diagnosability verification 的复杂性也不支持 polynomial-time claim。