Modeling and solving diagnosis of discrete-event systems via satisfiability
Alban Grastien, Anbu Anbulagan, Jussi Rintanen, Elena Kelareva · 2007
The diagnosis of a discrete-event system is finding out whether the behavior of the system is normal or faulty, given observations of this behavior. We show how the diagnosis problems can be translated into the propositional satisfiability problem (SAT) and then solved by the state-of-the-art SAT algorithms. Our experiments demonstrate that the SAT algorithms are able to deal with the problems, which are hard for traditional diagnosis algorithms.