LAUSR

We extend and verify diagnosability for a class of set intersection refinement strategies, which can be used for distributed state estimation and fault diagnosis in nondeterministic finite automata that are observed at multiple observation sites. These strategies allow observation sites to (periodically) communicate their diagnostic information (i.e., possible states along with corresponding status, such as normal operation and/or fault type) to other observation sites, which subsequently fuse all available diagnostic information (via set intersection operations), and continue operation based on the refined diagnostic information. We verify diagnosability using the proposed distributed protocol, with polynomial complexity, via compositions of (extended versions of) local verifiers, which are capable of capturing the refinement of information under the set intersection operations, as well as the influence of the refinement process on immediate or future diagnosis decisions.