Unfold and Cover: Qualitative Diagnosability for Petri Nets

International audienceIn recent years, classical discrete event fault diagnosis techniques have been extended to Petri net system models under partial order semantics. We propose here to take further advantage of the partial order representation of concurrent processes; we explore the relational structure of occurrence nets to derive a covering relation. It indicates that occurrence of some event a inevitable leads to occurrence of some event b, before a, after a, or concurrently. Covering defines a decomposition of occurrence nets into facets; we introduce the facet-based concept of q-diagnosability --for qualitative diagnosability as opposed to quantitative criteria-- which is specific to partial order semantics. All objects considered can be computed from a finite unfolding prefix of bounded length