Diagnosis of Dense-Time Systems Under Event and Timing Masks

We study diagnosis of timed discrete-event systems (TDESs) modeled as timed-automata. Earlier works on diagnosis of TDESs assumed that a diagnoser has partial observation of events but can measure (or observe) time with arbitrary precision. In practice, however, time can only be measured with finite precision. We model the finite precision observability of time using a digital-clock that measures time discretely by executing ticks. For the diagnosis purposes, the set of nonfaulty timed-traces is specified as another timed-automaton that is deterministic, generalizing the forms of nonfaulty specifications considered in the earlier works. We show that the set of timed-traces observed using a digital-clock with finite precision is regular, i.e., can be represented using a finite (untimed) automaton. We show that the verification of diagnosability (ability to detect the execution of a faulty timed-trace within a bounded time delay) as well as the offline synthesis of a diagnoser are decidable by reducing these problems to the untimed setting. The reduction of the diagnosis problem to the untimed setting also suggests an effective method for the offline computation of a diagnoser as well as its online implementation for diagnosis.