Decidability of a Hybrid Duration Calculus |
Thomas Bolander, Jens Ulrik Hansen, Michael R. Hansen
|
| 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. |
| Keywords | Duration calculus, hybrid logic, decision methods, monadic second order theory of order. |
| Type | Conference paper [With referee] |
| Conference | Electronic Notes in Theoretical Computer Science |
| Year | 2007 Vol. 174 pp. 113-133 |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |