Diagnosis of discrete event systems in rules-based model using first-order linear temporal logic

We study diagnosis of discrete event systems (DESs) modeled in the rule-based modeling formalism introduced, and applied to model failure-prone systems. An attractive feature of rule-based model is its compactness (size is polynomial in number of signals). A motivation for the work presented is to develop failure diagnosis techniques that are able to exploit this compactness. In this regard, we develop symbolic techniques for testing diagnosability and computing a diagnoser. Diagnosability test is shown to be an instance of 1st order temporal logic model-checking. An on-line algorithm for diagnoser synthesis is obtained by using predicates and predicate transformers.