On-Line Monitoring of Large Petri Net Models Under Partial Observation

We consider a Petri Net model of the plant. The observation is given by a subset of transitions whose occurrence is always and immediately sensed by a monitoring agent. Other transitions not in this subset are silent (unobservable). Classical on-line monitoring techniques, which are based on the estimation of the current state of the plant and the detection of the occurrence of undesirable events (faults), are not suitable for models of large systems due to high spatial complexity (exponential in the size of the entire model). In this paper we propose a method based on the explanation of plant observation. A legal trace minimally explains the observation if it includes all unobservable transitions whose firing is needed to enable the observed transitions. To do so, starting from an observable transition, using backward search techniques, a set of minimal explanations is derived, which are sufficient for detecting whether a fault event must have occurred for sure in the plant or not. The technique also allows production of a set of basis markings for the estimation of the current state of the plant. The set of all possible current markings can then be characterized as the unobservable reach of these basis markings. The computational complexity of the algorithm depends on the size of the largest connected subnet which includes only unobservable transitions. This allows monitoring of plants of any size in which there is no large unobservable subnet. We also illustrate the applicability of the method for the monitoring of a class of infinite state systems, unbounded Petri Nets with unobservable trap circuits, and we show how this can be useful for distributed implementations