Verification of diagnosability and co-diagnosability
Diagnosis of discrete event systems (DESs)

The notion of "diagnosability" allows us to formally verify whether a set of faults can be diagnosed within a given timeframe, based on a process model and a set of observable events . Depending on the structure (centralized, decentralized, distributed) and the fault model (event-based, state-based), several forms of this notion can be defined: event-based or state-based diagnosability and codiagnosability.

In order to define the various forms of this notion, we recall some basic definitions. Every automaton...