Abstract
Detectability is a basic property in partially-observed dynamical systems. It means whether one can use observed output sequences to determine the current and subsequent states, and provides bases for many related control problems such as state estimation and controller synthesis. Eventual strong detectability (ESD) means along every generated infinite event sequence s, one will always determine the states after some time delay depending on s. In this paper, we formulate ESD for a new model recently proposed by the second author called a labeled weighted automaton over a monoid m = (T,⊗,1) (denoted by Am), and use the notion of concurrent composition also proposed by the second author to give a necessary and sufficient condition for ESD of Am, where in an Am, each transition carries a weight in m and the weight of a run is the product of the weights of the transitions of the run. Particularly, we prove that the problem of verifying ESD of automaton AQn over the monoid (Qn,+) is coNP-complete, where the coNP-hardness even holds for automaton AN over the monoid (N,+). These results extend our previous result on polynomial-time ESD verification in labeled finite-state automata.