Expressiveness of the Interval Logics of Allen's Relations on the Class of All Linear Orders: Complete Classification

1 Introduction

Interval reasoning naturally arises in various fields of artificial intelligence, such as theories of action and change, natural language analysis and processing, and constraint satisfaction problems. Interval temporal logics formalize reasoning about interval structures over ordered domains, where time intervals, rather than time instants, are the primitive ontological entities. The variety of binary relations between intervals in linear orders was first studied systematically by Allen [Allen, 1983], who explored their use in systems for time management and planning. The modal logic featuring modal operators corresponding to Allen's interval relations was introduced by Halpern and Shoham in [Halpern and Shoham, 1991]; we hereafter call that logic HS. Temporal logics with interval-based semantics have also been proposed as a suitable formalism for the specification and verification of hardware [Moszkowski, 1983] and of real-time systems [Zhou and Hansen, 2004].

In [Halpern and Shoham, 1991], it was shown that the satisfiability problem for HS is undecidable in all natural classes of linear orders. For a long time, these sweeping undecidability results have discouraged attempts for practical applications of interval logics. A renewed interest in the area has recently been stimulated by the discovery of several interesting decidable fragments of HS [Bresolin et al., 2007a; 2007b; 2008; 2009; 2010; Montanari et al., 2010a; 2010b]. In that context, and for the purpose of identifying expressive interval logics for various intended applications, the comparative analysis of the expressiveness of the variety of interval logics is a major research problem in the area. In particular, the important problem arises to analyze the mutual definabilities among the modal operators of the logic HS and to classify the fragments of HS with respect to their expressiveness.

∗We would like to acknowledge the Spanish project TIN200914372-C03-01 (G. Sciavicco), the HYLOCORE project, funded by the Danish Natural Science Research Council (V. Goranko), the Italian PRIN project Innovative and multi-disciplinary approaches for constraint and preference reasoning (D. Della Monica, A. Montanari), and the Spanish/South-African Project HS2008-0006 (V. Goranko, G. Sciavicco).

†Currently affiliated with University of Salerno, Italy.

In the present paper we address and solve that problem, by identifying a complete set of inter-definability formulae among the modal operators of HS and thus providing a complete classification of all fragments of HS with respect to their expressiveness for the strict semantics (excl. point intervals) over the class of all linear orders. Using that result we have found that there are exactly 1347 expressively different such fragments out of 212 = 4096 sets of modal operators in HS.

The choice of strict semantics, excluding point intervals, instead of including them (non-strict semantics), conforms to the definition of interval adopted by Allen in [Allen, 1983]. It has at least two strong motivations. First, a number of representation paradoxes arise when the non-strict semantics is adopted, due to the presence of point intervals, as pointed out in [Allen, 1983]. Second, when point intervals are included, there seems to be no intuitive semantics for interval relations that makes them both pairwise disjoint and jointly exhaustive.

The structure of the paper: after the preliminary Section 2, in Section 3 we state the main result of the paper, and we prove that the proposed set of inter-definability equations is correct. The much more difficult proof of completeness is given in Section 4. Section 5 provides an assessment of the work done and it outlines future research directions.

2 Preliminaries

Let D = 〈D, <〉 be a linearly ordered set. An interval over D is an ordered pair [a, b], where a, b ∈ D and a ≤ b. Intervals of the type [a, a] are called point intervals, while the others are called strict intervals. There are 12 different non-trivial relations (excluding the equality) between two strict intervals

• 〈A〉 [a, b]RA[c, d] ⇔ b = c
• 〈L〉 [a, b]RL[c, d] ⇔ b < c
• 〈B〉 [a, b]RB[c, d] ⇔ a = c, d < b
• 〈E〉 [a, b]RE[c, d] ⇔ b = d, a < c
• 〈D〉 [a, b]RD[c, d] ⇔ a < c, d < b
• 〈O〉 [a, b]RO[c, d] ⇔ a < c < b < d

in a linear order, often called Allen's relations [Allen, 1983]: the six relations depicted in Table 1 and the inverse relations.

We treat interval structures as Kripke structures and Allen's relations as accessibility relations in them, thus associating a modal operator 〈X〉 with each Allen's relation RX. For each operator 〈X〉, its transpose, denoted by 〈X〉, corresponds to the inverse relation RX of RX (that is, RX = (RX)-1 ).

