Advanced

Decidability of a Hybrid Duration Calculus

Bolander, Thomas; Hansen, Jens Ulrik LU and Hansen, Michael R. (2007) In Electronical Notes in Theoretical Computer Science 174(6). p.113-133
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.
Please use this url to cite or link to this publication:
author
publishing date
type
Contribution to journal
publication status
published
subject
keywords
duration calculus hybrid logic decision methods monadic second order theory of order
in
Electronical Notes in Theoretical Computer Science
volume
174
issue
6
pages
113 - 133
publisher
Elsevier
external identifiers
  • scopus:34249752075
ISSN
1571-0661
DOI
10.1016/j.entcs.2006.11.029
language
English
LU publication?
no
id
87ec9cb6-ebf6-4ca4-aa2d-2b565d52e5dd (old id 4016218)
date added to LUP
2013-09-03 15:13:42
date last changed
2017-01-01 07:26:43
@article{87ec9cb6-ebf6-4ca4-aa2d-2b565d52e5dd,
  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,<br/><br>
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.},
  author       = {Bolander, Thomas and Hansen, Jens Ulrik and Hansen, Michael R.},
  issn         = {1571-0661},
  keyword      = {duration calculus hybrid logic decision methods monadic second order theory of order},
  language     = {eng},
  number       = {6},
  pages        = {113--133},
  publisher    = {Elsevier},
  series       = {Electronical Notes in Theoretical Computer Science},
  title        = {Decidability of a Hybrid Duration Calculus},
  url          = {http://dx.doi.org/10.1016/j.entcs.2006.11.029},
  volume       = {174},
  year         = {2007},
}