  Detectability describes the property of an system whose current and the
subsequent states can be uniquely determined after a finite number of
observations. In this paper, we relax detectability to C-detectability that
only requires a given set of crucial states can be distinguished from other
states. Four types of C-detectability: strong C-detectability, weak
C-detectability, periodically strong C-detectability, and periodically weak
C-detectability are defined in the framework of labeled Petri nets, which have
larger modeling power than finite automata. Moreover, based on the notion of
basis markings, the approaches are developed to verify the four C-detectability
of a bounded labeled Petri net system. Without computing the whole reachability
space and without enumerating all the markings consistent with an observation,
the proposed approaches are more efficient.
