  Detectability of discrete event systems (DESs) is a property to determine a
priori whether the current and subsequent states can be determined based on
observations. In this paper, we investigate the verification of two
detectability properties -- strong detectability and weak detectability -- for
DESs modeled by labeled Petri nets. Strong detectability requires that we can
always determine, after a finite number of observations, the current and
subsequent markings of the system, while weak detectability requires that we
can determine, after a finite number of observations, the current and
subsequent markings for some trajectories of the system. We show that for DESs
modeled by labeled Petri nets, checking strong detectability is decidable
whereas checking weak detectability is undecidable. Our results extend the
existing studies on the verification of detectability from finite-state
automata to labeled Petri nets. As a consequence, we strengthen a result on
checking current-state opacity for labeled Petri nets.
