Diagnose de falhas usando observação parcial de ações e proposições atômicas

Abstract

Fault diagnosis is a quite demanding research subject, in the literature on discrete event systems, many works explore it considering an event/action abstraction modeling approach, while some works explore it using a state abstraction approach. We propose an approach that considers partial observation of both actions and atomic propositions. To deal with this new approach, we redefine the equivalence of traces with respect to stuttering, considering partial observation of actions and atomic propositions. With this new definition of stuttering, we provide a new diagnosability definition. Finally, we provide an on-the-fly model-checking algorithm to verify the diagnosability using a unique LTL formula.