Halpern and Shoham's logic HS is a multi-modal logic with formulae built over a set AP of propositional letters, the propositional connectives ∨ and ¬, and a set of modal operators associated with all Allen's relations. With every subset {RX1 , . . . ,RXk } of these relations, we associate the fragment X1X2 . . . Xk of HS, the formulae of which are defined by the grammar:

The other propositional connectives, ∧ and →, and the dual operators [X] are defined as usual, e.g., [X]ϕ ≡ ¬〈X〉¬ϕ.

For a fragment F = X1X2 . . . Xk and a modal operator 〈X〉, we write 〈X〉 ∈ F if X ∈ {X1, . . . ,Xk}. Given two fragments F1 and F2, we write F1 ⊆ F2 if 〈X〉 ∈ F1 implies 〈X〉 ∈ F2, for every modal operator 〈X〉.

The semantics of HS is given in terms of interval models M = 〈I(D), V 〉, where I(D) is the set of all (strict) intervals over D. The valuation function V : AP ↦→ 2I(D) assigns to every p ∈ AP the set of intervals V (p) on which p holds. The truth of a formula on a given interval [a, b] in an interval model M is defined by structural induction on formulae:

• M, [a, b] ⊩ p iff [a, b] ∈ V (p), for all p ∈ AP;
• M, [a, b] ⊩ ¬ψ iff it is not the case that M, [a, b] ⊩ ψ;
• M, [a, b] ⊩ ϕ ∨ ψ iff M, [a, b] ⊩ ϕ or M, [a, b] ⊩ ψ;
• M, [a, b] ⊩ 〈X〉ψ iff there exists an interval [c, d] such that [a, b]RX[c, d] and M, [c, d] ⊩ ψ, where RX is any of Allen's relations.

A formula φ of HS is valid, denoted |= φ, if it is true on every interval in every interval model. Two formulae φ and ψ are equivalent, denoted φ ≡ ψ, if |= φ ↔ ψ.

Definition 2.1. A modal operator 〈X〉 of HS is definable in an HS-fragment F, denoted 〈X〉◁ F, if 〈X〉p ≡ ψ for some formula ψ = ψ(p) ∈ F, for any fixed propositional variable p. In such a case, the equivalence 〈X〉p ≡ ψ is called an inter-definability equation for 〈X〉 in F.

It is known from [Halpern and Shoham, 1991] that, in the strict semantics, all modal operators in HS are definable in the fragment containing the modalities 〈A〉, 〈B〉, and 〈E〉, and their transposes 〈A〉, 〈B〉, and 〈E〉 (In the non-strict semantics, the four modalities 〈B〉, 〈E〉, 〈B〉, and 〈E〉 suffice, as shown in [Venema, 1990]).

In this paper, we compare and classify the expressiveness of all fragments of HS on the class of all interval structures over linear orders. Formally, let F1 and F2 be any pair of such fragments. We say that:

• F2 is at least as expressive as F1, denoted F1 ⪯ F2, if every operator 〈X〉 ∈ F1 is definable in F2.
• F1 is strictly less expressive than F2, denoted F1 ≺ F2, if F1 ⪯ F2 but not F2 ⪯ F1.
• F1 and F2 are equally expressive (or, expressively equivalent), denoted F1 ≡ F2, if F1 ⪯ F2 and F2 ⪯ F1.
• F1 and F2 are expressively incomparable, denoted F1 ̸≡ F2, if neither F1 ⪯ F2 nor F2 ⪯ F1.

In order to show non-definability of a given modal operator in a given fragment, we use a standard technique in modal logic, based on the notion of bisimulation and the invariance of modal formulae with respect to bisimulations (see, e.g., [Blackburn et al., 2002]). Let F be an HS-fragment. An F-bisimulation between two interval models M = 〈I(D), V 〉 and M ′ = 〈I(D′ ), V ′ 〉 over AP is a relation Z ⊆ I(D)×I(D′ ) satisfying the following properties:

