Student research opportunities
Diagnosis of discrete event systems by SAT
Project Code: CECS_135
This project is available at the following levels:
Honours, Summer Scholar, Masters, PhD
Keywords:
Diagnosis, SAT, Discrete event systems
Supervisor:
Dr Alban GrastienOutline:
Diagnosis is the problem of detecting and identification failures
(unexpected events) in a system. Being able to accurately and quickly
determine the occurrence of faults in a network allows for rapid
intervention leading to 1) faster restoration and 2) lower
vulnerability to so-called fault propagation and cascading effects.
Diagnosis relies on a model of the system (in this occurrence, a
finite state machine) and the actual observations emitted by the
system. Diagnosis is a big community with many different techniques
employed. Diagnosis of discrete event systems is also fairly
developed.
One of the practical issues of diagnosis is the complexity, which is
exponential in the number of components. An approach recently
proposed was the use of SAT techniques for diagnosis. The early
experiments have shown very promising results by solving problems
that were already beyond reach of other methods. We believe that many
potential improvements can be made.
Goals of this project
The directions of this work is two-fold:
* Improve the efficiency of SAT-based diagnosis. Possible techniques
include:
- Improving the reduction for the diagnosis problem to the SAT
problem.
- Extracting useful information from the model to include in the SAT
problem.
- Running inexpensive computations to add information to the SAT
problem (typically, local diagnosis).
- Using incremental SAT techniques.
- Adapting the SAT solver for SAT problems generated from diagnosis
problems (example: adapting the branching variable policy).
- Etc.
* Extend the capacities of SAT-based diagnosis approaches:
- Including time information.
- Improving incremental techniques.
- Studying model properties that pertain to SAT-based diagnosis
methods.
- Etc.
This list is not exhaustive. A Master, Honours, or Summer Scholar
student would probably work only on one of the above mentioned
items.
There is clearly room for a PhD Thesis on the topic.
Student Gain
This work will provide the student a good introduction to diagnosis,
which is an important field in AI, and SAT, which is widely used in
almost all subfields of AI. For undergraduate, this is a wonderful
opportunity to start a collaboration that could lead to a PhD.
Background Literature
For an introduction to diagnosis by SAT:
Alban Grastien, Anbulagan, Jussi Rintanen, and Elena
Kelareva. Modeling and solving diagnosis of discrete-event systems via
satisfiability. In International Workshop on Principles of Diagnosis
(DX-07), 2007
For more information on existing works on diagnosis (and similar
problems) by SAT:
Jussi Rintanen and Alban Grastien. Diagnosability testing with
satisfiability algorithms. In International Joint Conference on
Artificial Intelligence (IJCAI-07), 2007.
Alban Grastien and Anbulagan. Incremental diagnosis of DES with a
non-exhaustive diagnosis engine. In International Workshop on
Principles of Diagnosis (DX-09), pages 345-352, 2009
Anbulagan and Alban Grastien. Importance of variables semantic in CNF
encoding of cardinality constraints. In Symposium on Abstraction,
Reformulation and Approximation (SARA-09), 2009.
