摘要：AbstractDetectability is a basic property that describes whether an observer can use thecurrentandpastvalues of an observed output sequence produced by a system to reconstruct itscurrentstate. We consider particular properties calledinstant strong detectabilityandinstant weak detectability,where the former implies that for each possible infinite observed output sequence each prefix of the output sequence allows reconstructing the current state, the latter implies that some infinite observed output sequence (if it exists) satisfies that each of its prefixes allows reconstructing the current state. For discrete-event systems modeled by finite-state automata, we give a linear-time verification algorithm for the former in the size of an automaton, and also give a polynomial-time verification algorithm for the latter.
