The verification of codiagnosability in the case of dynamic observations

Weilin Wang, Anouck R. Girard, Stephane Lafortune, Feng Lin

Research output: Chapter in Book/Report/Conference proceedingConference PaperOther


We consider the verification of the properties of diagnosability and codiagnosability in discrete event systems where observations are dynamic. Instead of having a fixed set of observable events, it is assumed that the observability properties of an event are state-dependent: an event occurrence at a state will be observable to a diagnosing agent if that agent activates in time the sensor corresponding to the event or receives a communication about the occurrence of the event. In this context, the known polynomial-complexity tests based on verifier automata for the properties of diagnosability and codiagnosability with fixed observable event set(s) are no longer directly applicable. We develop a new testing procedure that can handle state-based dynamic observations and remains of polynomial complexity in the state space of the system. This new testing procedure employs a covering of the state space of the system based on cluster automata, which enhances its computational efficiency. Based on cluster automata, a new type of verifier automaton is built, called the C-VERIFIER. Our use of cluster automata and C-VERIFIERS also yields computational savings in the special case of fixed observable event sets.

Original languageEnglish
Title of host publication2009 European Control Conference, ECC 2009
PublisherIEEE, Institute of Electrical and Electronics Engineers
Number of pages6
ISBN (Electronic)9783952417393
Publication statusPublished - 26 Mar 2014
Externally publishedYes
EventEuropean Control Conference 2009 - Budapest, Hungary
Duration: 23 Aug 200926 Aug 2009
Conference number: 10th (Proceedings)


ConferenceEuropean Control Conference 2009
Abbreviated titleECC 2009
Internet address

Cite this