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.

Automated summary

This article discusses the detectability problem for unambiguous weighted automata (UWAs), introducing four types of detectabilities and proposing necessary and sufficient conditions for verifying the detectabilities of a UWA based on an observer constructed over a weighted alphabet.