Modeling and solving diagnosis of discrete-event systems via satisfiability

摘要: The diagnosis of a discrete-event system is finding out whether the behavior normal or faulty, given observations this behavior. We show how problems can be translated into propositional satisfiability problem (SAT) and then solved by state-of-the-art SAT algorithms. Our experiments demonstrate that algorithms are able to deal with problems, which hard for traditional