CBPNs: coloured behavioural petri nets for model-based diagnosis

During the last two decades, Petri Nets (PNs) are used extensively in model-based diagnosis. However, the net model becomes fairly complex when dealing with large systems; since each instance of a system variable is modelled by a corresponding place. This is due to the fact that there is only one type of tokens. Consequently, Coloured Petri Nets (CPNs) appear as more suited in this task. This paper presents a causal model-based diagnosis framework based on CPNs. It introduces a particular net model called Coloured Behavioural Petri Net (CBPN) to represent behavioural causal models. In such a net model, functional dependencies are described by means of matrices attached to transitions. The reason for such an attachment is to facilitate the net model analysis on which the diagnosis process will be accomplished. We show how the diagnostic problem can be formalized in terms of reachability in a CBPN. We introduce the CW-analysis as a backward analysis on reachability graph, then we show how it can be exploited to solve a given CBPN diagnostic problem. Finally, a transformation procedure to fold a behavioural Petri net model to an equivalent CBPN one is described.