Decidability of Interval Temporal Logics over Split-Frames via Granularity

Abstract. Logics for time intervals provide a natural framework for representing and reasoning about timing properties in various areas of artificial intelligence and computer science. Unfortunately, most interval temporal logics proposed in the literature have been shown to be (highly) undecidable. Decidable fragments of these logics have been obtained by imposing severe restrictions on their expressive power. In this paper, we propose a new interval temporal logic, called Split Logic, which is equipped with operators borrowed from other interval temporal logics, but is interpreted over specific interval structures based on a layered view of the temporal domain. We show that there exists a straightforward correspondence between Split Logic and the first-order fragments of the monadic theories of time granularity proposed in the literature. This connection allows us to transfer existing decidability results for such theories to Split Logic.