@ARTICLE\{IMM2004-01784,
    author       = "M. Fr{\"{a}}nzle",
    title        = "Model-checking dense-time duration calculus",
    year         = "2004",
    keywords     = "Dense-time Duration Calculus; Decidability; Model-Checking",
    pages        = "121-139",
    journal      = "Formal Aspects of Computing",
    volume       = "16",
    editor       = "",
    number       = "2",
    publisher    = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/1784-full.html",
    abstract     = "Since the seminal work of Zhou Chaochen, M. R. Hansen, and
  P. Sestoft on decidability of dense-time Duration Calculus
  [Zhou, Hansen, Sestoft, 1993] 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."
}