  Among notions of detectability for a discrete-event system (DES), strong
detectability implies that after a finite number of observations to every
output/label sequence generated by the DES, the current state can be uniquely
determined. This notion is strong so that by using it the current state can be
easily determined. In order to keep the advantage of strong detectability and
weaken its disadvantage, we can additionally take some "subsequent outputs"
into account in order to determine the current state. Such a modified
observation will make some DES that is not strongly detectable become "strongly
detectable in a weaker sense", which we call "{\it $K$-delayed strong
detectability}" if we observe at least $K$ outputs after the time at which the
state need to be determined. In this paper, we study $K$-delayed strong
detectability for DESs modeled by finite-state automata (FSAs), and give a
polynomial-time verification algorithm by using a novel concurrent-composition
method. Note that the algorithm applies to all FSAs. Also by the method, an
upper bound for $K$ has been found, and we also obtain polynomial-time
verification algorithms for $(k_1,k_2)$-detectability and
$(k_1,k_2)$-D-detectability of FSAs firstly studied by [Shu and Lin, 2013]. Our
algorithms run in quartic polynomial time and apply to all FSAs, are more
effective than the sextic polynomial-time verification algorithms given by [Shu
and Lin 2013] based on the usual assumptions of deadlock-freeness and having no
unobservable reachable cycle. Finally, we obtain polynomial-time synthesis
algorithms for enforcing delayed strong detectability, which are more effective
than the exponential-time synthesis algorithms in the supervisory control
framework in the literature.
