Skip to Main content Skip to Navigation
Conference papers

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

Tarek Melliti 1 Philippe Dague 2, 3 
3 LEO - Distributed and heterogeneous data and knowledge
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : 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.
Complete list of metadata
Contributor : Philippe Dague Connect in order to contact the contributor
Submitted on : Monday, November 29, 2010 - 12:51:04 PM
Last modification on : Sunday, June 26, 2022 - 11:52:41 AM
Long-term archiving on: : Friday, December 2, 2016 - 6:12:30 PM


Files produced by the author(s)


  • HAL Id : inria-00540849, version 1


Tarek Melliti, Philippe Dague. Generalizing diagnosability definition and checking for open systems: a Game structure approach. 21st International Workshop on Principles of Diagnosis DX'10, Oct 2010, Portland, OR, United States. ⟨inria-00540849⟩



Record views


Files downloads