Verification of fault-predictability in labeled petri nets using predictor graphs

A fault-predictable discrete event system (DES) is a system where any fault can be correctly predicted before its occurrence. This paper studies the verification of fault-predictability in bounded and unbounded DESs modeled by labeled Petri nets (PNs). An approach based on the construction of a Predictor Net and a Predictor Graph (PG) is proposed. In particular, a necessary and sufficient condition for fault-predictability is derived by characterizing the structure of the PG. Furthermore, two rules are proposed to reduce the size of a given PN, which allows one to analyze the fault-predictability of the original net by verifying the fault-predictability of the reduced net.