Diagnosis of discrete event systems using satisfiability algorithms: A theoretical and empirical study

Alban Grastien, Anbu Anbulagan

    Research output: Contribution to journalArticlepeer-review

    16 Citations (Scopus)

    Abstract

    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.

    Original languageEnglish
    Article number6572825
    Pages (from-to)3070-3083
    Number of pages14
    JournalIEEE Transactions on Automatic Control
    Volume58
    Issue number12
    DOIs
    Publication statusPublished - Dec 2013

    Fingerprint

    Dive into the research topics of 'Diagnosis of discrete event systems using satisfiability algorithms: A theoretical and empirical study'. Together they form a unique fingerprint.

    Cite this