Abstract
In this paper, we characterize diagnosability for a labeled weighted automaton {{\mathcal{A}}^{{\mathbb{Q}} \geq 0}} over the monoid (ℚ ⩾0 ,+,0). By developing a notion of concurrent composition, under a mild assumption that no observable transition is instantaneous, we prove that diagnosability of automaton {{\mathcal{A}}^{{\mathbb{Q}} \geq 0}} can be verified in coNP. On the other hand, we prove that the problem of verifying diagnosability of a deterministic, deadlock-free automaton {{\mathcal{A}}^{{{\mathbb{N}}_0}}} is coNP-hard, where {{\mathcal{A}}^{{{\mathbb{N}}_0}}} denotes a labeled weighted automaton over the monoid (ℕ 0 ,+,0).