• local condition: Z-related intervals satisfy the same propositional letters over AP;
• forward condition: if ([a, b], [a′ , b′ ]) ∈ Z and ([a, b], [c, d]) ∈ RX for some 〈X〉 ∈ F, then there exists [c′ , d′ ] such that ([a′ , b′ ], [c′ , d′ ]) ∈ RX and ([c, d], [c′ , d′ ]) ∈ Z;
• backward condition: likewise, but fromM ′ toM.

The important property of bisimulations used here is that any F-bisimulation preserves the truth of all formulae in F. Thus, in order to prove that an operator 〈X〉 is not definable in F, it suffices to construct a pair of interval models M and M ′ and a F-bisimulation between them, relating a pair of intervals [a, b] ∈ M and [a′ , b′ ] ∈ M ′ , such that M, [a, b] ⊩ 〈X〉p, while M ′ , [a′ , b′ ] ̸⊩ 〈X〉p.

3 Comparing the expressiveness of the fragments of HS

In order to classify all fragments of HS with respect to their expressiveness, it suffices to identify all definabilities of modal operators 〈X〉 in fragments F, where 〈X〉 /∈ F.

A definability 〈X〉 ◁ F is optimal if 〈X〉 ̸◁ F ′ for any fragment F ′ such that F ′ ≺ F. A set of such definabilities is optimal if it consists of optimal definabilities.

The main result of the paper is the following theorem.

Theorem 3.1. The set of inter-definability equations given in Table 2 is sound, complete, and optimal.

Most of the equations in Table 2 are known from [Halpern and Shoham, 1991], except the definability 〈L〉 ◁ BE and its symmetric, 〈L〉 ◁ BE, which are new. We will first prove the soundness of the given set of inter-definability equations.

Lemma 3.2. The set of inter-definability equations given in Table 2 is sound.

Proof. We only need to prove the soundness for the new interdefinability equations 〈L〉p ≡ 〈B〉[E]〈B〉〈E〉p and its symmetric for 〈L〉. The proofs are analogous, so we only prove the former. First, we prove the left-to-right direction. Suppose that M, [a, b] ⊩ 〈L〉p for some model M and interval [a, b]. This means that there exists an interval [c, d] such that b < c and M, [c, d] ⊩ p. We exhibit an interval [a, y], with y > b such that, for every x (strictly) in between a and y, the interval [x, y] is such that there exist two points y′ and x′ such that y′ > y, x < x′ < y′ , and [x′ , y′ ] satisfies p. Let y be equal to c. The interval [a, c], which is started by [a, b], is such that for any of its ending intervals, that is, for any interval of the form [x, c], with a < x, we have that x < c < d and M, [c, d] ⊩ p. As for the other direction, we must show that 〈B〉[E]〈B〉〈E〉p implies 〈L〉p. To this end, suppose that M, [a, b] ⊩ 〈B〉[E]〈B〉〈E〉p for a model M and an interval [a, b]. Then, there exists an interval [a, c], for some c > b, such that [E]〈B〉〈E〉p is true on [a, c]. As a consequence, the interval [b, c] must satisfy 〈B〉〈E〉p, that means that there are two points x and y such that y > c, b < x < y, and [x, y] satisfies p. Since x > b, then M, [a, b] ⊩ 〈L〉p.

Proving completeness is the hard task; optimality will be established together with it. The completeness proof is organized as follows. For each HS operator 〈X〉, we show that 〈X〉 is not definable in any fragment of HS that does not contain as definable (according to Table 2) all operators of some of the fragments in which 〈X〉 is definable (according to Table 2). More formally, for each HS operator 〈X〉, the proof consists of the following steps:

1. using Table 2, find all fragments Fi such that 〈X〉◁ Fi;
2. identify the list M1, . . . ,Mm of all ⊆-maximal fragments of HS that contain neither the operator 〈X〉 nor any of the fragments Fi identified by the previous step;
3. for each fragment Mi, with i ∈ {1, . . . ,m}, provide a bisimulation for Mi which is not a bisimulation for X.

Details of the completeness proof will be provided in a series of lemmas (of increasing complexity) in the next section.

4 The completeness proof

In this section, we will prove that, for each modal operator 〈X〉 of HS, the set of inter-definability equations for 〈X〉 in Table 2 is complete for that operator, that is, 〈X〉 is not definable in any fragment of HS that does not contain (as definable) all operators of some of the fragments listed in Table 2 in which 〈X〉 is definable. Due to space limitations, we will not prove in detail all the cases. A detailed proof can be found in the extended technical report and it will appear in a future journal version of the present paper.

