Partial order diagnosability of discrete event systems using petri net unfoldings

In truly asynchronous, distributed systems, neither global state nor global time are available. The diagnosis approach with Petri net unfoldings, motivated by the problem of event correlation in telecommunications network management and proposed, uses only local states in combination with a partial order model of time. Here, we give a definition of weak and strong diagnosability in terms of partially ordered executions, and characterize diagnosable systems; the characterizing property can be effectively verified using a finite complete prefix of the net unfolding.