Marking diagnosability verification in labeled Petri nets

This paper studies the marking diagnosability verification problem in labeled Petri nets. Marking diagnosability is a property implying the fact that a plant Petri net has ever reached a pre-defined set of faulty markings can be detected in a finite number of future steps. We first show that the conventional basis-reachability-graph-based methods cannot be used due to the existence of partially faulty basis markings . To overcome such a problem,...