Diagnosis of Discrete Event Systems Using Satisfiability Algorithms: A Theoretical and Empirical Study

We propose a novel algorithm for the diagnosis of systems modelled as discrete event systems. Instead of computing all paths of the model that are consistent with the observations, we use a two-level approach: at the first level diagnostic questions are generated in the form does there exist a path from a given subset that is consistent with the observations?, whilst at the second level a satisfiability (SAT) solver is used to answer the questions. Our experiments show that this approach, implemented in SAT, can solve problems that we could not solve with other techniques.