Predictability Verification of Fault Patterns in Labeled Petri Nets

This article focuses on the predictability verification problem of fault patterns for both bounded and unbounded discrete event systems modeled with labeled Petri nets. A system is said to be predictable with respect to a fault pattern if any complete fault behavior in a fault pattern can be correctly predicted before its occurrence, where the fault patterns are characterized by a particular composition of a labeled Petri net with a fault pattern net. In this article, we construct a fault pattern predictor net and a basis fault pattern predictor graph (PG) that is based on the notion of basis markings. By exploiting the fault pattern predictor net and basis fault pattern PG, we derive a necessary and sufficient condition to check fault pattern predictability, which does not need the full reachability/coverability graph of a net, thus gaining practical computation benefits.