Exhaustive minimal diagnosis of DES with SAT
Alban Grastien (NICTA)
LOGIC AND COMPUTATION SEMINARDATE: 2011-04-05
TIME: 15:30:00 - 16:30:00
LOCATION: NICTA - 7 London Circuit
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
Diagnosis is the problem of determining which `diagnosis hypotheses' are consistent with the system description (model, here a discrete-event system DES) and the observation generated by the system; we are only interested in minimal hypotheses.
Diagnosis of systems modeled as DES is generally computed by finding all system trajectories in the model consistent with the observation, and extracting the diagnosis information. Because the number of such trajectories is potentially huge, the focus of much work in the domain has been in finding methods to efficiently and implicitly represent and compute those trajectories.
In 2007, we presented a different approach to diagnosis of DES. Rather than computing all trajectories, we proposed to search for only one trajectory from a predefined set of trajectories (such sets include for instance the set of trajectories modeling nominal behaviours, the set of trajectories modeling behaviours with x faults, etc). The proposed implementation reduced the search problem to a SAT problem and used the power of SAT solvers to generate solutions. We used it to compute the minimal-cardinality diagnosis by searching for trajectories with an increasing number of faults.
More recently, we started investigating the use of SAT-based diagnosis
of DES to generate all the minimal hypotheses. We developed two
families of approaches: the top-down approach tests preferrable
hypotheses first and degrade these hypotheses until the diagnosis is
found; the bottom-up approach searches for any solution and refines
these solutions until their minimality was proved. We discuss the
relative properties of these approaches (and in particular termination
issues) and draw connections with the approaches for diagnosis of
static systems.
