Diagnosis of dense-time systems using digital-clocks

We study failure diagnosis of timed discrete-event systems modeled as dense timed-automata for which reachability is decidable (Alur, 1999; Henzinger et al., 1994). Failure diagnosis of such systems was first studied in "formal techniques in real time and fault tolerant systems" by Tripakis (2002), assuming that a diagnoser has partial observation of events but can measure (or "observe") time perfectly. In this paper we relax the latter requirement since in practice time cannot be measured precisely. Thus in our setting we have partial observability of events as well as of "time". We model the observability of time based on a digital-clock of finite precision that measures time discretely by generating ticks, the logic of which is governed by a timed-automaton. As an example a finite-precision finite-drift digital clock that ticks every [Delta plusmn delta] (Delta > delta ges 0) units of time can be modeled as a timed-automaton. We show that the "discrete-time behavior" observed using such a clock is regular, i.e., can be represented using a finite (untimed) automaton. In our analysis we allow the non-failure behavior to be also represented as a separate dense timed-automaton that is deterministic (also decidable), which can be viewed as another extension. We show that the verification of diagnosability (ability to detect specification violation within a bounded delay) as well as the offline synthesis of a diagnoser for a diagnosable system is decidable by reducing the problem to the untimed domain. The reduction to the untimed domain also suggests an effective method for an online diagnosis