On Diagnosability Consistency of Composed Labeled Petri Nets via Buffer Places

Fault diagnosis in Internet of Things systems, where multiple distributed components interact asynchronously through communication buffers, poses significant challenges due to system scalability and communication uncertainties. To address this, this article studies the problem of diagnosability consistency in a discrete event system (DES) modeled using a labeled Petri net (LPN) composed of several interconnected subnets via buffer places. Due to the state explosion problem, the diagnosability analysis by a centralized approach for large-scale systems is computationally demanding and sometimes even impossible. In this work, we assume that Petri net modules are connected through buffer places according to predefined rules and do not share transitions or resources, offering a complementary and computationally efficient alternative to existing modular approaches for large-scale systems. The diagnosability of subnets is analyzed with a particular automaton, called an unfolded verifier, by determining whether there exists a fundamental path that leads to the violation of the diagnosability. The proposed approach investigates the diagnosability of large systems with modular structures (namely, global diagnosability), without constructing a global unfolded verifier, by analyzing the diagnosability of each module only (namely, local diagnosability). More precisely, the consistency between the local diagnosability and the global diagnosability is addressed by determining whether all the fundamental paths of subnets survive in the global net due to the composition of subnets. Finally, an algorithm is given to deduce the diagnosability of a monolithic system. Compared with the existing centralized approaches, the complexity is practically mitigated using the proposed one.