@CONFERENCE\{IMM2007-05009,
    author       = "T. Bolander and J. Hansen and M. R. Hansen",
    title        = "Decidability of a Hybrid Duration Calculus",
    year         = "2007",
    keywords     = "Duration calculus, hybrid logic, decision methods, monadic second order theory of order.",
    pages        = "113-133",
    booktitle    = "Electronic Notes in Theoretical Computer Science",
    volume       = "174",
    series       = "",
    editor       = "",
    publisher    = "",
    organization = "",
    address      = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/5009-full.html",
    abstract     = "We present a logic which we call Hybrid Duration Calculus (HDC). {HDC} is
  obtained by adding the following hybrid logical machinery to the
  Restricted Duration Calculus (RDC): nominals, satisfaction
  operators, down-arrow binder, and the global modality. {RDC} is known to be
  decidable, and in this paper we show that decidability is retained
  when adding the hybrid logical machinery. Decidability of {HDC} is
  shown by reducing the satisfiability problem to satisfiability of
  Monadic Second-Order Theory of Order. We illustrate the increased
  expressive power obtained in
  hybridizing {RDC} by showing that {HDC,} in contrast to {RDC,} 
  can express all of the 13 possible relations between intervals."
}