TY - JOUR
T1 - Diagnosis of discrete event systems using satisfiability algorithms
T2 - A theoretical and empirical study
AU - Grastien, Alban
AU - Anbulagan, Anbu
PY - 2013/12
Y1 - 2013/12
N2 - 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.
AB - 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.
KW - Diagnosis
KW - Discrete event systems
KW - Propositional satisfiability
UR - http://www.scopus.com/inward/record.url?scp=84889691158&partnerID=8YFLogxK
U2 - 10.1109/TAC.2013.2275892
DO - 10.1109/TAC.2013.2275892
M3 - Article
SN - 0018-9286
VL - 58
SP - 3070
EP - 3083
JO - IEEE Transactions on Automatic Control
JF - IEEE Transactions on Automatic Control
IS - 12
M1 - 6572825
ER -