Model-checking dense-time Duration Calculus

Since the seminal work of Zhou Chaochen, M. R. Hansen, and P. Sestoft on decidability of dense-time Duration Calculus ZHS93] it is well known that decidable fragments of Duration Calculus can only be obtained through withdrawal of much of the interesting vocabulary of this logic. While this was formerly taken as an indication that key-press verification of implementations with respect to elaborate Duration Calculus specifications were also impossible, we show that the model property is well decidable for realistic designs which feature natural constraints on their switching dynamics.The key issue is that the classical undecidability results rely on a notion of validity of a formula that refers to a class of models which is considerably richer than the possible behaviours of actual embedded real-time systems: that of finitely variable trajectories. By analysing two suitably sparser model classes we obtain model-checking procedures for rich subsets of Duration Calculus. Together with undecidability results also obtained, this sheds light upon the exact borderline between decidability and undecidability of Duration Calculi and related logics.Received June 1999Accepted in revised form September 2003 by M. R. Hansen and C. B. Jones