A remark on diagnosability verification
For researchers in discrete event systems, this work corrects critical errors in a widely-cited verification algorithm, showing that the problem is harder than previously claimed.
The paper identifies three inaccuracies in a prior algorithm for verifying diagnosability and co-diagnosability of discrete event systems: the algorithm incorrectly assumes deadlock-free and divergence-free conditions, a proposed fix using unobservable self-loops can alter diagnosability, and the claim of polynomial-time complexity is false because the problem is PSPACE-hard.
We point out three inaccuracies in paper [M.V. Moreira, T.C. Jesus, and J.C. Basilio. Polynomial time verification of decentralized diagnosability of discrete event systems. IEEE Transactions on Automatic Control, 56(7):1679-1684, July 2011]. First, the authors wrongly claimed that their algorithm for verifying (co-)diagnosability of labeled finite-state automata (LFSAs) did not depend on assumptions. We give an LFSA that is not deadlock-free or divergence-free such that their algorithm cannot correctly verify its diagnosability. Because diagnosability is a special case of co-diagnosability, their algorithm cannot correctly verify co-diagnosability either when LFSAs are not deadlock-free or divergence-free. Second, they wrongly claimed that adding at each dead state an unobservable self-loop can help verifying diagnosability for an LFSA that is not deadlock-free or divergence-free, but this is wrong, because such a modification sometimes changes the diagnosability of an LFSA. Third, they wrongly claimed that their algorithm for verifying co-diagnosability ran in polynomial time. A polynomial-time algorithm unlikely exists, because the problem of verifying co-diagnosability of LFSAs is PSPACE-hard.