4.1 Completeness for 〈L〉 and 〈L〉

Lemma 4.1. The set of inter-definability equations for 〈L〉 and 〈L〉 given in Table 2 is complete.

Proof. According to Table 2, 〈L〉 is definable in terms of A and BE. Hence, the fragments BEDOALEDO and BDOALBEDO are the only ⊆-maximal ones not featuring 〈L〉 and containing neither A nor BE. To prove the thesis, it suffices to exhibit a bisimulation for each one of these two fragments that does not preserve the relation induced by 〈L〉. Thanks to Lemma 3.2, BEDOALEDO and BDOALBEDO are expressively equivalent to BEOAED and BDOABE, respectively. Thus, to all our purposes, we can simply refer to the latter ones instead of the former ones.

As for the first fragment, let M1 = 〈I(N), V1〉 and M2 = 〈I(N), V2〉 be two models and let V1 and V2 be such that V1(p) = {[2, 3]} and V2(p) = ∅, where p is the only propositional letter of the language. Moreover, let Z be a relation between (intervals of) M1 and M2 defined as Z = {([0, 1], [0, 1])}. It can be easily shown that Z is a BEOAEDbisimulation. The local property is trivially satisfied, since all Z-related intervals satisfy ¬p. As for the forward and backward conditions, it suffices to notice that, starting from the interval [0, 1], it is not possible to reach any other interval using any of the modal operators of the fragment. At the same time, Z does not preserve the relation induced by the modality 〈L〉. Indeed, ([0, 1], [0, 1]) ∈ Z and M1, [0, 1] ⊩ 〈L〉p, but M2, [0, 1] ⊩ ¬〈L〉p. Therefore, 〈L〉 is not definable in BEDOALEDO.

As for the second fragment, let M1 = 〈I(Z-), V1〉 and M2 = 〈I(Z-), V2〉 be two models based on the set Z-= {. . . ,-2,-1}, and let V1 and V2 be such that V1(p) = {[-2,-1]} and V2(p) = ∅, where p is the only propositional letter of the language. Moreover, let Z be a relation between (intervals of) M1 and M2 defined as follows: ([x, y], [w, z]) ∈ Z def ⇔ [x, y] = [w, z] and [x, y] ̸= [-2, -1]. We prove that Z is a BDOABE-bisimulation. First, the local property is trivially satisfied, since all Z-related intervals satisfy ¬p. Moreover, starting from any interval, the only interval that satisfies p, that is, [-2,-1], cannot be reached using the set of modal operators featured by our fragment. At the same time, Z does not preserve the relation induced by 〈L〉, as ([-4, -3], [-4, -3]) ∈ Z and M1, [-4, -3] ⊩ 〈L〉p, but M2, [-4,-3] ⊩ ¬〈L〉p. Therefore, 〈L〉 is not definable in BDOALBEDO.

A completely symmetric argument can be applied for the completeness proof of 〈L〉.

4.2 Completeness for 〈E〉, 〈E〉, 〈B〉, and 〈B〉

Lemma 4.2. The set of inter-definability equations for 〈E〉, 〈E〉, 〈B〉, and 〈B〉 given in Table 2 is complete.

Proof. According to Table 2, we will show that 〈E〉 is not definable in terms of the only ⊆-maximal fragment not featuring it, namely, ALBDOALBEDO. (The inverse modality 〈E〉 and the symmetric modalities 〈B〉 and 〈B〉 can be dealt with using similar arguments.) Thanks to Lemma 3.2, it actually suffices to provide a bisimulation for ABDOABE.

Let M1 = 〈I(R), V1〉 and M2 = 〈I(R), V2〉, where p is the only propositional letter of the language, the valuation function V1 : AP → 2I(R) is defined as: [x, y] ∈ V1(p) def ⇔ x ∈ Q iff y ∈ Q, and the valuation function V2 : AP → 2I(R) as: [w, z] ∈ V2(p) def ⇔ w ∈ Q iff z ∈ Q, and ([0, 3], [w, z]) /∈ RE. Moreover, let Z be a relation between (intervals of) M1 and M2 defined as follows: ([x, y], [w, z]) ∈ Z def ⇔ [x, y] ∈ V1(p) iff [w, z] ∈ V2(p).

