Generalizing diagnosability definition and checking for open systems: a Game structure approach

Tarek Melliti and Philippe Dague
Submission Type: 
Full Paper
Supporting Agencies (optional): 
French National Agency for Research
phmc_10_129.pdf118.64 KBNovember 2, 2010 - 4:21am

Diagnosability is the property of a partially observable system with a given set of possible faults, that these faults can be detected with certainty with a finite
observation. Usually, the definition and the verification methods of diagnosability ignore the nature of the system events, controllable (by the system) or uncontrollable. In this paper we show the influence of controllability of events on the diagnosability definition and verification. We show that the classical diagnosability is a special case where we consider the whole system as controllable. Using Game Structure we generalize the definition of diagnosability by the mean of strategies. Then, Alternating-time Temporal Logic is used in order to model check
diagnosability in the case of uncontrollable events. We show how the framework is suitable for one system and also for a set of interacting systems.

Publication Control Number: 
Submission Keywords: 
diagnosability analysis
discrete-event systems
game structure
Alternating-time Temporal Logic
Submitted by: 

follow us

PHM Society on Facebook Follow PHM Society on Twitter PHM Society on LinkedIn PHM Society RSS News Feed