Necessary condition for a Petri net model that incorporates resources to produce an event stream from an unknown initial state

This paper presents conditions under which a type of Petri net model with resources, called System of Transition Processes with Resources (STPR), can produce a given event stream. In particular, a necessary condition is given for the event stream to be produced based on checking upper and lower bounds of the marking on the Petri net. Algorithms for checking the condition are presented; the computational complexity of checking the condition is polynomial in the number of places and transitions the first time it is checked for a particular model, and linear in the number of transitions when the model is checked for subsequent event streams. An example is presented showing how this condition can be used, together with a model generation approach, for anomaly detection in manufacturing systems.