We show that Z is an ABDOABE-bisimulation between M1 and M2. The satisfaction of the local condition immediately follows from the definition. The forward condition can be checked as follows. Let Q = R\Q and let [x, y] and [w, z] be two Z-related intervals. For each modal operator 〈X〉 of the language, let us assume that [x, y]RX[x′ , y′ ]. We have to exhibit an interval [w′ , z′ ] such that [x′ , y′ ] and [w′ , z′ ] are Zrelated, and [w, z] and [w′ , z′ ] are RX-related. We proceed case-by-case. Let 〈X〉 = 〈A〉 (and thus y = x′ ). Suppose that [x′ , y′ ] ∈ V1(p) (resp., [x′ , y′ ] /∈ V1(p)). We can always find a point z′ > z such that [z, z′ ] ∈ V2(p) (resp., [z, z′ ] /∈ V2(p)), independently from z belonging to Q or Q (since both Q and Q are right-unbounded). This implies that [x′ , y′ ] and [z, z′ ] are Z-related. Since [w, z] and [z, z′ ] are obviously RA-related, we have the thesis. If 〈X〉 = 〈B〉, the argument is similar to the previous one, but, in this case, the density of Q and Q is exploited. If 〈X〉 = 〈D〉, it suffices to choose two points w′ and z′ such that w < w′ < z′ < z, z′ ̸= 3, w′ belongs to Q if and only if x′ does, and z′ belongs to Q if and only if y′ does. As in the previous case, the existence of such points is guaranteed by the density of Q and Q. If 〈X〉 = 〈O〉, w′ and z′ are required to be such that w < w′ < z < z′ , and both density and right-unboundedness of Q and Q must be exploited. The remaining cases as well as the backward condition can be verified in a very similar way. At the same time, Z does not preserve the relation induced by 〈E〉: we have that ([0, 3], [0, 3]) ∈ Z, M1, [0, 3] ⊩ 〈E〉p, but M2, [0, 3] ⊩ ¬〈E〉p. Therefore, 〈E〉 cannot be defined in the fragment ALBDOALBEDO.

4.3 Completeness for 〈A〉 and 〈A〉

In the proofs of Lemma 4.3 and Lemma 4.4, in order to get the bisimulation we want, we need to exploit a well-known property of the set of real numbers R: R (resp., Q, Q) can be partitioned into a countable number of pairwise disjoint subsets, each one of which is dense in R. More formally, there are countably many nonempty sets Ri (resp., Qi, Qi), with i ∈ N, such that, for each i ∈ N, Ri (resp., Qi, Qi) is dense in R, R = ⋃i∈N Ri (resp., Q = ⋃i∈N Qi, Q = ⋃i∈N Qi), and Ri ∩Rj = ∅, (resp., Qi ∩Qj = ∅, Qi ∩Qj = ∅), for each i, j ∈ N with i ̸= j.

Lemma 4.3. The set of inter-definability equations for 〈A〉 and 〈A〉 given in Table 2 is complete.

Proof. According to Table 2, it suffices to show that 〈A〉 is not definable in the only ⊆-maximal fragment not containing it, namely, LBEDOALBEDO, which, by Lemma 3.2, turns out to be equivalent to LBEABE.

Let M1 = 〈I(R), V1〉 and M2 = 〈I(R), V2〉 be two models built on the only propositional letter p. In order to define the valuation functions V1 and V2, we take advantage of two partitions of the set R, one for M1 and the other one for M2, each of them consisting of exactly four sets that are dense in R. Formally, for j = 1, 2 and i = 1, . . . , 4, let Rij be dense in R. Moreover, for j = 1, 2, let R = ⋃4i=1 Rij and Rij ∩Ri′ j = ∅ for each i, i′ ∈ {1, 2, 3, 4} with i ̸= i′ .

For j = 1, 2, we force points in R1j (resp., R2j , R3j , R4j ) to behave in the same way with respect to the truth of p/¬p over the intervals they initiate and terminate by imposing the following constraints:

It can be easily shown that, from the given constraints, it immediately follows that:

