© The Author, 2006. Published by Oxford University Press. All rights reserved.
Original Articles |
A Minimal Hybrid Logic for Intervals
1 Department of Computing, Imperial Collage London, South Kensington Campus, London, SW7 2AZ, UK. E-mail: ah701{at}doc.ic.ac.uk
Taking our inspiration from van Benthem's treatment of temporal interval structures, and Halpern and Shoham's work on intervals, we introduce an interval hybrid temporal logic with two binary relations, precedence and inclusion, for talking about interval temporal structures. This paper can be seen as an continuation of the work began in an earlier paper, in which we undertook a purely modal treatment of interval temporal structures. By introducing an interval hybrid temporal logic, we enrich the logic with nominals, and thereby increase the expressivity of the logic. We study the interval hybrid temporal logic in its full generality and identify two important classes of interval temporal structures: the class of minimal interval structures, and the class of van Benthem minimal interval structures. We present sound and complete tableau calculi for both classes of structures. We prove that the logic of minimal interval structures is decidable, by developing a novel bulldozing technique that handles both the presence of nominals and the interaction between the two relations. We go on to show that the satisfiability problem is EXPTIME-complete. We conclude the paper with the remark that the decidability (or otherwise) and complexity of the logic of van Benthem minimal interval structures remains an interesting open problem
Key Words: tableau method, interval logics, hybrid logic, bulldozing
Received 20 July 2005. Revised 15 November 2005.