摘要：Abstract:This paper deals with analysis of diagnosability andK-diagnosability of dynamic systems in a model-checking framework. Dynamic systems are abstracted here as Discrete-Event Systems (DESs) and modeled by Input/Output Transition Systems (IOTSs). We reformulate diagnosability issues using CTL formula while considering extended definitions of diagnosability. Moreover, we introduce a formal definition ofK-diagnosability in model-checking framework and we discuss the problem ofKmin-diagnosability (the minimal value ofKensuring diagnosability). We also show how diagnosability analysis in model-checking framework can be extended in order to deal with repeated/intermittent failures. In this regard, the case of [1-∞]-diagnosability analysis is investigated. Finally, some of these theoretical contributions are illustrated through a benchmark.
