In this paper, emph{diagnosability} is characterized for a labeled max-plus automaton $mathcal{A}^{mathcal{D}}$ over a dioid $mathcal{D}$ as a real-time system. In order to represent time elapsing, a special class of dioids called emph{progressive} are considered, in which there is a total canonical order, there is at least one element greater than $textbf{1}$, the product of sufficiently many elements greater than $textbf{1}$ is arbitrarily large, and the cancellative law is satisfied. Then a notion of diagnosability is formulated for $mathcal{A}^{mathcal{D}}$ over a progressive dioid $mathcal{D}$. By developing a notion of emph{concurrent composition}, a sufficient and necessary condition is given for diagnosability of automaton $mathcal{A}^{mathcal{D}}$. It is also proven that the problem of verifying diagnosability of $mathcal{A}^{underline{mathbb{Q}}}$ is coNP-complete, where coNP-hardness even holds for deterministic, deadlock-free, and divergence-free $mathcal{A}^{underline{mathbb{N}}}$, where $underline{mathbb{Q}}$ and $underline{mathbb{N}}$ are the max-plus dioids having elements in $mathbb{Q}cup{-infty}$ and $mathbb{N}cup{-infty}$, respectively.
Download