A scalable jointree algorithm for diagnosability

Diagnosability is an essential property that determines how accurate any diagnostic reasoning can be on a system given any sequence of observations. An unobservable fault event in a discrete-event system is diagnosable iff its occurrence can always be deduced once sufficiently many subsequent observable events have occurred. A classical approach to diagnosability checking constructs a finite state machine known as a twin plant for the system, which has a critical path iff some fault event is not diagnosable. Recent work attempts to avoid the often impractical construction of the global twin plant by exploiting system structure. Specifically, local twin plants are constructed for components of the system, and synchronized with each other until diagnosability is decided. Unfortunately, synchronization of twin plants can remain a bottleneck for large systems; in the worst case, in particular, all local twin plants would be synchronized, again producing the global twin plant. We solve the diagnosability problem in a way that exploits the distributed nature of realistic systems. In our algorithm consistency among twin plants is achieved by message passing on a jointree. Scalability is significantly improved as the messages computed are generally much smaller than the synchronized product of the twin plants involved. Moreover we use an iterative procedure to search for a subset of the jointree that is sufficient to decide diagnosability. Finally, our algorithm is scalable in practice: it provides an approximate and useful solution if the computational resources are not sufficient.