Verification of detectability for unambiguous weighted automata

In this article, we deal with the detectability problem for unambiguous weighted automata (UWAs). The problem is to determine if, after a finite number of observations, the set of possible states is reduced to a singleton. Four types of detectabilities, namely, strong detectability, detectability, strong periodic detectability, and periodic detectability are defined in terms of different requirements for current state estimation. We first construct a deterministic finite state automaton (called observer) over a weighted alphabet and prove that it can be used as the current-state estimator of the studied UWA. Finally, necessary and sufficient conditions based on the observer are proposed to verify detectabilities of a UWA.