Decidability of a Hybrid Duration Calculus

Thomas Bolander, Jens Ulrik Hansen, Michael Reichhardt Hansen

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

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.
OriginalsprogEngelsk
TidsskriftElectronic Notes in Theoretical Computer Science
Vol/bind174
Udgave nummer6
Sider (fra-til)113-133
ISSN1571-0661
DOI
StatusUdgivet - 2007
Udgivet eksterntJa

Citer dette