Ph.D
Group : Large-scale Heterogeneous DAta and Knowledge
SAT-Based Diagnosability and Predictability Analysis in Centralized and Distributed Discrete Event Systems
Starts on 07/01/2013
Advisor : SIMON, Laurent
[DAGUE Philippe]
Funding : Contrat doctoral uniquement recherche
Affiliation : Université Paris-Saclay
Laboratory : LRI-IASI
Defended on 16/12/2016, committee :
Directeur de thèse :
M. Philippe Dague, Professeur, Université Paris-Sud
Co-directeur de thèse :
M. Laurent Simon, Professeur, Université de Bordeaux
Rapporteurs :
- M. Stéphane Lafortune, Professeur, University of Michigan
- M. Lakhdar Saïs, Professeur, Université d'Artois
Examinateurs :
- M. Stefan Haar, Directeur de recherche, Inria & ENS Cachan
- M. Hervé Marchand, Chargé de recherche, Inria & Université de Rennes 1
Research activities :
Abstract :
Complex systems are omnipresent in our lives, but subject to failures that it is important to detect or predict. Discrete event system (DES) modeling is a natural way to represent and study such systems formally. Thus, a system can be described by a set of states such that its current state is obtained after firing a sequence of events. These events are predefined in a finite set and can be fired spontaneously in the system. Not all these events are observable (measurable) and some of them are considered faulty, thus they model an abnormal change between two system states.
The diagnosis process in DES aims at determining with certainty if the system is currently in a faulty state or in a normal one, i.e., if an abnormal change of a system state has occurred or not. To this end, a system observer has only the sequence of observable events to decide the current status of the system state. However, this state might be currently ambiguous (normal or faulty) according to the available observations. Moreover, it can be permanently ambiguous! The possibility to disambiguate it using a finite number of observations is called the diagnosability of a faulty event occurrence. The fault is diagnosable if all its occurrences are diagnosable and the system is diagnosable if all its faults are diagnosable. Similarly, the possibility to predict a future occurrence of a fault using its preceding observable events is called the predictability of a faulty event occurrence. Both problems of diagnosability and predictability can be generalized to study the diagnosability or the predictability of a pattern of events, i.e., an extension-closed language represented by a finite state machine.
This thesis considers in its first part the problems of checking event diagnosability, event predictability and pattern diagnosability in centralized and distributed (with observable or unobservable synchronous communication events) discrete event systems, using SAT solvers. Thus, we have encoded them as SAT problems, studied incremental SAT variants and provided experimental results that prove the scalability and flexibility of this approach. In the second part, we have introduced the diagnosability planning problem. This problem consists in finding a plan of actions (intentional/designful predefined events) that ensures, when applied on a set of potential current system states (called a current belief state), to drive the system in a diagnosable belief state from which it can be left to run freely (without control actions). This problem can arise after an external intervention on the system, like the application of a repair plan after a fault detection. Thus, this approach can ensure the possibility to detect the system further faults. We analyzed this problem, proved its PSpace-completeness and proposed three methods to find the intended plan that we compared on a benchmark created for this purpose.
