Abstract
Detectability is a basic property that describes whether an observer can use the current and past values of an observed output sequence produced by a system to reconstruct its current state. We consider particular properties called instant strong detectability and instant 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. Copyright (C) 2020 The Authors.