Model-checking discrete duration calculus

Duration Calculus was introduced in ZHR91] as a logic to specify and reason about requirements for real-time systems. It is an extension of Interval Temporal Logic Mos85] where one can reason about integrated constraints over time-dependent and Boolean valued states without explicit mention of absolute time. Several major case studies, e.g. the gas burner system in RRH93], have shown that Duration Calculus provides a high level of abstraction for both expressing and reasoning about specifications. Using Timed Automata A1D92] one can express how real-time systems can be constructed at a level of detail which is close to an actual implementation. We consider in the paper the correctness of Timed Automata with respect to Duration Calculus formulae. For a subset of Duration Calculus, we show that one can automatically verify whether a Timed Automaton is correct with respect to a formulaD, abbreviated D, i.e. one can domodel-checking. The subset we consider is expressive enough to formalize the requirements to the gas burner system given in RRH93]; but only for a discrete time domain. Model-checking is done by reducing the correctness problem D to the inclusion problem of regular languages.