Title
Decidability of a Hybrid Duration Calculus
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.
Year
DOI
Venue
2007
10.1016/j.entcs.2006.11.029
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
restricted duration calculus,satisfiability problem,monadic second-order theory,hybrid logical machinery,monadic second order theory of order,duration calculus,down-arrow binder,following hybrid logical machinery,decision methods,global modality,increased expressive power,hybrid logic,hybridizing rdc,hybrid duration calculus
Discrete mathematics,Hybrid logic,Computer science,Boolean satisfiability problem,Satisfiability,Decidability,Operator (computer programming),Duration calculus,Monad (functional programming),Monadic predicate calculus
Journal
Volume
Issue
ISSN
174
6
Electronic Notes in Theoretical Computer Science
Citations 
PageRank 
References 
8
0.47
16
Authors
3
Name
Order
Citations
PageRank
Thomas Bolander112715.24
jens ulrik hansen2354.44
Michael r. Hansen354343.29