Marking Predictability and Prediction in Labeled Petri Nets

This article studies the marking prediction problem in labeled Petri nets. Marking prediction aims to recognize a priori that the plant will inevitably reach a given set of alert markings in finite future steps. Specifically, we require that a marking prediction procedure should have the following properties: i) no missed alarm, i.e., an alarm can always be issued before reaching an alert marking; and ii) no false alarm, i.e., once an alarm is issued, the plant will eventually reach an alert marking in the future. To this end, the notion of marking predictability is proposed as a necessary and sufficient condition for the solvability of the marking prediction problem. A fundamental marking estimation problem in a labeled Petri net is first solved using minimal explanations and basis reachability graphs. Then, we propose two notions of basis markings called boundary basis markings and basis indicators, and prove that a plant is predictable with respect to a set of alert markings if all basis markings confusable with boundary basis markings are basis indicators. By properly selecting a set of explicit transitions, the set of basis indicators can be efficiently computed by structural analysis of the corresponding basis reachability graph. Our method has polynomial complexity in the number of basis markings. Finally, we present an effective algorithm for online marking prediction if the plant is predictable.