The above constraints univocally induces the following definition of the valuation functions Vj(p) : AP → 2I(R) :

Now, let Z be the relation between (intervals of) M1 and M2 defined as follows. Two intervals [x, y] and [w, z] are Zrelated if and only if at least one of the following conditions holds:

We show that the relation Z is an LBEABE-bisimulation. It can be easily checked that every pair ([x, y], [w, z]) of Z-related intervals is such that either [x, y] ∈ V1(p) and [w, z] ∈ V2(p) or [x, y] ̸∈ V1(p) and [w, z] ̸∈ V2(p). In order to verify the forward condition, let [x, y] and [w, z] be two Z-related intervals. For each modal operator 〈X〉 of the language and each interval [x′ , y′ ] such that [x, y]RX[x′ , y′ ], we have to exhibit an interval [w′ , z′ ] such that [x′ , y′ ] and [w′ , z′ ] are Z-related, and [w, z] and [w′ , z′ ] are RX-related. We proceed case-by-case. Let 〈X〉 = 〈L〉. We must consider five sub-cases depending on the sets x′ and y′ belong to: (i) if x′ ∈ R11 ∪ R21 , then for each w′ ∈ R12 such that w′ > z, we have that, for every z′ > w′ , ([x′ , y′ ], [w′ , z′ ]) ∈ Z and [w, z]RL[w′ , z′ ] (the existence of w′ is guaranteed by rightunboundedness of R12 ); (ii) if x′ ∈ R31 and y′ ∈ R11 ∪R31 , then for each w′ , z′ such that z < w′ < z′ and w′ , z′ ∈ R32 , we have that ([x′ , y′ ], [w′ , z′ ]) ∈ Z and [w, z]RL[w′ , z′ ] (rightunboundedness of R32 ); (iii) if x′ ∈ R31 and y′ ∈ R21 ∪R41 , then for each w′ , z′ such that z < w′ < z′ , w′ ∈ R32 , and z′ ∈ R42 , we have that ([x′ , y′ ], [w′ , z′ ]) ∈ Z and [w, z]RL[w′ , z′ ] (right-unboundedness of R32 and R42 ); (iv) if x′ ∈ R41 and y′ ∈ R11 ∪ R31 , then for each w′ , z′ such that z < w′ < z′ , w′ ∈ R42 , and z′ ∈ R32 , we have that ([x′ , y′ ], [w′ , z′ ]) ∈ Z and [w, z]RL[w′ , z′ ] (right-unboundedness of R32 and R42 ); (v) if x′ ∈ R41 and y′ ∈ R21∪R41 , then for each w′ , z′ such that z < w′ < z′ and w′ , z′ ∈ R42 , we have that ([x′ , y′ ], [w′ , z′ ]) ∈ Z and [w, z]RL[w′ , z′ ] (right-unboundedness of R42 ). Assume now 〈X〉 = 〈B〉. If x ∈ R11 ∪ R21 and w ∈ R12 ∪ R22 , then for any w < z′ < z, both ([x, y′ ], [w, z′ ]) ∈ Z and [w, z]RB[w, z′ ] hold. If x ∈ Ri1 and w ∈ Ri2 , for some i ∈ {3, 4}, and y′ ∈ Rk1 , for some k ∈ {1, 2, 3, 4}, then for any w < z′ < z such that z′ ∈ Rk2 , it holds that ([x, y′ ], [w, z′ ]) ∈ Z and [w, z]RB[w, z′ ] (the existence of z′ is guaranteed by density of Rk2 in R). Finally, if x ∈ Ri1 and w ∈ Ri′ 2 for i, i′ ∈ {3, 4} with i ̸= i′ , then if y′ ∈ R11 ∪ R31 (resp., y′ ∈ R21 ∪ R41 ) for any w < z′ < z such that z′ ∈ R22 ∪ R42 (resp., z′ ∈ R12 ∪ R32 ), it holds that ([x, y′ ], [w, z′ ]) ∈ Z and [w, z]RB[w, z′ ] (density of R22 and R42 , resp., R12 and R32 , in R). The remaining cases can be dealt with in a similar way. Let us consider now two intervals [x, y] and [w, z] such that x ∈ R11 , w ∈ R12 , y ∈ R31 , and z ∈ R12 . By definition of Z, [x, y] and [w, z] are Zrelated, and by definition of V1 and V2, there exists y′ > y such that M1, [y, y′ ] ⊩ p, but there is no z′ > z such that M2, [z, z′ ] ⊩ p. This allows us to conclude that Z does not preserve the relation induced by 〈A〉, and thus 〈A〉 is not definable in LBEDOALBEDO.

