Verification of modular diagnosability with local specifications for discrete-event systems

Abstract

In this paper, we study the diagnosability verification for modular discrete-event systems (DESs), i.e., DESs that are composed of multiple components. We focus on a particular modular architecture, where each fault in the system must be uniquely identified by the modular component where it occurs and solely based on event observations of that component. Hence, all diagnostic computations for faults to be detected in this architecture can be performed locally on the respective modular component, and the obtained diagnosis information is only relevant for that component. We define the condition of modular language diagnosability with local specifications (MDLS) in order to capture that each fault can indeed be detected in this modular architecture. Then, we show that MDLS can be formulated as a specific language-diagnosability problem. As the main contribution of this paper, we develop an incremental abstraction-based approach for the verification of MDLS, which is based on projections that fulfill the loop-preserving observer condition. In particular, our approach efficiently avoids the construction of a global system model, which is infeasible for systems of realistic size. Furthermore, we do not rely on the assumption of a live global plant, which is prevalent in previous diagnosability methods for modular DESs. We illustrate our approach and its computational savings by a manufacturing system example.