Decidability of interval temporal logics over split-frames via granularity

Decidability of Interval Temporal Logics over Split-Frames via Granularity Angelo Montanari, Guido Sciavicco, and Nicola Vitacolonna University of Udine, via delle Scienze 206 33100 Udine (UD), Italy {montana, sciavicc, vitacolo}@dimi.uniud.it

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.

1

Introduction

Logics for time intervals provide a natural framework for dealing with timing properties in various fields of artificial intelligence and computer science [5,6,14,4,7]. As an example, in planning and qualitative physics reasoning about time intervals rather than time points is far more natural and closer to common sense (a systematic account of the relationships between point-based and interval-based temporal logics can be found in [13]). Unfortunately, most interval temporal logics proposed in the literature, such as Moszkowski’s Interval Temporal Logic (ITL) [5], Halpern and Shoham’s Modal Logic of Time Intervals (HS) [6], Venema’s CDT Logic [14], and Chaochen and Hansen’s Neighborhood Logic (NL) [4], have been shown to be (highly) undecidable. ITL is provided with the two modal operators d (next) and ; (chop). An ITL interval is a finite or infinite sequence of states. Given two formulae ϕ, ψ and an interval s0 , . . . , sn , dϕ holds over s0 , . . . , sn if and only if ϕ holds over s1 , . . . , sn , while ϕ ; ψ holds over s0 , . . . , sn if and only if there exists i, with 0 ≤ i ≤ n, such that ϕ holds over s0 , . . . , si and ψ holds over si , . . . , sn . The undecidability of Propositional ITL has been proved by a reduction from the problem of testing the emptiness of the intersection of two grammars in Greibach form [12]. HS features three basic operators hAi (after), hBi (begin), and hEi (end), together

¯ hBi, ¯ and hEi. ¯ Given a formula ϕ and an interval [a, b], hAiϕ with their duals hAi, holds at [a, b] if and only if ϕ holds at [b, c], for some c > b, hBiϕ holds at [a, b] if and only if ϕ holds at [a, c], for some c < b, and hEiϕ holds at [a, b] if and only if ϕ holds at [c, b], for some c > a. HS has been shown to be undecidable by coding the halting problem in it. CDT has three binary operators C, D, and T, which informally deal with the situations generated by adding an extra point in one of the three possible positions with respect to the two points delimiting an interval (before, in between, and after). Since HS is a subsystem of CDT, the undecidability of the latter easily follows. Finally, NL is a first-order interval logic with two expanding modalities ♦l and ♦r . Given a formula ϕ and an interval [a, b], ♦l ϕ holds at [a, b] if and only if ϕ holds at [c, a], for some c ≤ a, and ♦r ϕ holds at [a, b] if and only if ϕ holds at [b, c], for some c ≥ b. Since HS can be easily embedded in NL, the undecidability of the latter immediately follows. Decidable fragments of these logics have been obtained by imposing severe restrictions on their expressive power, e.g., [12,3]. As an example, Moszkowski [12] proves the decidability of the fragment of Propositional ITL with Quantification (over propositional variables) which results from the introduction of a locality constraint. Such a constraint states that each propositional variable is true over an interval if and only if it is true at its first state. This allows one to collapse all the intervals starting at the same state into the single interval consisting of the first state only. Decidability of ITL with locality can be easily proved by embedding it into Quantified Propositional Linear Temporal Logic. In this paper, we propose a new interval temporal logic, called Split Logic (SL for short), which is equipped with operators borrowed from HS and CDT, but is interpreted over specific interval structures, called split-frames. The distinctive feature of a split-frame is that there is at most one way to chop an interval into two adjacent subintervals and, consequently, it does not possess “all” the intervals. We will prove the decidability of SL with respect to particular classes of split-frames which can be put in correspondence with the first-order fragments of the monadic theories of time granularity proposed in the literature. Furthermore, we will establish the completeness of SL with respect to the guarded fragment of these theories. The paper is organized as follows. In Section 2 we introduce the relevant interval and granular temporal structures, while in Section 3 we describe the syntax and semantics of SL. In Section 4 we connect SL to first-order theories of time granularity, and then we establish some decidability results for SL. In Section 5 we state a completeness result for SL. In Section 6 we outline some decidable extensions of SL. Finally, in Section 7 we make some concluding remarks and discuss further research topics.

2

Temporal Structures

In the following, we separately introduce temporal structures for time intervals and time granularity. All the structures we will consider are relational structures, that is, tuples whose first component is a non-empty domain W and the remain-

ing components are relations on W . We assume that every relational structure contains at least the equality relation. 2.1

Interval Structures

Following [13], we opt for two primitive relations on intervals, namely an inclusion relation