A completely symmetric argument can be applied for the completeness proof of 〈A〉.

4.4 Completeness for 〈D〉, 〈D〉, 〈O〉, and 〈O〉

To deal with the modalities 〈D〉, 〈D〉, 〈O〉, and 〈O〉, we proceed as follows. We first introduce the notion of f-model, that is, for any given function f : R→Q, we define a model Mf , called f-model, whose valuation is based on f. Then, for any given pair of functions f1 and f2, we define a suitable relation Z f2 f1 between themodelsMf1 andMf2 (fromnowon, we will simply write Z when there is no ambiguity about the involved models). Finally, we specify the requirements that f1 and f2 must satisfy to make Z the bisimulation we want (these requirements vary from one modality to the other).

Lemma 4.4. The set of inter-definability equations for 〈D〉, 〈D〉, 〈O〉, and 〈O〉 given in Table 2 is complete.

Proof. We will detail the case of the modality 〈D〉. The other cases can be proved using similar arguments.

According to Table 2, 〈D〉 is definable in terms of BE. The fragments ALBOALBEDO and ALEOALBEDO are thus the only ⊆-maximal ones not featuring 〈D〉 and not containing BE. We should provide a bisimulation, not preserving the relation induced by 〈D〉, for each of these fragments, but, thanks to the symmetry of the operators, it suffices to consider only one of them, say ALBOALBEDO (by Lemma 3.2, we have that ALBOALBEDO is expressively equivalent to ABOABE). Given a function f : R → Q, we define the f-model Mf , over a language with one propositional letter p only, as the pair 〈I(R), Vf〉, where Vf : I(R) → 2AP is defined as follows: [x, y] ∈ Vf(p) def ⇔ y ≥ f(x). For any given pair of functions f1 and f2 (from R to Q), the relation Z is defined as follows:

where u ≡ v def ⇔ u ∈ Q iff v ∈ Q and [u, u′ ] ≡l [v, v′ ] def ⇔ u′ ∼ f1(u) and v′ ∼ f2(v), for ∼∈ {<,=,>}. Finally, the following constraints are imposed on f (if we replace 〈D〉 by one of the other modalities, the constraints must be suitably replaced as well): (i) for every x ∈ R, f(x) > x, (ii) for every x ∈ Q, both f -1 (x) ∩Q and f -1 (x) ∩Q are left-unbounded (notice that surjectivity of f immediately follows), and (iii) for every x, y ∈ R, if x < y, then there exists u1 ∈ Q (resp., u2 ∈ Q) such that x < u1 < y (resp., x < u2 < y) and y < f(u1) (resp., y < f(u2)).

Now, we show that if both f1 and f2 satisfy the above conditions, then Z is an ABOABE-bisimulation between Mf1 and Mf2 . Let [x, y] and [w, z] be two Z-related intervals. By definition, y ∼ f1(x) and z ∼ f2(w) for some ∼∈ {<,=, >}. If ∼∈ {=,>}, then both [x, y] and [w, z] satisfy p; otherwise, both of them satisfy ¬p. The local condition is thus satisfied. As for the forward condition, let [x, y] and [x′ , y′ ] be two intervals in Mf1 and [w, z] an interval in Mf2 . We have to prove that if [x, y] and [w, z] are Z-related, then, for each modal operator 〈X〉 of ABOABE such that [x, y]RX[x′ , y′ ], there exists an interval [w′ , z′ ] such that [x′ , y′ ] and [w′ , z′ ] are Z-related and [w, z]RX[w′ , z′ ]. Once more, we proceed case-by-case. For the sake of brevity, we only detail the case of 〈A〉. The other modalities can also be dealt with by exploiting the requirements for the functions f1 and f2 in a suitable way. Let 〈X〉 = 〈A〉. By definition of 〈A〉, x′ = y and we are forced to choose w′ = z. By y ≡ z, it immediately follows x′ ≡ w′ . We must find a point z′ > z such that y′ ≡ z′ and both y′ ∼ f1(y) and z′ ∼ f2(z) for some ∼∈ {<,=,>}. Let us suppose that y′ < f1(y). In such a case, we choose a point z′ such that z < z′ < f2(z) and y′ ≡ z′ . The existence of such a point is guaranteed by condition (i) on f2 and by the density of Q and Q in R. Otherwise, if y′ = f1(y), we choose z′ = f2(z). By definition of f1 and f2 (the codomain of f1 and f2 is Q), both y′ and z′ belong to Q and thus y′ ≡ z′ . Finally, if y′ > f1(y), we choose z′ > f2(z) such that y′ ≡ z′ . The existence of such a point is guaranteed by right-unboundedness of Q and Q. Satisfaction of the backward condition for all modalities can be checked in a similar way.

