Petri net reachability analysis meets model-based diagnostic problem solving

The present paper describes the formal connection between model-based diagnostic problem solving (usually performed inside logical frameworks) and Petri net reachability analysis, in case the model of the device under examination is described through a net model. We show that, by suitably re-formulating a diagnostic problem in a net-based setting, the characterisation of the diagnostic process can be obtained in terms of reachability of a given marking, representing the current observed parameters of the system to be diagnosed, from a particular marking representing the diagnosis. Reachability graph and P-invariant analysis can then be suitably used to perform diagnostic problem solving. A system called INVADS, implementing the invariant-based approach to diagnosis, is then briefly described