Supervision Patterns: Formal Diagnosability Checking by Petri Net Unfolding

This paper addresses the problem of checking diagnosability of supervision patterns in discrete-event systems. With a supervision pattern, it is possible to represent a complex behavior of the system, and especially a faulty behavior. As opposed to classical diagnosability analyzers that check by exploring the marking graph of the underlying net, the proposed method relies on Petri net unfoldings and thus avoids the combinatorial explosion induced by the use of marking graphs. The method is an adaptation of the twin-plant method to net unfolding: a pattern is diagnosable if the unfolding representing the twin-plant does not implicitly contain infinite sequences of events that are ambiguous.