Combining Enumerative and Symbolic Techniques for Diagnosis of Discrete-Event Systems

VECOS 2015 - 9th Workshop on Verification and Evaluation of Computer and Communication Systems, Bucarest, ROUMANIE, 10-/09/2015 - 11/09/2015In this paper, an efficient approach to verify diagnosability of discrete-event systems is proposed. The approach consists in constructing a hybrid diagnoser based on the symbolic observation graph (SOG), which is a technique that combines symbolic and enumerative representations in order to build a deterministic observer from a partially observed model. The construction of the diagnoser as well as the verification of diagnosability are performed simultaneously on-the-fly, which can considerably reduce the generated state space of the diagnoser and thus the overall running time. Furthermore, the proposed approach provides a heuristic strategy in order to converge fast into the necessary part, of the diagnoser, for analysing diagnosability