To complete the proof, we exhibit two functions that meet the requirements we have imposed to f1 and f2, but do not preserve the relation induced by 〈D〉. Let P(Q) = {Qq | q ∈ Q} and P(Q) = {Qq | q ∈ Q} be infinite and countable partitions of Q and Q, respectively, such that for every q ∈ Q, both Qq and Qq are dense in R. For every q ∈ Q, let Rq = Qq ∪ Qq. We define a function g : R → Q that maps every real number x to the index q (a rational number) of the class Rq it belongs to. Formally, for every x ∈ R, g(x) = q, where q ∈ Q is the unique rational number such that x ∈ Rq. The two functions f1 : R → Q and f2 : R → Q are defined as follows:

It is not difficult to check that the above-defined functions meet the requirements for f1 and f2, and thus Z is an ABOABE-bisimulation. On the other hand, Z does not preserve the relation induced by 〈D〉. Consider the interval [0, 3] in Mf1 and the interval [0, 3] in Mf2 . It is immediate to see that these two intervals are Z-related. However, Mf1 , [0, 3] ⊩ 〈D〉p (as Mf1 , [1, 2] ⊩ p), but Mf2 , [0, 3] ⊩ ¬〈D〉p. This allows us to conclude that 〈D〉 is not definable in the fragment ALBOALBEDO.

4.5 Harvest

The proof of Theorem 3.1 follows now immediately.

We have used the equations in Table 2 as the basis of a simple program that identifies and counts all expressively different fragments of HS with respect to the strict semantics. Using that program, we have found that, under our assumptions (strict semantics, over the class of all linear orders) there are exactly 1347 genuine, that is, expressively different, fragments out of 212 = 4096 different subsets of HS-operators.

5 Conclusions

In this paper, we have obtained a sound, complete, and optimal set of inter-definability equations among all modal operators in HS, thus providing a characterization of the relative expressive power of all interval logics definable as fragments of HS. Such a classification has a number of important applications. As an example, it allows one to properly identify the (small) set of HS fragments for which the decidability of the satisfiability problem is still an open problem.

It should be emphasized that the set of inter-definability equations listed in Table 2 and the resulting classification do not apply if the non-strict semantics is considered. For instance, if the non-strict semantics is assumed, then, as shown in [Venema, 1990], 〈A〉 (resp., 〈A〉) can be defined in BE (resp., BE). Also, if the semantics is restricted to specific classes of linear orders, the completeness of the set of equations in Table 2 is no longer guaranteed. For instance, in discrete linear orders, 〈A〉 can be defined in BE: 〈A〉p ≡ ϕ(p) ∨ 〈E〉ϕ(p), where ϕ(p) is a shorthand for [E]⊥∧ 〈B〉([E][E]⊥∧ 〈E〉(p∨ 〈B〉p)); likewise, 〈A〉 is definable in BE. As another example, in dense linear orders, 〈L〉 can be defined in DO: 〈L〉p ≡ 〈O〉(〈O〉⊤ ∧ [O](〈O〉p ∨ 〈D〉p∨〈D〉〈O〉p)); likewise, 〈L〉 is definable in DO. (In view of these inter-definabilities, Lemma 4.1 cannot be proved by using bisimulation between models over the reals.)

The classification of the expressiveness of HS fragments with respect to the non-strict semantics, as well as over specific classes of linear orders, is currently under investigation and will be reported in a forthcoming publication.