Fault diagnosis for timed automata

Abstract

We study the problem of fault-diagnosis in the context of dense-time automata. The problem is, given the model of a plant as a timed automaton with a set of observable events and a set of unobservable events, including a special event modeling faults, to construct a deterministic machine, the diagnoser, which reacts to observable events and time delays, and announces a fault within a delay of at most Δ time units after the fault occurred. We define what it means for a timed automaton to be diagnosable, and provide algorithms to check diagnosability. The algorithms are based on standard reachability analyses in search of accepting states or non-zeno runs. We also show how to construct a diagnoser for a diagnosable timed automaton, and how the diagnoser can be implemented using data structures and algorithms similar to those used in most timed-automata verification tools.