Verification of Coprognosability in Decentralized Fault Prognosis of Labeled Petri Nets

We investigate the problem of decentralized fault prognosis of discrete-event systems modeled by unbounded labeled Petri nets. We assume that the system is monitored by a set of local agents (prognosers) with local observations so that they can predict the occurrence of fault in the system as a team. It is known in the literature that the notion of coprognosability provides the necessary and sufficient condition for the existence of a set of decentralized prognosers so that any fault can be predicted before its occurrence without false alarm. In this paper, we investigate the verification of coprognosability for systems modeled by labeled Petri nets. We show that coprognosability is decidable even when the Petri net is unbounded. Specifically, we provide an approach to transform the coprognosability verification problem to a model checking problem that can be effectively solved. Our result extends existing works on coprognosability analysis in decentralized fault prognosis from regular languages to Petri net languages.