A semi-symbolic diagnoser for fault diagnosis of bounded labeled petri nets

In this paper, we present a diagnoser-based approach to deal with fault diagnosis of bounded labeled Petri nets. The approach consists in building a semi-symbolic diagnoser to analyze diagnosability and perform online diagnosis. The contribution of this paper is twofold: (i) from the theoretical point of view, we provide new conditions for checking diagnosability based on a novel diagnoser variant that explicitly separates the normal reachable markings from the faulty ones, in each diagnoser node. This allows us to independently keep tracking the normal and the faulty diagnoser paths more efficiently. (ii) From the practical point of view and in order to reduce the memory required to build the diagnoser efficiently, we establish a semi-symbolic encoding of the diagnoser state-space. Such a representation deploys a symbolic encoding of the diagnoser nodes content, using Binary Decision Diagrams, while it keeps an explicit encoding of the observable transitions between the nodes. In addition, we provide an on-the-fly algorithm to simultaneously construct the diagnoser and analyze diagnosability. The effectiveness of the approach is illustrated through some experimentation performed on a Petri net benchmark.