Eventual strong detectability of labeled weighted automata over monoids. Issue 28 (2022)

• Record Type: Journal Article
• Authors: Zhang, Tianchen; Zhang, Kuize
• Is Part Of: IFAC-PapersOnLine. Volume 55:Issue 28(2022)
• Page Start: 270
• Page End: 275
• Publication Date: 2022
• Subjects: labeled weighted automaton over monoid -- discrete-event system -- labeled finite-state automaton -- eventual strong detectability -- verification -- complexity; Automatic control -- Periodicals; 629.805
• DOI: 10.1016/j.ifacol.2022.10.353
• Languages: English
• ISSNs: 2405-8963

Abstract

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 A m ), and use the notion of concurrent composition also proposed by the second author to give a necessary and sufficient condition for ESD of A m, where in an A m, 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 A Q n over the monoid (Q n, +) is coNP-complete, where the coNP-hardness even holds for automaton A N over the monoid (N, +). These results extend our previous result on polynomial-time ESD verification in labeled finite-state automata.