IEEE Transactions on Automatic Control, Vol.64, No.10, 4353-4360, 2019
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.