Incremental Diagnosis of DES by Satisfiability

Abstract. We propose a SAT-based algorithm for incremental diagnosis of discrete-event systems. The monotonicity is ensured by a prediction window that uses the future observations to lead the current diagnosis. Experiments stress the impact of parameters tuning on the correctness and the efficiency of the approach. 1 Diagnosis by SAT Diagnosis is the AI problem of determining whether a system is running correctly during a time window, and of identifying any failure otherwise. Consider a system which is completely modeled by a DES (basically a finite state machine) denoted Mod. This system is running and generates observations. The goal of the diagnosis is to determine from the model and the observations whether faulty events occurred on the system. The problem can be reduced to finding particular paths on the DES consistent with the observations [4]. Since failures are rare events, we can consider paths that minimize the number of faults. In [2], we proposed to solve the DES diagnosis...

• Type: Conference
• Year: 2008
• Where: ECAI
• Authors: Alban Grastien, Anbulagan
• Keywords: Artificial Intelligence, ECAI 2008, Incremental Diagnosis, SAT Diagnosis, Temporal Window