标题：Detectability of Nondeterministic Finite Transition Systems * * This work was supported in part by the German Research Foundation (DFG) through the grant ZA 873/1-1.
摘要：AbstractNondeterministic finite transition systems (NFTSs) have been widely used in the past decade to (approximately) abstract physical systems described by ordinary differential equations. One can leverage the NFTSs and algorithmic machinery for automated synthesis of finite systems to automatically synthesize controllers for the original physical systems against complex logical specifications. The current state detection/estimation of NFTSs is of fundamental importance, as the current state is often used inside the synthesized controllers to compute the current input value for the concrete physical systems. In this paper, the problem of detectability is formulated as whether one can determine the current and all subsequent states of the NFTSs considered by using any sufficiently long input sequence and the corresponding output sequence. We design a polynomial time algorithm to verify the detectability, and based on the algorithm, we design a detector, i.e., a partial function that maps the set of (input, output) sequences of a specific length to the set of states, to determine the current and all subsequent states of detectable NFTSs.
