# Reasoning with Time Intervals: A Logical and Computational Perspective

Authors: Guido Sciavicco
Journal: ISRN Artificial Intelligence
 (2012)

---

## Abstract

The role of time in artificial intelligence is extremely important. Interval-based temporal reasoning can be seen as a generalization of the classical point-based one, and the first results in this field date back to Hamblin (1972) and Benhtem (1991) from the philosophical point of view, to Allen (1983) from the algebraic and first-order one, and to Halpern and Shoham (1991) from the modal logic one. Without purporting to provide a comprehensive survey of the field, we take the reader to a journey through the main developments in modal and first-order interval temporal reasoning over the past ten years and outline some landmark results on expressiveness and (un)decidability of the satisfiability problem for the family of modal interval logics.


---

## Body

## 1. Introduction

Temporal reasoning is pervasive in many areas of computer science and artificial intelligence, such as, for instance, formal specification and verification of sequential, concurrent, and reactive real-time systems, temporal knowledge representation, temporal planning and maintenance, theories of actions, events, and fluents, temporal databases, and natural language analysis and processing. In most cases,time instants (points) are assumed to be the basic ontological temporal entities. However, often “durationless” time points are not suitable to properly reason about real-world events, which have an intrinsic duration. Indeed, many practical aspects of temporality occurring for instance in hardware specifications, real-time processes, and progressive tenses in natural language are better modeled and dealt with if the underlying temporal ontology is based on time intervals (periods), rather than instants, as the primitive entities. As an example, consider a typical safety requirement of traffic light systems at road intersections as the following one. “For every time interval I during which the green light is on for the traffic on either road at the intersection, the green light must be continuously off and the red light must be continuously on for the traffic on the other intersecting road, for a time interval beginning strictly before and ending strictly after I."The nature of time and, in particular, the discussion whether time instants or time intervals should be regarded as the primary objects of temporal ontology have always been a hotly debatable philosophical theme, and the philosophical roots of interval-based temporal reasoning can be dated back to Zeno and Aristotle [1]. Zeno already noted that in an interval-based setting, several of his paradoxes “disappear” [2, 3], like the flying arrow paradox “if at each instant the flying arrow stands still, how is movement possible?” and the dividing instant dilemma (“if the light is on and it is turned off, what is its state at the instant between the two events?”). Of course, the two types of temporal ontologies are closely related and technically reducible to each other: on one hand, time intervals can be determined by pairs of time instants; on the other hand, a time instant can be construed as a degenerated interval (point interval) whose left and right endpoints coincide. While these reductions can be used to reconcile the different philosophical and ontological standpoints, they do not resolve the main semantic issue arising when developing logical formalisms for capturing temporal reasoning: should formulae in the given logical language be interpreted as referring to instants or to intervals? The possible natural answers to this question lead to (at least) three reasonable alternatives, giving rise to point-based logics, interval-based logics, and mixed, two-sorted logics, respectively, where points and intervals are considered as separate sorts on a par and formulae for both sorts are constructed. This exposition is devoted exclusively to the second alternative. The literature on point-based temporal logics is abundant and will not be discussed here. The reader is referred to [2] for a detailed philosophical-logical comparative discussion of both approaches, while a recent study and technical exploration of the two-sorted approach can be found in [4]. Nevertheless, the most recent studies show how the mixed approach is actually more suitable than the other two alternatives, as from a mixed comprehensive language one can tailor the most adapted sublanguage to solve a particular problem at hand. Therefore, while we limit this survey to intervals only, we do so by excluding from the semantics degenerate intervals with coincident endpoints and restricting our attention to pure interval temporal logics only.Interval temporal reasoning can be declined into a number of different flavors. Nevertheless, all formal approaches share a common root, that is, thefirst-order characterization of the languages being studied, about which we will give a rather complete survey. Over an ideal path from “very expressive and very complex” to “less expressive and computationally simpler,” the first-order level sits at the left extreme; going down from left to right, we encounter the modal logic level, where relations are embedded into modal operators, and the use of quantifier is relativized to the relations (see, e.g., [5]). Modal interval temporal logics are the very core of this survey, and, in particular, the modal logic of Allen’s relations, also known as HS, first introduced by Halpern and Shoham [6], and its fragments, under the assumption that point intervals are excluded from the semantics. An impressive amount of work has been recently done in this area, and we are now in the position of asserting that more than the 95% of all fragments of HS has been studied from the decidability/undecidability/expressive power point of view. But modal interval temporal logics do not end with HS. Although this paper will not include these alternative tools into account, let us remind them here for the interested reader. While the systematic logical study of purely interval-based temporal reasoning started with the seminal work of Halpern and Shoham, Venema [7] introduced and studied the even more expressive interval logic CDT involving binary modal operators associated with the ternary relation chop (C) and its two residual relations D and T. Over the single relation C, Moszkowski proposed in [8] the propositional interval temporal logic (PITL), and its first-order extension ITL, obtaining one of the earliest decidability results by means of the so-called locality principle. Such a principle has the effect of reducing the interval semantics to a point-based ones, and, even if we recognize its importance and suitability for a number of application, we tend to consider this choice rather tangential to the pure interval reasoning which we are interested in. From PITL and ITL, a family of formal systems known as duration calculi, particularly suitable for specification and verification of real-time processes in computer science [9–12], has been developed. Back to pure interval reasoning, the main problem in modal interval temporal logics is the decidability/undecidability of its satisfiability problem; as CDT is strictly more expressive than HS [7], this higher expressivity cuts CDT out irremediably, as HS itself is already undecidable over every interesting class of linearly ordered sets [6]. The same holds for nearly every proper fragment of CDT with C, D, or T only [13]. On the right extreme of our ideal path, we find the algebraic (or constraint-based) approaches. From the logical point of view, a network of constraints can be seen as a purely existential first-order formula. Therefore, its satisfiability problem is, in general, decidable, and, typically, the complexity of the problems associated with this approach is NP or below. More importantly, constraint-based temporal reasoning has been fully explored in the literature, and it is already textbooks’ material in artificial intelligence (see, e.g., [14]). Concluding, the research in this particular subfield is still very active, but, on one side, it is centered in finding more and more efficient algorithms for problems already known to be decidable, and, on the other side, their main aspects are implementative and algorithmic, but not logical.This paper aims to highlight the main logical aspects of interval temporal reasoning and reviewing, in particular, the last 10 years of research in these aspects. We will start with a motivating section (Section2) that points to justify the study of interval temporal reasoning as an artificial intelligence tool. Then, we will focus on more technical aspects, from the first-order roots of interval languages (Section 3) to modal languages for interval reasoning with binary relations (Section 4). We will then conclude (Section 5) this review by pointing out which are, in our view, the most interesting open problems and research challenges. The addendum (Section 6) is devoted to some technical details for the interested reader: we fully prove there three representative results mentioned in the paper.


## 2.  Motivation

The role of logic in artificial intelligence is, in essence, to allow one to formally express the knowledge and reason about it. In principle, for a given problemP, one has to modulate the choice of the appropriate language under the following two parameters: expressive power (the ability of expressing the conditions of P) and computational complexity (the ability of reasoning about the formulas of the language). Such two parameters are not independent: as a general rule, the more expressive power, the higher computational complexity; the ideal choice maximizes the expressive power while keeps low enough the complexity of the logic, and, in particular, the complexity of its satisfiability (and validity) problem. So, in general, one cannot use first- (and higher-) order logic(s), as its satisfiability problem is undecidable, and, at the same time, simple propositional logic (and fragments of it such as Horn clauses), whose complexity is only NP (and lower), is usually not enough. Therefore, the main task for applied logicians is to find an expressive enough, yet decidable (and, possibly, in an efficient way) language that suits the problem at hand, and in interval temporal reasoning we follow exactly this scheme. As we have already remarked, the study of first-order logic for interval temporal reasoning is not useless, as it gives us more information on the relations, their expressive power, and, in principle, allows us to have a better understanding of the problems. But the most interesting results belong to the middle class (see Section 1), that is, modal (temporal) logics, as represented in Figure 1, as we will see some interesting and previously unexpected decidability results “popped out” in the recent past. Purely existential (constraint-based) reasoning, as well as pure propositional reasoning, are, on the other hand, very well-studied, and we choose not to include it in this paper.Figure 1
Expressive power versus computational complexity in interval temporal reasoning.Interval temporal reasoning is literally ubiquitous in artificial intelligence. Think for example to temporal databases [15, 16], where the temporal attributes (e.g., valid time, event time, etc.) are inherently nonpunctual, and, in some cases, it makes no sense to reduce the intervals to the set of its points, as shown, for example, in [17]. In temporal databases, we need interval-based constraint reasoning to check whether or not a given table is temporally consistent, but we need logical temporal reasoning to formulate, check, and execute temporal queries, and to design temporal data mining algorithms. As another example, logical reasoning has been applied to help the diagnostic process in medicine; typical statements from the medical context take into account the temporal aspects of drugs’ intake, symptoms’ appearance and duration, and so on. Interval temporal reasoning is therefore the perfect logical tool to formalize such statements [18–20]. But the clearest example of how (logical) interval temporal reasoning can be useful in artificial intelligence is probably automated planning. Automated planning is a field of artificial intelligence that studies methods and algorithms to find action sequences (plans) to achieve a given goal, under suitable constraints [21]. One of the most relevant approaches in the literature is the so-called planning as satisfiability paradigm, where a planning problem is encoded by some logical formula that models the rules and the constraints to generate plans, in such a way that any model of the formula is a valid solution of the problem. The first attempts at this paradigm were based on propositional logics [22], while the most recent ones use linear (point-based) temporal logic as the logic to encode planning problems [23], since it allows a natural representation of a world that changes over time. To standardize planning domain and problem description languages, the planning domain definition language (PDDL) was introduced in 1998, and in 2004 PDDL was extended to the version 2.1, which introduces, among the other extensions, an explicit model of concurrency with durative actions, that are actions occurring over a time interval. To simplify the algorithmic treatment of the problem, durative actions in PDDL are modeled as pair of start/stop instantaneous actions, even though this ignores the realities of modeling and execution for complex systems [24]. Let us consider here a complete example of automatic planning.Given an autonomous robot, themotion planning problem focuses on generating trajectories which reach a given goal while avoiding obstacles. Unlike the classical approach that has been used to solve this problem, mainly concentrated on point-based temporal logics and model checking techniques (see, e.g., [25]), we state the problem as a satisfiability problem. Given a formula Sys describing all trajectories of the robot, and a formula Req describing the requirements, we have that the formula Sys∧Req is satisfiable if and only if there exists a feasible trajectory for the robot, that is, a trajectory respecting the requirements. In [25], the robot motion is defined by a finite transition system D=(Q,q0,→D,hD) where Q is a finite set of cells where the robot can be (and, obviously, the robot will be in any given cell during a nonzero interval of time), q0 is the initial cell, →D⊆Q×Q is the dynamics, and hD:Q↦Π is an observation map that assigns a set of propositional letters in Π to every cell. Now, the formula Sys can be thought as the conjunction of the following requirements: (i)
“The first state (i.e., the current interval) isq0”;(ii)
“If an interval of time is labeled with the stateq, thenqlabels also every sub-interval of it”;(iii)
“There cannot be an interval labeled withq  and followed by an interval labeled withq'  unless(q,q′)∈→D”;(iv)
“There cannot be an interval labeled withq  and  q'  when  q≠q'”.As an example of a possible specification, consider [25, Example 1];(i)
“Visit arear2, then arear3, then arear4and, finally, return to arear1  while avoiding areasr2andr3”.It should be clear now that:(1) logical reasoning is essential in artificial intelligence and (2) interval temporal reasoning can be easily applied to a number of fields, including automatic planning. At this point, besides choosing the appropriate expressive level (as previously discussed), there is a number of parameters that we can modulate. Among the most important ones, we have (1)
the class of (usually linear) orders over which we interpret the set of formulas (i.e., the class of all linear orders, the class of all strongly discrete linear orders, etc.);(2)
the set of interval relations allowed in the language. Thus, in front of a new problem, we can choose the correct language by setting the expressive power level that we need, and, orthogonally, the correct semantical framework. It should be noticed that choosing a particular set of relations and a particular class of orders also heavily influences the computational properties of the language, as we will see in detail in Section 4.From a more philosophical point of view, we must observe that some languages allow us to specify different relationships between the truth values of assertions over intervals and their components. In [24], the authors observe that the truth of a proposition over an interval is sometimes related to its truth over other intervals, and they classify propositions depending on the relationships that have to be considered in order to determine their truth. An assertion φ is called downward hereditary if whenever it holds over an interval it holds over all of its subintervals, possibly excluding the two endpoints; for instance, “John played less than forty minutes" is downward hereditary. Symmetrically, an assertion is upward hereditary if whenever it holds over all the subintervals of a given interval, possibly excluding the two endpoints, it also holds over the given interval itself; for example, “The airplane flies at 35000 feet" is upward hereditary. Moreover, an assertion is said to be liquid if it is both downward hereditary and upward hereditary (e.g., “the room is empty"), and concatenable if whenever it holds over two consecutive intervals it holds also over their union (e.g., “John traveled an even number of miles." Finally, it is gestalt if whenever it never holds over two intervals one of which properly contains the other, as in “Exactly six minutes passed," and it is solid if whenever it never holds over two properly overlapping intervals, as “The plane executed the LANDING procedure (from start to finish)." While in first-order logic basically any of the above relationships can be expressed, when we will turn our attention to the modal framework, the question of which language allows us to express what will be a nontrivial one.


## 3. First-Order Interval Temporal Reasoning

In general, reasoning at the first-order level is undecidable, even if there are a few exceptions. Ever since it has been shown that the satisfiability problem for the full language is undecidable, a great effort has been made in order to identify more and more expressive decidable fragments. At least three different strategies have been explored:(1) to limit the number of variables of the language; (2) to limit the allowed types of formula by relativizing quantification (guarded fragments); (3) to limit the structure and the shape of the quantifier prefix. First-order logics with a limited number of variables have been explored in connection with interval temporal logics; most notably, the equivalence in expressive power between the two-variable fragment of first-order logic over linear orders (shown to be NEXPTIME-complete in [26]) has made it possible to prove decidability of the fragment of HS (introduced earlier in this paper) that only features Allen’s relations meets and met by, also known as Propositional Neighborhood Logic (PNL; see Section 4), before specific decision procedures were devised for it [27]. Guarded fragments of first-order logics have been shown to be extremely useful to understand and to explain the good computational properties of modal logics [5]; however, to the best of our knowledge, they turned out to be almost useless to tackle interval-based temporal logics, with the main reason being the fact that transitive guards, necessary to force the structures to be ordered, preserve decidability only when at most two variables are allowed, while interval properties (when intervals are interpreted as pairs of points) are mostly three-variable. The third strategy has been used, to the best of our knowledge, only in a limited form, specifically, to devise a decidable fragment of the modal logic CDT [28].Coming back to pure first-order interval reasoning, the study of interval relations and their expressive power is important to understand interval reasoning and its properties, more than from a computational point of view. Let us consider a linearly ordered set𝔻=〈D,<〉. An interval over a linear order is defined as an ordered pair [a,b] such that a<b  (as recalled, the non-strict semantics only requires that a≤b, thus including degenerate objects of the type [a,a]). The set of all intervals on 𝔻 is denoted by 𝕀(𝔻). The variety of all possible binary relations between intervals has been studied by Allen [29]. There are thirteen of Allen’s relations, including equality. Table 1 gives and illustrates the definitions of 6 of these relations, the other 7 consisting of the inverses of those illustrated and equality (which is of course equal to its own inverse). For each relation r, its inverse is denoted by ri. Since we will always be assuming equality in our language, we will only need to deal explicitly with the other twelve relations. We denote this set by AL={m,b,s,f,d,o,mi,bi,si,fi,di,oi}. For the sake of completeness, let us recall that this notation has been recently replaced by a more flexible one that allows one to easily deal with points too and with intersort relations [4]; nevertheless, in this paper, we limit ourselves to pure interval reasoning.Table 1
Allen’s interval relations, excluding equality.
[
a
,
b
]
m
[
c
,
d
]
⇔
b
=
c
[
a
,
b
]
b
[
c
,
d
]
⇔
b
<
c
[
c
,
d
]
s
[
a
,
b
]
⇔
a
=
c
,
d
<
b
[
c
,
d
]
f
[
a
,
b
]
⇔
b
=
d
,
a
<
c
[
c
,
d
]
d
[
a
,
b
]
⇔
a
<
c
,
d
<
b
[
a
,
b
]
o
[
c
,
d
]
⇔
a
<
c
<
b
<
dGiven a subsetS={r1,…,rn}⊆AL of Allen’s relations, a concrete interval structure of signatureS is a relational structure ℐ=〈𝕀(𝔻),r1,r2,…,rn〉, where each ri is defined on 𝕀(𝔻) according to Table 1. ℐ is further said to be of the classC when 𝔻 belongs to the specific class of linearly ordered sets C. Since all thirteen of Allen’s relations are already implicit in 𝕀(𝔻), we will often simply write 〈𝔻,𝕀(𝔻)〉 for a concrete interval structure 〈𝕀(𝔻),r1,r2,…,rn〉. This is in accordance with the standard usage in much of the literature on interval temporal logics. We denote by FO+S the language of first-order logic with equality and relation symbols corresponding to the relations in S. Suppose now that, in this setting, we want to express some of the requirement specified in Section 3. Assertions over intervals become unary relational symbols, so that, for example, saying “The current state isq0” becomes Q0(x), and x is a free first-order variable (an interval) over which we evaluate the formula. Expressing “If an interval of time is labeled with the stateq, thenqlabels also every subinterval of it” can be done by means of the formula ∀y(Q(y)→∀z((d(z,y)∨s(z,y)∨f(z,y))→Q(z))). It is clear that the following questions now arise.(1)
If we consider the abstract language (intervals are first-order variables, and interval relations are binary relations), are we sure that we are talking precisely about the intended concrete structures where intervals are pairs of points and all relations can be expressed using the ordering relation?(2)
In the abstract language, which relations are really necessary and which ones can be expressed in terms of others? The first question is known as representation problem, and it is solved by a representation theorem. In the relevant literature, we find a number of representation theorems: Benthem [2], over rationals and with the interval relations during and before, Allen and Hayes [30], for the dense unbounded case without point intervals and for the relation meets, Ladkin [31], for point-based structures with the quaternary relation chop, Venema [32], for structures with the relations starts and finishes, Goranko et al. [33], that generalizes the results for structures with meets and met by, and Coetzee [34] for dense structure with overlaps and meets. Clearly, if two sets of interval relations give rise to expressively equivalent languages, two separate representations theorems for them are not needed. To answer the second question we need to refer to more recent results. In [35], this problem has been considered, and, in particular, it has been studied under different hypothesis for the underlying structure. In the context of linearly ordered sets, the following classes have been considered (among others):(1)
the class of all linearly ordered sets;(2)
the class of all dense linearly ordered sets;(3)
the class of all (weakly) discrete linearly ordered sets. To be precise, by dense linear order we mean a structure such that, for every pair a<b, there exists c such that a<c<b, and by (weakly) discrete (in contrast with strongly discrete) we mean that in the structure every point with a successor/predecessor has an immediate one (resp., such that there exists a finite number of points in between any two distinct points). While the expressive power of interval relations is identical over strongly and weakly discrete linear orders (and, as it turns out, in the finite case too), the properties of modal logics over such classes are different, as we will see in Section 4. Thus, in this section, we will distinguish among the class Lin of all linearly ordered sets, the class Den of all dense linearly ordered sets, and the class Wdis of all (weakly) discrete linearly ordered sets, which we will now refer to as simply discrete. As a final note, we should recall that also the class of all strongly discrete linearly ordered sets includes, as subclasses, the class of all linearly ordered sets based on ℕ and those based on ℤ, among others; moreover, the class Wdis includes as subclasses the class of all linearly ordered sets based on ℕ+ℕ and those based on ℤ+ℤ, among others. Finally, the class of all linearly ordered sets based on ℝ is also interesting (at the modal logic level), but the decidability results specific for this class are more complicated and scarce than the others.


### 3.1. Classification

The results in this part are merely technical. Let us review them all here, with a quick intuition of the proofs; we will give some technical details in the last section of the paper for the interested reader.All classifications known in this setting are displayed in Tables2 and 3. Notice that there are no differences between Lin and Wdis, here. To prove these results, we proceed as follows. First, we give a notion of definability in a given extension FO+S of first-order logic with S⊆AL, relativized to a specific class C∈{Lin,Den,Wdis}. Then, we observe that if S contains a certain relation r, then its inverse relation ri is always definable; thus we limit our attention to the subset {m,b,s,f,d,o} of AL, called AL+. We then say that S is complete overC if and only if FO+S defines r for all r∈AL+ and is a minimal complete set overC, denoted by mcs (resp., maximally incomplete set overC, denoted by MIS) if and only if it is complete (resp., incomplete) over C, and every proper subset (resp., every strict superset) of S is incomplete (resp., complete) over the same class. Finally, we turn our attention to specific classes.Table 2
Minimal complete and maximal incomplete sets in Lin and Wdis.
MISs
mcss
{
s
}
{
m
}
{
f
}
{
o
,
s
}
{
o
,
d
,
b
}
{
o
,
f
}
{
d
,
s
}
{
d
,
f
}
{
s
,
f
}
{
s
,
b
}
{
f
,
b
}Table 3
Minimal complete and maximal incomplete sets in Den.
MISs
mcss
{
s
}
{
m
}
{
f
}
{
o
}
{
d
}
{
b
}
{
d
,
s
}
{
d
,
f
}
{
s
,
f
}OverLin and Wdis (Table 2), where the results are identical, we first notice that {m} is complete (and clearly it is minimal), by simply recalling Allen and Hayes’ result [30]. Then, we prove the completeness of all sets in the right-hand column of the table, by simply devising the correct definitions of the relations that are not included. After that, we show that the three sets {s},{f}, and {o,d,b} are incomplete (notice that all subsets of an incomplete set are incomplete); to do so, for each extension of first-order logic (say, e.g., FO+{s}), we prove by bisimulation that there exists at least one relation which cannot be expressed. Finally, we observe that as each proper subset S′ of any set S from the right-hand column is incomplete and that each superset S′′ of any set of the left-hand column is either complete or contains a complete set,   and we are done. Also, notice that completeness results on a class C of semantic structures are also completeness result on every subclass C′, and every incompleteness result on a class C′ also applies to every superclass C. This last observation, plus some easy variations on the results in the class Lin, specifically, concerning the incompleteness of {s} and {f}, allows us to devise the classifications over Wdis. When we turn our attention on Den, we simply observe, again, that every complete set over Lin is also complete over Den. Thus the completeness of {m}, {d,s}, {d,f}, and {s,f} over Den follows immediately. The cases {o} and {b} have to be treated in a specific way, but it turns out that the technical details are not so different from other cases. The incompleteness of {s} and {f} can be proved using the same argument as in the case of all linearly ordered sets, and only a specific bisimulation is needed for the case {d}.


### 3.2. Relative Expressivity

The above results allowed us to identify all minimally complete and maximally incomplete fragments of first-order logic with equality enriched with Allen’s interval relations in the class of all linearly ordered sets. We still have not completely answered the question of which are the expressively different fragments in this case, and we will now do so.We first prove that overLin and Wdis there are exactly 10 expressively different fragments of FO+AL, namely {s}, {f}, {o}, {d}, {b}, {o,d}, {o,b}, {d,b}, {o,d,b}, and {m}. The set {m} is complete and hence represents all complete fragments. The fragments {s}, {f}, and {o,d,b} are maximally incomplete and hence pairwise incomparable among each other and also different from {m}. The fragments {o}, {d}, {o,d}, {o,b}, and {d,b} are related as illustrated in the Hasse diagram in Figure 2. In other words, among these fragments the relative expressivity is simply given by set containment. It remains to prove that no two of them are expressively equivalent, by suitable bisimulations. After that, over Den, there are exactly 4 expressively different sets, namely {s}, {f}, {d}, and {m}. This is essentially a corollary of the classification results. Indeed, all complete sets are expressively equivalent, by definition, and are thus all represented by {m}. Moreover, all maximally incomplete singletons must be incomparable. Since all subsets with two or more elements are complete, this covers all cases.Figure 2
Expressively different fragments ofFO+AL+ in Lin and Wdis.


### 3.3. Remarks

In this section, we have considered extensions of first-order logic with equality with subsets of Allan’s interval relations. We obtained a complete classification of these fragments in terms of relative expressivity when interpreted over the classes of interval structures based on all, all dense, and all discrete linear orders, respectively, (in the class of all strongly discrete linearly ordered sets the results are identical). Our results are specific to the pure semantics; that is, point intervals are excluded (as recalled in Section1). Very recently, in a more general context of interval reasoning with points and intervals (treated as two different sorts), similar results are being obtained, but, in that case, a closer analysis of the relations is needed, since mixing points and intervals at the algebraic level raises the problem of obtaining a set of mutually exclusive relations. As a consequence of this work, we now have a complete view of the open representation problems in the strict semantics. Another natural question to ask is what happens when equality is not assumed but treated on the same footing as the other Allen’s relations. Finally, one might ask what happens in terms of expressive power when the first order language is limited, say, in the number of variables at disposal, or to some well-defined prefix-quantifier fragment.


## 3.1. Classification

The results in this part are merely technical. Let us review them all here, with a quick intuition of the proofs; we will give some technical details in the last section of the paper for the interested reader.All classifications known in this setting are displayed in Tables2 and 3. Notice that there are no differences between Lin and Wdis, here. To prove these results, we proceed as follows. First, we give a notion of definability in a given extension FO+S of first-order logic with S⊆AL, relativized to a specific class C∈{Lin,Den,Wdis}. Then, we observe that if S contains a certain relation r, then its inverse relation ri is always definable; thus we limit our attention to the subset {m,b,s,f,d,o} of AL, called AL+. We then say that S is complete overC if and only if FO+S defines r for all r∈AL+ and is a minimal complete set overC, denoted by mcs (resp., maximally incomplete set overC, denoted by MIS) if and only if it is complete (resp., incomplete) over C, and every proper subset (resp., every strict superset) of S is incomplete (resp., complete) over the same class. Finally, we turn our attention to specific classes.Table 2
Minimal complete and maximal incomplete sets in Lin and Wdis.
MISs
mcss
{
s
}
{
m
}
{
f
}
{
o
,
s
}
{
o
,
d
,
b
}
{
o
,
f
}
{
d
,
s
}
{
d
,
f
}
{
s
,
f
}
{
s
,
b
}
{
f
,
b
}Table 3
Minimal complete and maximal incomplete sets in Den.
MISs
mcss
{
s
}
{
m
}
{
f
}
{
o
}
{
d
}
{
b
}
{
d
,
s
}
{
d
,
f
}
{
s
,
f
}OverLin and Wdis (Table 2), where the results are identical, we first notice that {m} is complete (and clearly it is minimal), by simply recalling Allen and Hayes’ result [30]. Then, we prove the completeness of all sets in the right-hand column of the table, by simply devising the correct definitions of the relations that are not included. After that, we show that the three sets {s},{f}, and {o,d,b} are incomplete (notice that all subsets of an incomplete set are incomplete); to do so, for each extension of first-order logic (say, e.g., FO+{s}), we prove by bisimulation that there exists at least one relation which cannot be expressed. Finally, we observe that as each proper subset S′ of any set S from the right-hand column is incomplete and that each superset S′′ of any set of the left-hand column is either complete or contains a complete set,   and we are done. Also, notice that completeness results on a class C of semantic structures are also completeness result on every subclass C′, and every incompleteness result on a class C′ also applies to every superclass C. This last observation, plus some easy variations on the results in the class Lin, specifically, concerning the incompleteness of {s} and {f}, allows us to devise the classifications over Wdis. When we turn our attention on Den, we simply observe, again, that every complete set over Lin is also complete over Den. Thus the completeness of {m}, {d,s}, {d,f}, and {s,f} over Den follows immediately. The cases {o} and {b} have to be treated in a specific way, but it turns out that the technical details are not so different from other cases. The incompleteness of {s} and {f} can be proved using the same argument as in the case of all linearly ordered sets, and only a specific bisimulation is needed for the case {d}.


## 3.2. Relative Expressivity

The above results allowed us to identify all minimally complete and maximally incomplete fragments of first-order logic with equality enriched with Allen’s interval relations in the class of all linearly ordered sets. We still have not completely answered the question of which are the expressively different fragments in this case, and we will now do so.We first prove that overLin and Wdis there are exactly 10 expressively different fragments of FO+AL, namely {s}, {f}, {o}, {d}, {b}, {o,d}, {o,b}, {d,b}, {o,d,b}, and {m}. The set {m} is complete and hence represents all complete fragments. The fragments {s}, {f}, and {o,d,b} are maximally incomplete and hence pairwise incomparable among each other and also different from {m}. The fragments {o}, {d}, {o,d}, {o,b}, and {d,b} are related as illustrated in the Hasse diagram in Figure 2. In other words, among these fragments the relative expressivity is simply given by set containment. It remains to prove that no two of them are expressively equivalent, by suitable bisimulations. After that, over Den, there are exactly 4 expressively different sets, namely {s}, {f}, {d}, and {m}. This is essentially a corollary of the classification results. Indeed, all complete sets are expressively equivalent, by definition, and are thus all represented by {m}. Moreover, all maximally incomplete singletons must be incomparable. Since all subsets with two or more elements are complete, this covers all cases.Figure 2
Expressively different fragments ofFO+AL+ in Lin and Wdis.


## 3.3. Remarks

In this section, we have considered extensions of first-order logic with equality with subsets of Allan’s interval relations. We obtained a complete classification of these fragments in terms of relative expressivity when interpreted over the classes of interval structures based on all, all dense, and all discrete linear orders, respectively, (in the class of all strongly discrete linearly ordered sets the results are identical). Our results are specific to the pure semantics; that is, point intervals are excluded (as recalled in Section1). Very recently, in a more general context of interval reasoning with points and intervals (treated as two different sorts), similar results are being obtained, but, in that case, a closer analysis of the relations is needed, since mixing points and intervals at the algebraic level raises the problem of obtaining a set of mutually exclusive relations. As a consequence of this work, we now have a complete view of the open representation problems in the strict semantics. Another natural question to ask is what happens when equality is not assumed but treated on the same footing as the other Allen’s relations. Finally, one might ask what happens in terms of expressive power when the first order language is limited, say, in the number of variables at disposal, or to some well-defined prefix-quantifier fragment.


## 4. Modal Interval Temporal Reasoning

Apropositional modal logic can be thought as an extension of classical propositional logic in which each proposition p is not just true or false, but its truth value depends on the world or state in which it is evaluated. Such worlds are collected into a set W, and the relations between them tell us which world is accessible from which one. Modal logic can therefore be seen as the logic of directed graphs. Depending on how we interpret such a graph, we obtain a particular logic. As for example, worlds can be seen as moments of times and the accessibility relation as the next relation between them; in this particular setting, now is the current world, and sometimes in the future is any world reachable through the irreflexive closure of the accessibility relation. The accessibility relation does not need to be unique, and, therefore, in general, the syntax of a propositional modal logic is
(1)φ::=p|¬φ|φ∨ψ|⋄1φ|⋯|⋄nφ|,
where each ⋄i corresponds to the accessibility relation Ri. The other propositional connectives can be seen as shortcuts; moreover, the formula ¬⋄i¬φ is usually abbreviated by □iφ. From the semantical point of view, we consider a structure of the type M=〈W,R1,R2,…,Rn,V〉, where W is the set of worlds, each Ri is a subset of W×W, and V maps each propositional letter to the subset of W in which it is true. So, the truth function, denoted by ⊩, is relative to a specific world w, and it is(i)
M,w⊩p if and only if w∈V(p);(ii)
M,w⊩¬φ if and only if it is not the case that M,w⊩φ;(iii)
M,w⊩φ∨ψ if and only if M,w⊩φ or M,w⊩ψ;(iv)
M,w⊩⋄iφ if and only if there exists a world v such that Ri(v,w) and that M,v⊩ψ. It is clear that the properties and the nature of each Ri are the main parameter that influence, on one side, what problems can we model with a specific modal logic and, on the other side, its computational properties. A complete reference for modal logic in general, is [36]. We are interested here in a specific class of modal logics, that go under the generic name of temporal logics, characterized by the presence of one or more relations Ri, each one of which is a partial order. Point-based temporal logics have been successfully used in various computer science areas, including both well-established areas, like program specification and verification, knowledge representation and reasoning, and temporal databases, and emerging areas, like multiagent systems and bioinformatics. But here we are interested in interval temporal logics.


### 4.1. Modal Interval Temporal Logics

Let us consider, once again, the set of interval relations shown in Table1. If we associate exactly one modal operator to each relation, we obtain a propositional modal language with 12 modal operators; Figure 3 gives us the standard notation for these modal operators. The modal logic obtained in this way has been introduced by Halpern and Shoham in [6, 37], and it is usually referred to as HS. It should be clear now that formulas of HS can be seen as first-order formulas in the language introduced in Section 4 above, where quantifiers can be used only in a specific way. Consider, indeed, any formula generated by the grammar:
(2)φ::=p|¬φ|φ∨ψ|〈X〉φ|〈X-〉φ,
where 〈X〉∈{〈A〉,〈B〉,〈E〉,〈L〉,〈O〉,〈D〉} and 〈X¯〉 is its inverse. Such a formula can be translated into a first-order formula using only unary relational symbols, and where Allen’s relations are used to relativize quantifier. So, for example, the formula
(3)p→〈A〉q,
becomes
(4)P(x)→∃y(m(x,y)∧Q(y)).
In this setting, we can still formalize the requirements of our example. So, for instance, saying “The current state isq0” becomes q0, evaluated on the current world (interval), and expressing “If an interval of time is labeled with the stateq, thenqlabels also every sub-interval of it” can be done by means of the formula [A](q→[D]q∧[B]q∧[E]q)∧[A][A](q→[D]q∧[B]q∧[E]q).Figure 3
Allen’s interval relations and the corresponding HS modalities.A few remarks are in order, here. First of all, even if it might seem so, not every possible interval-related requirement can be expressed in this new setting, as quantifiers can be usedonly in this special, reduced way; so we are dealing here with a proper fragment of first-order language extended with Allen’s relations, and we can now hope for decidability (this is not the case for HS, as it turns out, but we can still look into proper fragments of HS). Second, in the example above there is subtle mistake: in the natural language version we quantify over every interval (again, we would like to use a nonrelativized quantifier, but we cannot), while in the modal version of this formula we actually quantify over every interval starting immediately after the current one (first conjunct) and every interval starting (non immediately) after the current one (second conjunct). Now, two orthogonal issues arise, the one being purely philosophical, while the other concerns the expressive power of the language: (1) can we settle with this reduced expressive power and suitably rephrase our requirement to obtain a “good enough” formalization? and (2) can we, instead, more cleverly use our modal operators in order to better describe our problem? It turns out that in the case of full HS we can actually simulate a non-relativized quantifiers in satisfactory way for our particular problem. So, we define
(5)[U]φ≡φ∧[A¯]φ∧[A¯][A¯]φ∧[A¯][A¯][A](φ∧[A]φ),
and our formula becomes [U](q→[D]q∧[B]q∧[E]q). Nevertheless, in general, the questions remain. Summing up, in addition to the class of linearly ordered sets in which the formulas are interpreted, we should add a new parameter while choosing the correct modal language for interval temporal reasoning: which subset of HS modalities do we want in our language? This is motivated by the fact that, unfortunately, HS itself is undecidable no matters which class of linearly ordered sets is, and this result is shown in the original paper [6]. But a series of more recent results, which we will detail in the following, prove that this is not always the case, as depending on the particular subset of modalities and the particular class of linearly ordered sets, we have fragments of HS which are decidable, with complexities that range from NP-complete to NEXPTIME-complete, EXPSPACE-complete, and to nonprimitive recursive.To make the notation and the notions uniform to the current literature, let us conclude this preliminary study on modal interval temporal logics by pointing out that, usually, a structure is formalized as a tupleM=〈𝔻,𝕀(𝔻),V〉, where 𝔻=〈𝔻,<〉 is a linearly ordered set (belonging to a specific class), 𝕀(𝔻) is the set of all intervals [a,b] (a<b) that can be formed over 𝔻, and V is the evaluation function that assigns every propositional letter p to the set of intervals over which it is true. Therefore, the truth function for a HS-formula becomes(i)
M,[a,b]⊩p if and only if [a,b]∈V(p);(ii)
M,[a,b]⊩¬φ if and only if it is not the case that M,[a,b]⊩φ;(iii)
M,[a,b]⊩φ∨ψ if and only if M,[a,b]⊩φ or M,[a,b]⊩ψ;(iv)
M,[a,b]⊩〈A〉φ if and only if there exists a point c>b such that M,[b,c]⊩ψ;(v)
M,[a,b]⊩〈L〉φ if and only if there exist two points c,d>b such that M,[c,d]⊩ψ;(vi)
M,[a,b]⊩〈B〉φ if and only if there exists a point a<c<b such that M,[a,c]⊩ψ;(vii)
M,[a,b]⊩〈E〉φ if and only if there exists a point a<c<b such that M,[c,b]⊩ψ;(viii)
M,[a,b]⊩〈D〉φ if and only if there exist two points a<c,d<b such that M,[c,d]⊩ψ;(ix)
M,[a,b]⊩〈O〉φ if and only if there exist two points a<c<b<d such that M,[c,d]⊩ψ.Relations between intervals are unary when intervals are the primary semantic elements and binary when intervals are seen as pairs points over a linearly ordered sets. The question on which properties must be (first order) axiomatized in the first-order language extended with Allen’s relations to make sure that they represent the intended relations between pairs of points is the representation problem, and it has been discussed in Section3.Unlike the first-order level, at the modal logic one we have more classes of linearly ordered sets to consider, as they present, in general, different results:(1)
the class of all linearly ordered sets (Lin);(2)
the class of all dense linearly ordered sets (Den);(3)
the class of all (weakly) discrete linearly ordered sets (Wdis).(4)
the class of all strongly discrete linearly ordered sets (SDen);(5)
the class of all finite linearly ordered sets (Fin);(6)
the class of all left-bounded ordered sets (LBou);(7)
the class of all right-bounded ordered sets (RBou). Unfortunately, at this level the situation is not as easy as it was at the first-order one. The problem of studying the expressive power of fragments of HS has been solved only in Lin; we will review these results, but only marginally; the interested reader can find it in [38]. The problem of classifying such fragments with respect to the decidability/undecidability status of their satisfiability problem, and its complexity, has been solved in full in Fin, SDen, SDen∩LBou, and SDen∩RBou and only partially in the other classes. In the following of this section, we will review the most representative results concerning these classification, while in the last section of the paper we will give some technical details for the interested reader.


### 4.2. The Class of All Finite Linearly Ordered Sets

Here, we give a complete picture of fragments of HS with respect to (un)decidability of their satisfiability problem over finite linear orders. In particular, we identify the set of all expressively different decidable fragments, and we determine the exact complexity of each of them; it turns out that there are exactly 62 decidable fragments of HS, shown in Figure4. We will denote the fragments by the set of their modalities, in alphabetical order, and omit those which are definable in terms of the others (in the considered fragment). As we will see, if we restrict our attention to decidable fragments, the only definable operators are 〈L〉 and 〈L¯〉. 〈L〉 can be defined as 〈A〉〈A〉 and 〈L¯〉 by 〈A¯〉〈A¯〉. Moreover, thanks to the highly symmetrical structure of the class of decidable fragments, all decidability results for fragments involving modalities 〈B〉 and 〈B¯〉 (for Allen’s relations starts and started by) can be immediately transferred to mirror fragments involving modalities 〈E〉 and 〈E-〉 (for Allen’s relations finishes and finished by). It is worth to notice that this transference of results is immediate because finite linear orders are left/right symmetric, which, in general, is not true.Figure 4
Hasse diagram of all and only decidable fragments of HS over finite linear orders.The objective of this section is to present all decidable fragments of HS in the classFin. Every fragment not shown in Figure 4 is undecidable. First, we have to prove that the Hasse diagram presented in the figure is correct from the expressive power point of view and that every fragment not shown actually includes as subfragment, an undecidable one. After that, we will analyze the various fragments from the complexity point of view. Most of these results have been proved in the recent paper [39].


#### 4.2.1.  Expressive Power

Given a fragmentℱ=X1X2⋯Xk and a modal operator 〈X〉, we write 〈X〉∈ℱ if X∈{X1,…,XK}. Given two fragments ℱ1 and ℱ2, we write ℱ1⊆ℱ2 if 〈X〉∈ℱ1 implies 〈X〉∈ℱ2, for every modality 〈X〉. An HS modality 〈X〉 is definable in an HS fragment ℱ, denoted 〈X〉⊲ℱ, if 〈X〉p≡ψ(p) for some formula ψ(p)∈F, for any fixed proposition letter p. The equivalence 〈X〉p≡ψ(p) is called an interdefinability equation for〈X〉inℱ. In [6], Halpern and Shoham show that, according to strict semantics, all HS modalities are definable in the fragment featuring the modalities 〈A〉, 〈B〉, and 〈E〉 and their transposes 〈A¯〉, 〈B¯〉, and 〈E¯〉. Given two HS fragments ℱ1 and ℱ2, we say that ℱ2 is at least as expressive asℱ1 (ℱ1⪯ℱ) if each operator 〈X〉∈ℱ1 is definable in ℱ2 and that ℱ1 is strictly less expressive than ℱ2, (ℱ1⪯ℱ2), if ℱ1⪯ℱ2, but not ℱ2⪯ℱ1. Moreover, we say that ℱ1 and ℱ2 are expressively incomparable (ℱ1≢ℱ2), if neither ℱ1⪯ℱ2 nor ℱ2⪯ℱ1.To prove that Figure4 is sound and complete with respect to the class of finite linear orders, we focus our attention on AA¯BB¯ and its fragments showing that: (1) each pair of fragments which are not related to each other in Figure 4 is expressively incomparable; (2) an edge from a fragment ℱ1 to a fragment ℱ2 means that ℱ2≺ℱ1; and (3) each fragment which is displayed in Figure 4 is undecidable. It can be easily shown that (i) and (ii) are immediate consequences of the fact that 〈L〉p≡〈A〉〈A〉p and 〈L-〉p≡〈A¯〉〈A¯〉p are all and only the interdefinability equations for AA¯BB¯ over finite linear orders. Indeed, the equations are sound, and, to prove that they are the only possible ones, for each operator 〈X〉∈AA¯BB¯, we can show that 〈X〉 is not definable in the maximal fragment of AA¯BB¯ not containing 〈X〉 itself. This amounts to prove that, first, 〈A〉⋪A¯BB¯L and 〈A¯〉⋪ABB¯L¯, second, 〈B¯〉⋪AA¯B and 〈B〉⋪AA¯B¯, and, third, 〈L¯〉⋪ABB¯ and 〈L〉⋪A¯BB¯, all of which can be done by means of easy bisimulations. Finally, proving that each fragment which is displayed in Figure 4 is undecidable can be done by pairing the above observations with known undecidability results for HS fragments. Indeed, we observe that Figure 4 contains all expressively different fragments of HS featuring modalities from the set {〈A〉,〈A¯〉,〈B〉,〈B¯〉,〈L〉,〈L¯〉}. Now, by contradiction, suppose that there exists a decidable fragment ℱ which is not included in Figure 4; by the previous observation, ℱ must contain at least one modality from the set {〈D〉,〈D¯〉,〈O〉,〈O¯〉,〈E〉,〈E¯〉}. If it contains one modality from the set {〈D〉,〈D¯〉,〈O〉,〈O¯〉}, then it is undecidable, since all HS fragments featuring one (and only one) of these modalities are already undecidable [40, 41] in the finite case. Hence, ℱ must contain at least one modality in the set {〈E〉,〈E¯〉}. This prevents modalities 〈B〉 and 〈B¯〉 to be included in ℱ, as they would immediately yield undecidability [42] in the finite case. Then, it follows that  ℱ  can contain only modalities from the set {〈A〉,〈A¯〉,〈E〉,〈E¯〉,〈L〉,〈L¯〉}, and thus it must belong to the diagram, which is a contradiction.


#### 4.2.2.  NP-Completeness

From [43], we know that BB¯ (and thus also its fragments B and B¯) is NP-complete. We can prove that the NP-membership of BB¯ [43] can be extended to BB¯LL¯. Since the satisfiability problem for propositional logic is itself NP-complete, BB¯LL¯ and its fragments are NP-complete. By a model-theoretic argument, it is possible to show that finite satisfiability of a BB¯LL¯-formula φ can be reduced to satisfiability in a model whose domain has a cardinality lower than a certain value which is polynomial in |φ|. This is done in two steps. First, one proves that satisfiability of a BB¯LL¯-formula φ in a finite model M=〈𝕀({0,…,N}),V〉 can be reduced to satisfiability of the formula τ(φ)=φ∨〈B¯〉φ∨〈L〉φ∨〈L〉〈L¯〉(φ∨〈B¯〉φ) over the interval [0,1], that is, M,[x,y]⊩φ if and only if M,[0,1]⊩τ(φ) (initial satisfiability). Then, by exploiting the fact that all intervals ending (resp., beginning) at the same point satisfy the same 〈L〉-formulas (resp., 〈L¯〉-formulas) and their negations, one observes that φ is initially satisfiable over a finite model if and only if it is initially satisfiable over a model M=〈𝕀({0,…,N}),V〉, with N∈O(|φ|), thanks to the fact that exceeding points can be eliminated preserving the satisfiability (the argument here is similar to the one used in [44] for a different fragment).


#### 4.2.3. NEXPTIME-Completeness

The subset of NEXPTIME-complete fragments has been known for a few years already. NEXPTIME-membership ofAA¯ (also known as Propositional Neighborhood Logic, or PNL) has been shown in [27]. NEXPTIME-hardness of A, given in [44], holds also for finite satisfiability, and it can be easily adapted to the case of A¯. NEXPTIME-hardness of any fragment containing 〈A〉 or 〈A¯〉 immediately follows.


#### 4.2.4.  EXPSPACE-Completeness

Let us turn our attention to the computational complexity ofABB¯L¯ and of its subfragments. EXPSPACE-membership for ABB¯L¯ has been shown in [45]. EXPSPACE-hardness holds for AB, as proved in [46]. But in [39], it has been shown that the reduction used in [46] works also in the finite case, and it can be adapted to AB¯. Indeed, EXPSPACE-hardness follows from a reduction of the 2n-corridor tiling problem, which is known to be EXPSPACE-complete [47, Section 5.5]. Formally, an instance of the exponential-corridor tiling problem is a tuple 𝒯=(T,t0,t1,TL,TR,CH,CV,n) consisting of a finite set T of tiles, two tiles t0,t1∈T, a set of left tiles TL⊆T, a set of right tiles TR⊆T, two binary relations CH and CV over T (specifying the horizontal and vertical constraints), and a positive natural number n. The problem amounts to deciding whether there exists a positive natural number l and a tiling f:{0,…,2n-1}×{0,…,l-1}→T of the corridor of width 2n and height l, that associates the tile t0 to (0,0), the tile t1 to (0,l-1), a tile in TL (resp., TR) with the first (resp., last) tile of every row of the corridor and that respects the following horizontal and vertical constraints CH and CV: (1) for every x<2n-1 and every y<l, we havef(x,y)CHf(x+1,y); and (2) for every x<2n and every y<l-1, we have  f(x,y)CVf(x,y+1).


#### 4.2.5.  Nonprimitive Recursiveness

Finally, we focus our attention on the remaining fragments. It turns out that, although decidable, they are of nonprimitive recursive complexity. From [48, 49], we know that there is a reduction from the finite satisfiability problem for AA¯B and AA¯B¯ to the so-called reachability problem for a lossy counter automata, which is known to be nonprimitive recursive [50]. In [39], it has been proved that such a reduction can be adapted to the cases of A¯B and A¯B¯, completing the picture.


### 4.3. The Class of All Strongly Discrete Linearly Ordered Sets

We now turn our attention on the classSDen of strongly discrete linear orders, that is, of those linear structures characterized by the presence finitely many points in between any two points. This class includes, for instance, ℕ, ℤ, and all finite linear orders. We give a complete classification of all HS fragments as before, and as shown in Figure 5, AA¯BB¯ and its mirror image AA¯EE¯ are the minimal fragments including all decidable subsets of operators from the HS repository, for a total of 62 languages. Of those, 44 turn out to be decidable. As a matter of fact, the status of various fragments has been established in the past few years, and the picture has been completed in the recent paper [51]. It is worth to observe that when we consider the subclasses SDen∩LBou and SDen∩RBou, the number of decidable fragments over ℕ raises up to 47, the three new decidable fragments being all nonprimitive recursive.Figure 5
Hasse diagram of fragments ofAA¯BB¯ and AA¯EE¯ over strongly discrete linear orders.


#### 4.3.1.  Expressive Power and Undecidability

Again, we focus our attention on fragments ofAA¯BB¯ and of its mirror image, AA¯EE¯, in order to prove that Figure 5 is sound and complete for the class of all strongly discrete linear orders. The relative positions of the various fragments can be shown to be correct exactly in the same way as in the finite case, as the class of all strongly discrete linearly ordered sets includes that of finite linearly ordered sets. On the contrary, here we have to prove that not only that the fragments which are not in the picture are undecidable, but also are undecidable those fragments marked in red. In particular, those fragments that are not referred to in the figure have been proved undecidable over the class of strongly discrete linearly ordered sets [40, 41]. From [48, 49], we know that there is a reduction from the satisfiability problem for AA¯B and AA¯B¯ to the structural termination problem for a lossy counter automata, which is known to be undecidable [50]. By partly exploiting some of the basic concepts of such a reduction, and using, instead, the nonemptiness problem for incrementing counter automata over infinite words, which, again, is known to be undecidable [52], one can actually see that AE is also undecidable in the considered class. Moreover, this fragment is in fact symmetric to A¯B over SDen, and, thus, the result trivially holds also for the latter fragment. Adapting it to AE¯ (and therefore, by symmetry, to A¯B¯) is then straightforward. As a note, let us recall that incrementing counter automata can be considered a variant of lossy counter automata in which faulty transitions increase the values instead of decrementing them; a comprehensive survey on faulty machines and on the complexity, decidability, and undecidability of various problems associated with such machines can be found in [53].


#### 4.3.2.  NP-Completeness

Considering now, again,BB¯LL¯ and its fragments, as in the finite case we can prove that NP-completeness of BB¯ [43] can be extended to it. Since the satisfiability problem for propositional logic is NP-complete, that for every proper fragment of BB¯LL¯ including it is at least NP-hard. The model theoretic argument used in the finite case can be extended to the infinite case; the only difference is that, instead of a model of polynomial length, we prove that each satisfiable formula has a periodic model where the lengths of prefixes and periods have a bound which is polynomial in the length of the original formula [51].


#### 4.3.3.  NEXPTIME/EXPSPACE-Completeness

NEXPTIME-membership ofAA¯ has been proved in [27]. NEXPTIME-hardness of A, shown in [44], holds also for the class of strongly discrete linear orders, and it can be adapted to the case of A¯, to prove NEXPTIME-hardness of any fragment including 〈A〉 or 〈A¯〉. As for EXPSPACE-complete fragments, we know from [45] that ABB¯L¯ is EXPSPACE-complete. Hardness for this class is claimed in the same paper for the fragments ABB¯ and AB. As in the finite case, this can be proved by a reduction from the exponential-corridor tiling problem, and in [39], it has been proved that this reduction can be modified to cover AB¯, and both reductions for AB and AB¯ immediately apply to the case of strongly discrete linearly ordered sets.


#### 4.3.4.  The ClassesSDen∩LBou  and  SDen∩LBou

As already observed, the asymmetry of models in these classes (e.g., models inSDen∩LBou, such as those based on ℕ, are left bounded), is reflected in the computational behavior of (some of) the fragments of AA¯BB¯ and its mirror image AA¯EE¯. To see this, let us consider for example the set of structures based on ℕ: (1)A¯B, but not AE, becomes decidable (nonprimitive recursive) [48]; (2)A¯B¯ and A¯BB¯, but not AE¯ nor AEE¯, become decidable (this can be shown by a suitable adaptation of the argument given in [48]); (3)A¯BL and A¯B¯L remain undecidable, but the proof [48] must be suitably adapted (see Figure 6).Figure 6
Hasse diagram of all fragments ofAA¯BB¯ and AA¯EE¯ over the natural numbers.


### 4.4.  Other Classes of Linearly Ordered Sets

As recalled, each (sub)class of structures requires, in general, a different treatment. We do not have a complete picture for any other class, yet, although we know a number of results. To understand how the situation might change for different classes, consider, for example, the dense case. The fragmentAA¯BB¯DD¯ is the minimal undecidable fragment that includes all decidable ones on dense linear orders, and it contains two, incomparable, maximal decidable fragments, namely, BB¯DD¯ and ABBL¯. The fragment AA¯ is still NEXPTIME-complete [54], and NEXPTIME-hardness already holds, again, for A and A¯; ABB¯L¯, is in EXPSPACE, and EXPSPACE-hardness already holds for the fragments ABB¯ and AB [55]; the fragments ABB¯A¯ and ABB¯ are already undecidable [48]; the fragment BB¯DD¯ (which includes 〈L〉 and 〈L¯〉 as definable operators) is in PSPACE, and PSPACE-hardness holds for D and D¯ alone [56]; finally, BB¯ is NP-complete [43], and, obviously, NP-hardness holds for B and B¯ alone too. Probably, we could extend the NP-completeness (in particular, NP-membership) of BB¯ can be extended to BB¯LL¯ and each one of its fragments, as we did in the strongly discrete case, and the EXPSPACE-completeness (in particular, EXPSPACE-hardness) of AB might be possibly adapted to the fragment AB¯, but, still, this is currently ongoing research. In the dense case, as well as in other case such as Wdis, thought, finding out the decidability/undecidability status of some fragments such as A¯B and A¯B¯ seems to be a really hard problem; a similar consideration can be done for D in the case of Lin.


### 4.5. Harvest

Let us focus, once again, on the finite case, as in automated planning (see Section2), we want our plans to be complete (i.e., the goal is eventually reached), sound (the constraints are respected), and, in general, finite (the goal is reached in a finite amount of time). With the classification at hand, we can now wisely choose the correct language depending on the particular problem that we want to solve. Consider, for example, the universal modality problem. We have already observed that every fragment above AA¯ is strong enough to define it. But, if our satisfiability problem consists of a set φ1∧⋯∧φk of formulas each one of which is evaluated, say, at the initial interval [0,1], then every fragment above A can do so too:
(6)[U]ψ≡[A]ψ∧[A][A]ψ.
What if we want to lower the theoretical complexity of the language? A good choice could be BB¯LL¯, which is NP-complete. In this case, we can define
(7)[U]ψ≡[L]ψ∧[L][L¯]ψ,
that is, the use of the past can compensate the lower expressive power of 〈L〉 with respect to 〈A〉.Consider, now, the (harder) problem of establishing a sequence of states, which is, a sequence of propositions that are both gestalt and solid. The most intuitive solution requires the use of the fragmentABE (≡HS)
(8)States≡〈A〉s∧[U](s→¬〈D〉⊑s)∧[U](s→〈A〉s∨[A]⊥),
where 〈D〉⊑ψ≡(〈B〉ψ∨〈E〉ψ∨〈D〉ψ) is the definable reflexive during modality (this modal operator has been studied on its own in [57]). But, doing so, we are giving up decidability. A better solution would require the use of the fragment AD(9)States≡〈A〉s∧[U](s∧(〈A〉s∨[A]⊥))∧[U](s→([D]s′∧〈D〉s′))∧[U](s′→¬(s∨〈A〉s))∧[U](s→¬〈A〉s′).
Again, this fragment, although simpler than HS itself, is still undecidable. A closer look to this problem gives us a definitive solution in the fragment AB, which is decidable in EXPSPACE:
(10)States≡〈A〉s∧[U](s∧(〈A〉s∨[A]⊥))∧[U](s→([B]s′∧〈B〉s′))∧[U](s′→¬(s∨〈A〉s)).In view of the above considerations, we could say that at the modal logic level, to find the correct language for a given problem is an exercise in expressive power. The potentialities of a specific language are indeed hidden in the language itself, and one has to spend sometime to find out whether or not a specific problem can be formalized with it.


## 4.1. Modal Interval Temporal Logics

Let us consider, once again, the set of interval relations shown in Table1. If we associate exactly one modal operator to each relation, we obtain a propositional modal language with 12 modal operators; Figure 3 gives us the standard notation for these modal operators. The modal logic obtained in this way has been introduced by Halpern and Shoham in [6, 37], and it is usually referred to as HS. It should be clear now that formulas of HS can be seen as first-order formulas in the language introduced in Section 4 above, where quantifiers can be used only in a specific way. Consider, indeed, any formula generated by the grammar:
(2)φ::=p|¬φ|φ∨ψ|〈X〉φ|〈X-〉φ,
where 〈X〉∈{〈A〉,〈B〉,〈E〉,〈L〉,〈O〉,〈D〉} and 〈X¯〉 is its inverse. Such a formula can be translated into a first-order formula using only unary relational symbols, and where Allen’s relations are used to relativize quantifier. So, for example, the formula
(3)p→〈A〉q,
becomes
(4)P(x)→∃y(m(x,y)∧Q(y)).
In this setting, we can still formalize the requirements of our example. So, for instance, saying “The current state isq0” becomes q0, evaluated on the current world (interval), and expressing “If an interval of time is labeled with the stateq, thenqlabels also every sub-interval of it” can be done by means of the formula [A](q→[D]q∧[B]q∧[E]q)∧[A][A](q→[D]q∧[B]q∧[E]q).Figure 3
Allen’s interval relations and the corresponding HS modalities.A few remarks are in order, here. First of all, even if it might seem so, not every possible interval-related requirement can be expressed in this new setting, as quantifiers can be usedonly in this special, reduced way; so we are dealing here with a proper fragment of first-order language extended with Allen’s relations, and we can now hope for decidability (this is not the case for HS, as it turns out, but we can still look into proper fragments of HS). Second, in the example above there is subtle mistake: in the natural language version we quantify over every interval (again, we would like to use a nonrelativized quantifier, but we cannot), while in the modal version of this formula we actually quantify over every interval starting immediately after the current one (first conjunct) and every interval starting (non immediately) after the current one (second conjunct). Now, two orthogonal issues arise, the one being purely philosophical, while the other concerns the expressive power of the language: (1) can we settle with this reduced expressive power and suitably rephrase our requirement to obtain a “good enough” formalization? and (2) can we, instead, more cleverly use our modal operators in order to better describe our problem? It turns out that in the case of full HS we can actually simulate a non-relativized quantifiers in satisfactory way for our particular problem. So, we define
(5)[U]φ≡φ∧[A¯]φ∧[A¯][A¯]φ∧[A¯][A¯][A](φ∧[A]φ),
and our formula becomes [U](q→[D]q∧[B]q∧[E]q). Nevertheless, in general, the questions remain. Summing up, in addition to the class of linearly ordered sets in which the formulas are interpreted, we should add a new parameter while choosing the correct modal language for interval temporal reasoning: which subset of HS modalities do we want in our language? This is motivated by the fact that, unfortunately, HS itself is undecidable no matters which class of linearly ordered sets is, and this result is shown in the original paper [6]. But a series of more recent results, which we will detail in the following, prove that this is not always the case, as depending on the particular subset of modalities and the particular class of linearly ordered sets, we have fragments of HS which are decidable, with complexities that range from NP-complete to NEXPTIME-complete, EXPSPACE-complete, and to nonprimitive recursive.To make the notation and the notions uniform to the current literature, let us conclude this preliminary study on modal interval temporal logics by pointing out that, usually, a structure is formalized as a tupleM=〈𝔻,𝕀(𝔻),V〉, where 𝔻=〈𝔻,<〉 is a linearly ordered set (belonging to a specific class), 𝕀(𝔻) is the set of all intervals [a,b] (a<b) that can be formed over 𝔻, and V is the evaluation function that assigns every propositional letter p to the set of intervals over which it is true. Therefore, the truth function for a HS-formula becomes(i)
M,[a,b]⊩p if and only if [a,b]∈V(p);(ii)
M,[a,b]⊩¬φ if and only if it is not the case that M,[a,b]⊩φ;(iii)
M,[a,b]⊩φ∨ψ if and only if M,[a,b]⊩φ or M,[a,b]⊩ψ;(iv)
M,[a,b]⊩〈A〉φ if and only if there exists a point c>b such that M,[b,c]⊩ψ;(v)
M,[a,b]⊩〈L〉φ if and only if there exist two points c,d>b such that M,[c,d]⊩ψ;(vi)
M,[a,b]⊩〈B〉φ if and only if there exists a point a<c<b such that M,[a,c]⊩ψ;(vii)
M,[a,b]⊩〈E〉φ if and only if there exists a point a<c<b such that M,[c,b]⊩ψ;(viii)
M,[a,b]⊩〈D〉φ if and only if there exist two points a<c,d<b such that M,[c,d]⊩ψ;(ix)
M,[a,b]⊩〈O〉φ if and only if there exist two points a<c<b<d such that M,[c,d]⊩ψ.Relations between intervals are unary when intervals are the primary semantic elements and binary when intervals are seen as pairs points over a linearly ordered sets. The question on which properties must be (first order) axiomatized in the first-order language extended with Allen’s relations to make sure that they represent the intended relations between pairs of points is the representation problem, and it has been discussed in Section3.Unlike the first-order level, at the modal logic one we have more classes of linearly ordered sets to consider, as they present, in general, different results:(1)
the class of all linearly ordered sets (Lin);(2)
the class of all dense linearly ordered sets (Den);(3)
the class of all (weakly) discrete linearly ordered sets (Wdis).(4)
the class of all strongly discrete linearly ordered sets (SDen);(5)
the class of all finite linearly ordered sets (Fin);(6)
the class of all left-bounded ordered sets (LBou);(7)
the class of all right-bounded ordered sets (RBou). Unfortunately, at this level the situation is not as easy as it was at the first-order one. The problem of studying the expressive power of fragments of HS has been solved only in Lin; we will review these results, but only marginally; the interested reader can find it in [38]. The problem of classifying such fragments with respect to the decidability/undecidability status of their satisfiability problem, and its complexity, has been solved in full in Fin, SDen, SDen∩LBou, and SDen∩RBou and only partially in the other classes. In the following of this section, we will review the most representative results concerning these classification, while in the last section of the paper we will give some technical details for the interested reader.


## 4.2. The Class of All Finite Linearly Ordered Sets

Here, we give a complete picture of fragments of HS with respect to (un)decidability of their satisfiability problem over finite linear orders. In particular, we identify the set of all expressively different decidable fragments, and we determine the exact complexity of each of them; it turns out that there are exactly 62 decidable fragments of HS, shown in Figure4. We will denote the fragments by the set of their modalities, in alphabetical order, and omit those which are definable in terms of the others (in the considered fragment). As we will see, if we restrict our attention to decidable fragments, the only definable operators are 〈L〉 and 〈L¯〉. 〈L〉 can be defined as 〈A〉〈A〉 and 〈L¯〉 by 〈A¯〉〈A¯〉. Moreover, thanks to the highly symmetrical structure of the class of decidable fragments, all decidability results for fragments involving modalities 〈B〉 and 〈B¯〉 (for Allen’s relations starts and started by) can be immediately transferred to mirror fragments involving modalities 〈E〉 and 〈E-〉 (for Allen’s relations finishes and finished by). It is worth to notice that this transference of results is immediate because finite linear orders are left/right symmetric, which, in general, is not true.Figure 4
Hasse diagram of all and only decidable fragments of HS over finite linear orders.The objective of this section is to present all decidable fragments of HS in the classFin. Every fragment not shown in Figure 4 is undecidable. First, we have to prove that the Hasse diagram presented in the figure is correct from the expressive power point of view and that every fragment not shown actually includes as subfragment, an undecidable one. After that, we will analyze the various fragments from the complexity point of view. Most of these results have been proved in the recent paper [39].


### 4.2.1.  Expressive Power

Given a fragmentℱ=X1X2⋯Xk and a modal operator 〈X〉, we write 〈X〉∈ℱ if X∈{X1,…,XK}. Given two fragments ℱ1 and ℱ2, we write ℱ1⊆ℱ2 if 〈X〉∈ℱ1 implies 〈X〉∈ℱ2, for every modality 〈X〉. An HS modality 〈X〉 is definable in an HS fragment ℱ, denoted 〈X〉⊲ℱ, if 〈X〉p≡ψ(p) for some formula ψ(p)∈F, for any fixed proposition letter p. The equivalence 〈X〉p≡ψ(p) is called an interdefinability equation for〈X〉inℱ. In [6], Halpern and Shoham show that, according to strict semantics, all HS modalities are definable in the fragment featuring the modalities 〈A〉, 〈B〉, and 〈E〉 and their transposes 〈A¯〉, 〈B¯〉, and 〈E¯〉. Given two HS fragments ℱ1 and ℱ2, we say that ℱ2 is at least as expressive asℱ1 (ℱ1⪯ℱ) if each operator 〈X〉∈ℱ1 is definable in ℱ2 and that ℱ1 is strictly less expressive than ℱ2, (ℱ1⪯ℱ2), if ℱ1⪯ℱ2, but not ℱ2⪯ℱ1. Moreover, we say that ℱ1 and ℱ2 are expressively incomparable (ℱ1≢ℱ2), if neither ℱ1⪯ℱ2 nor ℱ2⪯ℱ1.To prove that Figure4 is sound and complete with respect to the class of finite linear orders, we focus our attention on AA¯BB¯ and its fragments showing that: (1) each pair of fragments which are not related to each other in Figure 4 is expressively incomparable; (2) an edge from a fragment ℱ1 to a fragment ℱ2 means that ℱ2≺ℱ1; and (3) each fragment which is displayed in Figure 4 is undecidable. It can be easily shown that (i) and (ii) are immediate consequences of the fact that 〈L〉p≡〈A〉〈A〉p and 〈L-〉p≡〈A¯〉〈A¯〉p are all and only the interdefinability equations for AA¯BB¯ over finite linear orders. Indeed, the equations are sound, and, to prove that they are the only possible ones, for each operator 〈X〉∈AA¯BB¯, we can show that 〈X〉 is not definable in the maximal fragment of AA¯BB¯ not containing 〈X〉 itself. This amounts to prove that, first, 〈A〉⋪A¯BB¯L and 〈A¯〉⋪ABB¯L¯, second, 〈B¯〉⋪AA¯B and 〈B〉⋪AA¯B¯, and, third, 〈L¯〉⋪ABB¯ and 〈L〉⋪A¯BB¯, all of which can be done by means of easy bisimulations. Finally, proving that each fragment which is displayed in Figure 4 is undecidable can be done by pairing the above observations with known undecidability results for HS fragments. Indeed, we observe that Figure 4 contains all expressively different fragments of HS featuring modalities from the set {〈A〉,〈A¯〉,〈B〉,〈B¯〉,〈L〉,〈L¯〉}. Now, by contradiction, suppose that there exists a decidable fragment ℱ which is not included in Figure 4; by the previous observation, ℱ must contain at least one modality from the set {〈D〉,〈D¯〉,〈O〉,〈O¯〉,〈E〉,〈E¯〉}. If it contains one modality from the set {〈D〉,〈D¯〉,〈O〉,〈O¯〉}, then it is undecidable, since all HS fragments featuring one (and only one) of these modalities are already undecidable [40, 41] in the finite case. Hence, ℱ must contain at least one modality in the set {〈E〉,〈E¯〉}. This prevents modalities 〈B〉 and 〈B¯〉 to be included in ℱ, as they would immediately yield undecidability [42] in the finite case. Then, it follows that  ℱ  can contain only modalities from the set {〈A〉,〈A¯〉,〈E〉,〈E¯〉,〈L〉,〈L¯〉}, and thus it must belong to the diagram, which is a contradiction.


### 4.2.2.  NP-Completeness

From [43], we know that BB¯ (and thus also its fragments B and B¯) is NP-complete. We can prove that the NP-membership of BB¯ [43] can be extended to BB¯LL¯. Since the satisfiability problem for propositional logic is itself NP-complete, BB¯LL¯ and its fragments are NP-complete. By a model-theoretic argument, it is possible to show that finite satisfiability of a BB¯LL¯-formula φ can be reduced to satisfiability in a model whose domain has a cardinality lower than a certain value which is polynomial in |φ|. This is done in two steps. First, one proves that satisfiability of a BB¯LL¯-formula φ in a finite model M=〈𝕀({0,…,N}),V〉 can be reduced to satisfiability of the formula τ(φ)=φ∨〈B¯〉φ∨〈L〉φ∨〈L〉〈L¯〉(φ∨〈B¯〉φ) over the interval [0,1], that is, M,[x,y]⊩φ if and only if M,[0,1]⊩τ(φ) (initial satisfiability). Then, by exploiting the fact that all intervals ending (resp., beginning) at the same point satisfy the same 〈L〉-formulas (resp., 〈L¯〉-formulas) and their negations, one observes that φ is initially satisfiable over a finite model if and only if it is initially satisfiable over a model M=〈𝕀({0,…,N}),V〉, with N∈O(|φ|), thanks to the fact that exceeding points can be eliminated preserving the satisfiability (the argument here is similar to the one used in [44] for a different fragment).


### 4.2.3. NEXPTIME-Completeness

The subset of NEXPTIME-complete fragments has been known for a few years already. NEXPTIME-membership ofAA¯ (also known as Propositional Neighborhood Logic, or PNL) has been shown in [27]. NEXPTIME-hardness of A, given in [44], holds also for finite satisfiability, and it can be easily adapted to the case of A¯. NEXPTIME-hardness of any fragment containing 〈A〉 or 〈A¯〉 immediately follows.


### 4.2.4.  EXPSPACE-Completeness

Let us turn our attention to the computational complexity ofABB¯L¯ and of its subfragments. EXPSPACE-membership for ABB¯L¯ has been shown in [45]. EXPSPACE-hardness holds for AB, as proved in [46]. But in [39], it has been shown that the reduction used in [46] works also in the finite case, and it can be adapted to AB¯. Indeed, EXPSPACE-hardness follows from a reduction of the 2n-corridor tiling problem, which is known to be EXPSPACE-complete [47, Section 5.5]. Formally, an instance of the exponential-corridor tiling problem is a tuple 𝒯=(T,t0,t1,TL,TR,CH,CV,n) consisting of a finite set T of tiles, two tiles t0,t1∈T, a set of left tiles TL⊆T, a set of right tiles TR⊆T, two binary relations CH and CV over T (specifying the horizontal and vertical constraints), and a positive natural number n. The problem amounts to deciding whether there exists a positive natural number l and a tiling f:{0,…,2n-1}×{0,…,l-1}→T of the corridor of width 2n and height l, that associates the tile t0 to (0,0), the tile t1 to (0,l-1), a tile in TL (resp., TR) with the first (resp., last) tile of every row of the corridor and that respects the following horizontal and vertical constraints CH and CV: (1) for every x<2n-1 and every y<l, we havef(x,y)CHf(x+1,y); and (2) for every x<2n and every y<l-1, we have  f(x,y)CVf(x,y+1).


### 4.2.5.  Nonprimitive Recursiveness

Finally, we focus our attention on the remaining fragments. It turns out that, although decidable, they are of nonprimitive recursive complexity. From [48, 49], we know that there is a reduction from the finite satisfiability problem for AA¯B and AA¯B¯ to the so-called reachability problem for a lossy counter automata, which is known to be nonprimitive recursive [50]. In [39], it has been proved that such a reduction can be adapted to the cases of A¯B and A¯B¯, completing the picture.


## 4.2.1.  Expressive Power

Given a fragmentℱ=X1X2⋯Xk and a modal operator 〈X〉, we write 〈X〉∈ℱ if X∈{X1,…,XK}. Given two fragments ℱ1 and ℱ2, we write ℱ1⊆ℱ2 if 〈X〉∈ℱ1 implies 〈X〉∈ℱ2, for every modality 〈X〉. An HS modality 〈X〉 is definable in an HS fragment ℱ, denoted 〈X〉⊲ℱ, if 〈X〉p≡ψ(p) for some formula ψ(p)∈F, for any fixed proposition letter p. The equivalence 〈X〉p≡ψ(p) is called an interdefinability equation for〈X〉inℱ. In [6], Halpern and Shoham show that, according to strict semantics, all HS modalities are definable in the fragment featuring the modalities 〈A〉, 〈B〉, and 〈E〉 and their transposes 〈A¯〉, 〈B¯〉, and 〈E¯〉. Given two HS fragments ℱ1 and ℱ2, we say that ℱ2 is at least as expressive asℱ1 (ℱ1⪯ℱ) if each operator 〈X〉∈ℱ1 is definable in ℱ2 and that ℱ1 is strictly less expressive than ℱ2, (ℱ1⪯ℱ2), if ℱ1⪯ℱ2, but not ℱ2⪯ℱ1. Moreover, we say that ℱ1 and ℱ2 are expressively incomparable (ℱ1≢ℱ2), if neither ℱ1⪯ℱ2 nor ℱ2⪯ℱ1.To prove that Figure4 is sound and complete with respect to the class of finite linear orders, we focus our attention on AA¯BB¯ and its fragments showing that: (1) each pair of fragments which are not related to each other in Figure 4 is expressively incomparable; (2) an edge from a fragment ℱ1 to a fragment ℱ2 means that ℱ2≺ℱ1; and (3) each fragment which is displayed in Figure 4 is undecidable. It can be easily shown that (i) and (ii) are immediate consequences of the fact that 〈L〉p≡〈A〉〈A〉p and 〈L-〉p≡〈A¯〉〈A¯〉p are all and only the interdefinability equations for AA¯BB¯ over finite linear orders. Indeed, the equations are sound, and, to prove that they are the only possible ones, for each operator 〈X〉∈AA¯BB¯, we can show that 〈X〉 is not definable in the maximal fragment of AA¯BB¯ not containing 〈X〉 itself. This amounts to prove that, first, 〈A〉⋪A¯BB¯L and 〈A¯〉⋪ABB¯L¯, second, 〈B¯〉⋪AA¯B and 〈B〉⋪AA¯B¯, and, third, 〈L¯〉⋪ABB¯ and 〈L〉⋪A¯BB¯, all of which can be done by means of easy bisimulations. Finally, proving that each fragment which is displayed in Figure 4 is undecidable can be done by pairing the above observations with known undecidability results for HS fragments. Indeed, we observe that Figure 4 contains all expressively different fragments of HS featuring modalities from the set {〈A〉,〈A¯〉,〈B〉,〈B¯〉,〈L〉,〈L¯〉}. Now, by contradiction, suppose that there exists a decidable fragment ℱ which is not included in Figure 4; by the previous observation, ℱ must contain at least one modality from the set {〈D〉,〈D¯〉,〈O〉,〈O¯〉,〈E〉,〈E¯〉}. If it contains one modality from the set {〈D〉,〈D¯〉,〈O〉,〈O¯〉}, then it is undecidable, since all HS fragments featuring one (and only one) of these modalities are already undecidable [40, 41] in the finite case. Hence, ℱ must contain at least one modality in the set {〈E〉,〈E¯〉}. This prevents modalities 〈B〉 and 〈B¯〉 to be included in ℱ, as they would immediately yield undecidability [42] in the finite case. Then, it follows that  ℱ  can contain only modalities from the set {〈A〉,〈A¯〉,〈E〉,〈E¯〉,〈L〉,〈L¯〉}, and thus it must belong to the diagram, which is a contradiction.


## 4.2.2.  NP-Completeness

From [43], we know that BB¯ (and thus also its fragments B and B¯) is NP-complete. We can prove that the NP-membership of BB¯ [43] can be extended to BB¯LL¯. Since the satisfiability problem for propositional logic is itself NP-complete, BB¯LL¯ and its fragments are NP-complete. By a model-theoretic argument, it is possible to show that finite satisfiability of a BB¯LL¯-formula φ can be reduced to satisfiability in a model whose domain has a cardinality lower than a certain value which is polynomial in |φ|. This is done in two steps. First, one proves that satisfiability of a BB¯LL¯-formula φ in a finite model M=〈𝕀({0,…,N}),V〉 can be reduced to satisfiability of the formula τ(φ)=φ∨〈B¯〉φ∨〈L〉φ∨〈L〉〈L¯〉(φ∨〈B¯〉φ) over the interval [0,1], that is, M,[x,y]⊩φ if and only if M,[0,1]⊩τ(φ) (initial satisfiability). Then, by exploiting the fact that all intervals ending (resp., beginning) at the same point satisfy the same 〈L〉-formulas (resp., 〈L¯〉-formulas) and their negations, one observes that φ is initially satisfiable over a finite model if and only if it is initially satisfiable over a model M=〈𝕀({0,…,N}),V〉, with N∈O(|φ|), thanks to the fact that exceeding points can be eliminated preserving the satisfiability (the argument here is similar to the one used in [44] for a different fragment).


## 4.2.3. NEXPTIME-Completeness

The subset of NEXPTIME-complete fragments has been known for a few years already. NEXPTIME-membership ofAA¯ (also known as Propositional Neighborhood Logic, or PNL) has been shown in [27]. NEXPTIME-hardness of A, given in [44], holds also for finite satisfiability, and it can be easily adapted to the case of A¯. NEXPTIME-hardness of any fragment containing 〈A〉 or 〈A¯〉 immediately follows.


## 4.2.4.  EXPSPACE-Completeness

Let us turn our attention to the computational complexity ofABB¯L¯ and of its subfragments. EXPSPACE-membership for ABB¯L¯ has been shown in [45]. EXPSPACE-hardness holds for AB, as proved in [46]. But in [39], it has been shown that the reduction used in [46] works also in the finite case, and it can be adapted to AB¯. Indeed, EXPSPACE-hardness follows from a reduction of the 2n-corridor tiling problem, which is known to be EXPSPACE-complete [47, Section 5.5]. Formally, an instance of the exponential-corridor tiling problem is a tuple 𝒯=(T,t0,t1,TL,TR,CH,CV,n) consisting of a finite set T of tiles, two tiles t0,t1∈T, a set of left tiles TL⊆T, a set of right tiles TR⊆T, two binary relations CH and CV over T (specifying the horizontal and vertical constraints), and a positive natural number n. The problem amounts to deciding whether there exists a positive natural number l and a tiling f:{0,…,2n-1}×{0,…,l-1}→T of the corridor of width 2n and height l, that associates the tile t0 to (0,0), the tile t1 to (0,l-1), a tile in TL (resp., TR) with the first (resp., last) tile of every row of the corridor and that respects the following horizontal and vertical constraints CH and CV: (1) for every x<2n-1 and every y<l, we havef(x,y)CHf(x+1,y); and (2) for every x<2n and every y<l-1, we have  f(x,y)CVf(x,y+1).


## 4.2.5.  Nonprimitive Recursiveness

Finally, we focus our attention on the remaining fragments. It turns out that, although decidable, they are of nonprimitive recursive complexity. From [48, 49], we know that there is a reduction from the finite satisfiability problem for AA¯B and AA¯B¯ to the so-called reachability problem for a lossy counter automata, which is known to be nonprimitive recursive [50]. In [39], it has been proved that such a reduction can be adapted to the cases of A¯B and A¯B¯, completing the picture.


## 4.3. The Class of All Strongly Discrete Linearly Ordered Sets

We now turn our attention on the classSDen of strongly discrete linear orders, that is, of those linear structures characterized by the presence finitely many points in between any two points. This class includes, for instance, ℕ, ℤ, and all finite linear orders. We give a complete classification of all HS fragments as before, and as shown in Figure 5, AA¯BB¯ and its mirror image AA¯EE¯ are the minimal fragments including all decidable subsets of operators from the HS repository, for a total of 62 languages. Of those, 44 turn out to be decidable. As a matter of fact, the status of various fragments has been established in the past few years, and the picture has been completed in the recent paper [51]. It is worth to observe that when we consider the subclasses SDen∩LBou and SDen∩RBou, the number of decidable fragments over ℕ raises up to 47, the three new decidable fragments being all nonprimitive recursive.Figure 5
Hasse diagram of fragments ofAA¯BB¯ and AA¯EE¯ over strongly discrete linear orders.


### 4.3.1.  Expressive Power and Undecidability

Again, we focus our attention on fragments ofAA¯BB¯ and of its mirror image, AA¯EE¯, in order to prove that Figure 5 is sound and complete for the class of all strongly discrete linear orders. The relative positions of the various fragments can be shown to be correct exactly in the same way as in the finite case, as the class of all strongly discrete linearly ordered sets includes that of finite linearly ordered sets. On the contrary, here we have to prove that not only that the fragments which are not in the picture are undecidable, but also are undecidable those fragments marked in red. In particular, those fragments that are not referred to in the figure have been proved undecidable over the class of strongly discrete linearly ordered sets [40, 41]. From [48, 49], we know that there is a reduction from the satisfiability problem for AA¯B and AA¯B¯ to the structural termination problem for a lossy counter automata, which is known to be undecidable [50]. By partly exploiting some of the basic concepts of such a reduction, and using, instead, the nonemptiness problem for incrementing counter automata over infinite words, which, again, is known to be undecidable [52], one can actually see that AE is also undecidable in the considered class. Moreover, this fragment is in fact symmetric to A¯B over SDen, and, thus, the result trivially holds also for the latter fragment. Adapting it to AE¯ (and therefore, by symmetry, to A¯B¯) is then straightforward. As a note, let us recall that incrementing counter automata can be considered a variant of lossy counter automata in which faulty transitions increase the values instead of decrementing them; a comprehensive survey on faulty machines and on the complexity, decidability, and undecidability of various problems associated with such machines can be found in [53].


### 4.3.2.  NP-Completeness

Considering now, again,BB¯LL¯ and its fragments, as in the finite case we can prove that NP-completeness of BB¯ [43] can be extended to it. Since the satisfiability problem for propositional logic is NP-complete, that for every proper fragment of BB¯LL¯ including it is at least NP-hard. The model theoretic argument used in the finite case can be extended to the infinite case; the only difference is that, instead of a model of polynomial length, we prove that each satisfiable formula has a periodic model where the lengths of prefixes and periods have a bound which is polynomial in the length of the original formula [51].


### 4.3.3.  NEXPTIME/EXPSPACE-Completeness

NEXPTIME-membership ofAA¯ has been proved in [27]. NEXPTIME-hardness of A, shown in [44], holds also for the class of strongly discrete linear orders, and it can be adapted to the case of A¯, to prove NEXPTIME-hardness of any fragment including 〈A〉 or 〈A¯〉. As for EXPSPACE-complete fragments, we know from [45] that ABB¯L¯ is EXPSPACE-complete. Hardness for this class is claimed in the same paper for the fragments ABB¯ and AB. As in the finite case, this can be proved by a reduction from the exponential-corridor tiling problem, and in [39], it has been proved that this reduction can be modified to cover AB¯, and both reductions for AB and AB¯ immediately apply to the case of strongly discrete linearly ordered sets.


### 4.3.4.  The ClassesSDen∩LBou  and  SDen∩LBou

As already observed, the asymmetry of models in these classes (e.g., models inSDen∩LBou, such as those based on ℕ, are left bounded), is reflected in the computational behavior of (some of) the fragments of AA¯BB¯ and its mirror image AA¯EE¯. To see this, let us consider for example the set of structures based on ℕ: (1)A¯B, but not AE, becomes decidable (nonprimitive recursive) [48]; (2)A¯B¯ and A¯BB¯, but not AE¯ nor AEE¯, become decidable (this can be shown by a suitable adaptation of the argument given in [48]); (3)A¯BL and A¯B¯L remain undecidable, but the proof [48] must be suitably adapted (see Figure 6).Figure 6
Hasse diagram of all fragments ofAA¯BB¯ and AA¯EE¯ over the natural numbers.


## 4.3.1.  Expressive Power and Undecidability

Again, we focus our attention on fragments ofAA¯BB¯ and of its mirror image, AA¯EE¯, in order to prove that Figure 5 is sound and complete for the class of all strongly discrete linear orders. The relative positions of the various fragments can be shown to be correct exactly in the same way as in the finite case, as the class of all strongly discrete linearly ordered sets includes that of finite linearly ordered sets. On the contrary, here we have to prove that not only that the fragments which are not in the picture are undecidable, but also are undecidable those fragments marked in red. In particular, those fragments that are not referred to in the figure have been proved undecidable over the class of strongly discrete linearly ordered sets [40, 41]. From [48, 49], we know that there is a reduction from the satisfiability problem for AA¯B and AA¯B¯ to the structural termination problem for a lossy counter automata, which is known to be undecidable [50]. By partly exploiting some of the basic concepts of such a reduction, and using, instead, the nonemptiness problem for incrementing counter automata over infinite words, which, again, is known to be undecidable [52], one can actually see that AE is also undecidable in the considered class. Moreover, this fragment is in fact symmetric to A¯B over SDen, and, thus, the result trivially holds also for the latter fragment. Adapting it to AE¯ (and therefore, by symmetry, to A¯B¯) is then straightforward. As a note, let us recall that incrementing counter automata can be considered a variant of lossy counter automata in which faulty transitions increase the values instead of decrementing them; a comprehensive survey on faulty machines and on the complexity, decidability, and undecidability of various problems associated with such machines can be found in [53].


## 4.3.2.  NP-Completeness

Considering now, again,BB¯LL¯ and its fragments, as in the finite case we can prove that NP-completeness of BB¯ [43] can be extended to it. Since the satisfiability problem for propositional logic is NP-complete, that for every proper fragment of BB¯LL¯ including it is at least NP-hard. The model theoretic argument used in the finite case can be extended to the infinite case; the only difference is that, instead of a model of polynomial length, we prove that each satisfiable formula has a periodic model where the lengths of prefixes and periods have a bound which is polynomial in the length of the original formula [51].


## 4.3.3.  NEXPTIME/EXPSPACE-Completeness

NEXPTIME-membership ofAA¯ has been proved in [27]. NEXPTIME-hardness of A, shown in [44], holds also for the class of strongly discrete linear orders, and it can be adapted to the case of A¯, to prove NEXPTIME-hardness of any fragment including 〈A〉 or 〈A¯〉. As for EXPSPACE-complete fragments, we know from [45] that ABB¯L¯ is EXPSPACE-complete. Hardness for this class is claimed in the same paper for the fragments ABB¯ and AB. As in the finite case, this can be proved by a reduction from the exponential-corridor tiling problem, and in [39], it has been proved that this reduction can be modified to cover AB¯, and both reductions for AB and AB¯ immediately apply to the case of strongly discrete linearly ordered sets.


## 4.3.4.  The ClassesSDen∩LBou  and  SDen∩LBou

As already observed, the asymmetry of models in these classes (e.g., models inSDen∩LBou, such as those based on ℕ, are left bounded), is reflected in the computational behavior of (some of) the fragments of AA¯BB¯ and its mirror image AA¯EE¯. To see this, let us consider for example the set of structures based on ℕ: (1)A¯B, but not AE, becomes decidable (nonprimitive recursive) [48]; (2)A¯B¯ and A¯BB¯, but not AE¯ nor AEE¯, become decidable (this can be shown by a suitable adaptation of the argument given in [48]); (3)A¯BL and A¯B¯L remain undecidable, but the proof [48] must be suitably adapted (see Figure 6).Figure 6
Hasse diagram of all fragments ofAA¯BB¯ and AA¯EE¯ over the natural numbers.


## 4.4.  Other Classes of Linearly Ordered Sets

As recalled, each (sub)class of structures requires, in general, a different treatment. We do not have a complete picture for any other class, yet, although we know a number of results. To understand how the situation might change for different classes, consider, for example, the dense case. The fragmentAA¯BB¯DD¯ is the minimal undecidable fragment that includes all decidable ones on dense linear orders, and it contains two, incomparable, maximal decidable fragments, namely, BB¯DD¯ and ABBL¯. The fragment AA¯ is still NEXPTIME-complete [54], and NEXPTIME-hardness already holds, again, for A and A¯; ABB¯L¯, is in EXPSPACE, and EXPSPACE-hardness already holds for the fragments ABB¯ and AB [55]; the fragments ABB¯A¯ and ABB¯ are already undecidable [48]; the fragment BB¯DD¯ (which includes 〈L〉 and 〈L¯〉 as definable operators) is in PSPACE, and PSPACE-hardness holds for D and D¯ alone [56]; finally, BB¯ is NP-complete [43], and, obviously, NP-hardness holds for B and B¯ alone too. Probably, we could extend the NP-completeness (in particular, NP-membership) of BB¯ can be extended to BB¯LL¯ and each one of its fragments, as we did in the strongly discrete case, and the EXPSPACE-completeness (in particular, EXPSPACE-hardness) of AB might be possibly adapted to the fragment AB¯, but, still, this is currently ongoing research. In the dense case, as well as in other case such as Wdis, thought, finding out the decidability/undecidability status of some fragments such as A¯B and A¯B¯ seems to be a really hard problem; a similar consideration can be done for D in the case of Lin.


## 4.5. Harvest

Let us focus, once again, on the finite case, as in automated planning (see Section2), we want our plans to be complete (i.e., the goal is eventually reached), sound (the constraints are respected), and, in general, finite (the goal is reached in a finite amount of time). With the classification at hand, we can now wisely choose the correct language depending on the particular problem that we want to solve. Consider, for example, the universal modality problem. We have already observed that every fragment above AA¯ is strong enough to define it. But, if our satisfiability problem consists of a set φ1∧⋯∧φk of formulas each one of which is evaluated, say, at the initial interval [0,1], then every fragment above A can do so too:
(6)[U]ψ≡[A]ψ∧[A][A]ψ.
What if we want to lower the theoretical complexity of the language? A good choice could be BB¯LL¯, which is NP-complete. In this case, we can define
(7)[U]ψ≡[L]ψ∧[L][L¯]ψ,
that is, the use of the past can compensate the lower expressive power of 〈L〉 with respect to 〈A〉.Consider, now, the (harder) problem of establishing a sequence of states, which is, a sequence of propositions that are both gestalt and solid. The most intuitive solution requires the use of the fragmentABE (≡HS)
(8)States≡〈A〉s∧[U](s→¬〈D〉⊑s)∧[U](s→〈A〉s∨[A]⊥),
where 〈D〉⊑ψ≡(〈B〉ψ∨〈E〉ψ∨〈D〉ψ) is the definable reflexive during modality (this modal operator has been studied on its own in [57]). But, doing so, we are giving up decidability. A better solution would require the use of the fragment AD(9)States≡〈A〉s∧[U](s∧(〈A〉s∨[A]⊥))∧[U](s→([D]s′∧〈D〉s′))∧[U](s′→¬(s∨〈A〉s))∧[U](s→¬〈A〉s′).
Again, this fragment, although simpler than HS itself, is still undecidable. A closer look to this problem gives us a definitive solution in the fragment AB, which is decidable in EXPSPACE:
(10)States≡〈A〉s∧[U](s∧(〈A〉s∨[A]⊥))∧[U](s→([B]s′∧〈B〉s′))∧[U](s′→¬(s∨〈A〉s)).In view of the above considerations, we could say that at the modal logic level, to find the correct language for a given problem is an exercise in expressive power. The potentialities of a specific language are indeed hidden in the language itself, and one has to spend sometime to find out whether or not a specific problem can be formalized with it.


## 5. Conclusions

In this paper, we have seen how temporal reasoning is pervasive in so many areas of computer science and artificial intelligence, and we gave a number of representative examples. We analyzed some very recent results at the first-order and the modal logic level in this area, which has been quite active in the past years. We now want to conclude this paper by presenting some interesting open issues and research directions.At the first-order level, at least two problems are still pending. First, we would like to produce an integrated theory that includes both points and intervals, with a consistent notation, and solve the problem of classifying, in the same way as we did in the pure interval case, all extensions of first-order logic with point and interval relations, and study their expressive power. Secondly, the generalization of such results, both considering intervals only, and considering both points and interval, to a more general class of orders that includes, for example, tree orders is certainly not immediate and will probably present interesting and new developments.More importantly, at the modal level the job is not done.In primis, when we only look to the pure interval case, we have already seen that the classification of the various fragments is still incomplete for many classes of linear orders. Two missing cases are particularly difficult: (1) while the recent papers [41, 58] have tackled and solved the case of D over finite orders, the same fragments over Lin is still open; (2) we know that AA¯B is undecidable over Wdis, but the status of the two subfragments A¯B and A¯B¯ in the same class is still unknown. In secundis, and on a longer perspective, most of the results that we have reviewed for HS and their fragments still hold when we allow point intervals in the semantics, but a truly integrated modal theory of points and intervals has not been devised yet. In principle, such a theory would include most, if not all, point-based temporal logics such as  LTL[F,G]  or  LTL[S,U]  [59] as well as HS and its fragments creating, as sub product, a number of potentially interesting languages that feature suitable sets of mixed modalities, possibly revealing unexpected new decidable languages. Initial attempts in this sense include [4].Future research directions include, also, different approaches to modal reasoning. A particularly interesting one, currently at the level of initial experiments, aims to tackle the problem of the high complexity of interval temporal reasoning. Even in the simplest meaningful case, that is, the fragmentAA¯ in Fin, we have a theoretical complexity of NEXPTIME, which, in artificial intelligence, is considered very high and almost unsuitable for real-time reasoning. Consider for example a set of requirements with 50 symbols. To check its satisfiability, we have to expect a computation time proportional to O(2250), which is a very big number. The idea is to give up the completeness of the deduction method, in order to drastically cut this computation time, by means of Evolutionary Algorithms. We are exploring, in particular, a solution approach using multiobjective combinatorial optimization problem, which is identified and solved by using metaheuristics. Metaheuristics have been shown to be effective for difficult combinatorial optimization problems appearing in various industrial, economical, and scientific domains. Prominent examples of metaheuristics for combinatorial optimization are evolutionary algorithms, which have been found very powerful for satisfiability problems [60–63]. Initial experiments look very promising.


## 6. Addendum: Some Technical Results

Looking at the (yet incomplete) bibliography of this paper, we can immediately see that the amount of work published on this topic is quite big. In particular, every fragment of HS presents a potentially new problem, and it must be treated in a different way. In general, there is no free result when it comes to interval temporal reasoning, and even more so when we focus on the modal level. The technical level required to understand such results is not trivial and involves the knowledge of model theory, complexity theory, and terminating and nonterminating tableaux, among others. For the interested reader, we give here three representative examples: the first one is the maximal incomplete and minimal complete sets of first-order interval relations in the class of all linearly ordered sets (Table2), known from [35], the second one is the undecidability of full HS (a result known since [37], but presented here is a novel and simpler form), and the third one is the decidability of A (known since [44]). In the latter two cases, we focus our attention on the finite case, for the sake of simplicity.


### 6.1. Minimal Complete and Maximal Incomplete Sets of Allen’s Relations inLin

#### 6.1.1.  Preliminaries

Let us start by making precise the notions seen in Section3. Let S⊆AL. We say that FO+S  definesr∈AL over Lin, denoted by FO+S→Linr, if there exists FO+S-formula φ(x,y) such that φ(x,y)↔r(x,y) is valid on the class of concrete interval structures of signature (S∪{r}) based on linear orders. Note that FO+S→Linr for all r∈S. As an example, FO+{m}→Cb, as the formula ∃z(m(x,z)∧m(z,y))↔b(x,y) is a valid formula. As we have noticed, for each r∈AL, FO+{r}→ri; indeed, we have that ri(x,y)↔r(y,x) is always valid. Thus, we limit our attention to the set AL+={m,b,s,f,d,o}. Now, we say that S is complete overLin if and only if FO+S→Linr for all r∈AL+. Moreover, we say that S is a minimal complete set overLin, denoted by mcs (resp., maximally incomplete set overLin, denoted by MIS) if and only if it is complete (resp., incomplete) over Lin, and every proper subset (resp., every strict superset) of S is incomplete (resp., complete) over the same class.


#### 6.1.2.  Minimal Completeness

The following relation will be useful:r=m∨b. Notice that FO+{r}→m, since we have m(x,y)↔r(x,y)∧¬∃k(r(x,k)∧r(k,y)). Now, the case S={m} has been proved in [30] for the class of all unbounded dense linear orders; it is easy to check that no essential use of density or of the unboundedness is made. As for the case S={s,f}, consider the following definability equation:
(11)r(x,y)⟷∃k(s(x,k)∧f(y,k))∧¬∃k(f(k,x)∧s(k,y)).
We denote the right-hand part of the formula by ϕ(x,y). Assume first that ℱ⊨φ[[a,b],[c,d]]. We wish to show that ℱ⊨r([a,b],[c,d]), that is, b≤c. Suppose, by way of contradiction, that c<b. By assumption, there exists an interval k=[k1,k2] such that a=k1<b<k2 and k1<c<d=k2. Then a<c<b and c<b<d, hence [c,b]f[a,b] and [c,b]s[c,d], contradicting ℱ⊨¬∃k(f(k,[a,b])∧s(k,[c,d])). Conversely, suppose that ℱ⊨r([a,b],[c,d]), that is, a<b≤c<d. Then the interval k=[a,d] witnesses the first conjunct of ϕ. Moreover, any interval [a′,b] finishing [a,b] is disjoint from [c,d] and hence does not start it. The case S={o,s} can be dealt with by means of the following equations:
(12)r(x,y)⟷¬o(x,y)∧∀z(s(y,z)→¬o(x,z))∧({∨∃k(s(x,k)∧o(k,y))}∃k(s(x,k))∧¬∃k(s(y,k))∧¬∃k(s(k,y))∨∃k1∃k2(s(x,k1)∧s(y,k2)∧o(k1,k2))∨∃k(s(x,k)∧o(k,y))).
The intuition is that we consider three cases; namely, (1)y is a unit interval ending with the greatest (end) point in the linear order, (2)y does not end with the greatest point in the linear order, and (3)y is not a unit interval. It should be clear these cases are exhaustive, since the disjunction of (2) and (3) is equivalent to the negation of (1). The top, middle, and lower disjuncts in the last conjunct of the formula will hold, respectively, in cases (1), (2), and (3). As for the case S={o,f} we have that, since oi is definable in terms of o, it becomes precisely symmetric to the case {o,s}, and we can obtain ri (the inverse relation of r, defined above) in terms of oi and f, which allows us to define mi and hence m. In the case S={s,d}, we first define o, and then we obtain completeness from the completeness of {o,s}; to define o, it is sufficient to consider the following definability equation:
(13)o(x,y)⟷∃k(s(x,k)∧¬d(y,k)∧∃w(d(w,k)∧s(w,y)))∧∃w(s(w,y)∧∀k(d(x,k)→d(w,k))).
The case S={f,d} is symmetric to {s,d}, and in the case S={s,b}, we can show that {s,b} can define d, and then completeness will follow from the completeness of {s,d} which was proven above. This can be done via showing that {s,b} can define r′=d∨f. (Note that r′([a,b],[c,d]) if and only if d([a,b],[c,d])∨f([a,b],[c,d]) if and only if c<a<b≤d.) It is then immediate to see that the following definition is correct:
(14)d(x,y)⟷∃k(s(x,k)∧r′(k,y)).
It thus remains for us to show how to define r′ in terms of s and b, which can be done by means of the following definition:
(15)r′(x,y)⟷ψ(x,y)∧∃z(s(z,y))∧∀z((s(z,x)∨z=x)→¬s(z,y))∧∀k(b(y,k)→b(x,k))∧(¬∃k(s(y,k))∨∃k(s(x,k))),
where
(16)ψ(x,y):=(¬∃k(b(k,y))∧∀z(¬∃k(b(k,z))→same_beg(z,y)))∨(∃k(b(k,x))∧∀z(b(z,y)→b(z,x))),same_beg(z,y):=z=y∨s(z,y)∨s(y,z).
Finally, the case S={f,b} is symmetric to the previous one.


#### 6.1.3.  Maximal Incompleteness

We first prove the incompleteness in the caseS={s}. Consider the structure ℱ=〈𝕀(ℚ),s〉, where ℚ is the set or rational numbers with their usual ordering. Define ζ:𝕀(ℚ)→𝕀(ℚ) such that
(17)ζ:[a,b]↦[a,a+2·|b-a|].
In other words, the image of any interval [a,b] under ζ has the same beginning point, but double the length of [a,b]. We claim that ζ is an automorphism of the structure ℱ. It is clear that ζ is a bijection. Further, [a1,b1]s[a2,b2] if and only if a1=a2 and b1<b2, that is, if and only if a1=a2 and a1+2·|b1-a1|<a2+2·|b2-a2|, which happens if and only if ζ([a1,b1])sζ([a2,b2]). Now, we show that b is not respected, for which it is enough to observe that, since ζ([0,1])=[0,2] and ζ([2,3])=[2,4], for all formulas φ(x,y) of FO+{s} we have that ℱ⊨φ([0,1,2,3]) if and only if ℱ⊨φ([0,2,2,4]), but at the same time [0,1]b[2,3] and ¬([0,2]b[2,4]). A symmetric construction proves the incompleteness of the case S={f}. For the case S={o,b,d}, it suffices to consider the structure ℱ=〈𝕀(𝔻),o,b,d〉 where 𝔻 is the subset {-1,0,1} of ℤ with the usual ordering. An automorphism of this structure can be defined by taking ζ:𝕀(𝔻)→𝕀(𝔻) such that ζ([-1,1])=[-1,1], ζ([-1,0])=[0,1], and ζ([0,1])=[-1,0]. These results suffice to prove the correctness of Table 2.


### 6.2. Undecidability of HS inFin

#### 6.2.1.  Intuition

The satisfiability problem for HS has been shown undecidable when interpreted in nearly any interesting class of linearly ordered sets [6, 37]. The argument presented there was innovative at that time; it was based on a clever reduction from the Halting Problem for Turing machines to the satisfiability problem for HS. On the other hand, the argument is long and complex and, probably, a bit difficult to visualize. In the recent past, as we have seen in this paper, smaller and smaller fragments of HS have been proved to be undecidable as well, and in most cases a simpler argument structure has been used, based on a reduction from the “right” tiling problem. Tiling problems [36, 64] are a class of problems based on the same idea and conveniently modulated in order to represent a particular complexity class or a particular undecidability degree. In general, an instance of tiling problem consists of a set of tile types T, that one can imagine as squared tiles with a color on each border, and (a portion of) the integer plane, and its asks to find, if exists, a function f from T to the points in the plane that respects the colors, that is, if two tiles share a side, that side must be of the same color; depending on the particular tiling problem, additional constraints might be added. The one we need here is known as Finite Tiling Problem (FTP), proposed in the literature in different, yet closely related, versions. Here we refer to the one introduced and shown to be undecidable in [65], and we formally define it as the problem of establishing whether there exist two natural numbers k and l such that a finite set of tile types T, containing two distinguished tile types t0 and tf, can correctly tile the finite plane {0,…,k}×{0,…,l}, under the additional restriction that f(0,0)=t0 and f(k,l)=tf.


#### 6.2.2.  The Reduction

Reducing the FTP to the satisfiability problem for HS corresponds to write a (parametric-in-T) HS-formula φFTP which is satisfiable if and only if T can tile the finite plane {0,…,k}×{0,…,l} for some k and l. As FTP is undecidable, no length limits for φFTP are needed; if we were proving instead that a particular fragment ℱ is hard for some complexity class, the reduction formula should be polynomial in length to preserve the complexity. Formulas of HS are built over an (unconstrained) set 𝒜𝒫 of propositional letters, in which we can assume to have enough letters to our purpose. The idea is that φFTP axiomatizes the existence of a sequence of levels (denoted by the letter lev), which is initiated by a symbol * and composed by a finite number of tiles (denoted by t). Each tile is connected to the corresponding one by a letter corr, and corrs do not start, finish, or are contained in any other corr, which leaves as the only option, a one-to-one correspondence between tiles and, also, levels with the same number of tiles. To ensure this, we just need to make sure that corrs do not skip any level, nor are inside any level. To finalize the encoding, we assert that meeting tiles (those which share a vertical side) agree on their colors, as well as corresponding tiles (sharing an horizontal side), that is, those connected by a corr. Our encoding, therefore, will make use of, among others, the propositional letters *,tile,corr,lev,t0,tf,t1,…,tk, plus two special letters levs and levf to denote the first and the last level. Moreover, letters of type ti are assumed to have colors r(ti),l(ti),u(ti), and d(ti). To simplify the encoding, it is convenient to put tiles and *s on intervals of the type [a,a+1], which, on finite orders, are easily captured by [B]⊥.


#### 6.2.3.  The Encoding

The formulaφFTP is the conjunction of the following formulas: (18)φ1≡〈A〉*∧〈A〉(lev∧levs)∧〈L〉(lev∧levf),φ2≡[U]((levs∨levf)→lev),φ3≡[U](((*∨tile)→[B]⊥)∧([B]⊥→(*∨tile))),φ4≡[U](lev→(〈B〉*∧[D]([B]⊥→tile)∧[E]([B]⊥→tile))),φ5≡[U](*→¬tile),φ6≡[U](levs→¬levf),φ7≡[U](levs→[A]¬levs∧[L]¬levs),φ8≡[U](levf→[A¯]¬levf∧[L]¬levf),φ9≡[U](lev→(¬(〈D〉lev∨〈B〉lev∨〈E〉lev))),φ10≡[U](lev→〈A〉(lev∨levf)),φ11≡⋀z∈{s,f}[U](levz→[D](tile→tilez)),φ12≡⋀z∈{s,f}[U](levz→[E](tile→tilez)),φ13≡[U](tile∧¬tiles→(〈A〉corr∧〈A¯〉corr)),φ14≡[U](tiles→〈A〉corr),φ15≡[U](tilef→〈A¯〉corr),φ16≡[U](*→¬〈A〉corr),φ17≡[U](corr→¬(〈B〉(〈A〉*∧〈B〉〈A〉*))),φ18≡[U](corr→¬(〈B〉corr∨〈D〉corr∨〈E〉corr)),φ19≡[U](tile→⋁(t∈T)t),φ20≡〈A〉〈A〉(tile∧t0),φ21≡〈L〉(levs∧〈E〉(tile∧tf)),φ22≡[U](⋀ti∈T((ti∧¬〈A〉*)→〈A〉⋁tjr(ti)=l(tj)ti)),φ23≡[U](⋀(ti∈T)({⋁tju(ti)=d(tj)ti}(ti∧〈A〉corr)→[A](corr→〈A〉⋁tju(ti)=d(tj)ti))).


### 6.3. Decidability of the FragmentA in theFin

Let us now consider the problem of proving that satisfiability ofA over Fin is decidable in NEXPTIME.


#### 6.3.1. Preliminary Definitions

We start with some useful definitions. Letφ be an A-formula to be checked for satisfiability and let 𝒜𝒫 be the set of its propositional letters. The closureCL(φ) of φ is the set of all subformulae of φ and of their negations (we identify ¬¬ψ with ψ). The set of temporal requests of φ is the set TF(φ) of all temporal formulae in CL(φ), that is, TF(φ)={〈A〉ψ,[A]ψ∈CL(φ)}. By induction on the structure of φ, we can easily prove that for every formula φ, |CL(φ)|≤2·|φ|, while TF(φ)∣≤2·(|φ|-1). A φ-atom is a set A⊆CL(φ) such that: (1) for every ψ∈CL(φ), ψ∈A if and only if ¬ψ∉A; (2) for every ψ1∨ψ2∈CL(φ), ψ1∨ψ2∈A if and only if ψ1∈A or ψ2∈A. We denote the set of all φ-atoms by Aφ; clearly, |Aφ|≤2|φ|. Now, atoms are connected by the natural binary relation; in fact, we can define Rφ as a binary relation over Aφ in such a way that for every pair of atoms A,A′∈Aφ, ARφA′ if and only if for every [A]ψ∈CL(φ), if [A]ψ∈A, then ψ∈A′. At this point, we can define a class of extended models, called fulfilling labeled structures, as follows. First, a φ-labeled structure (LIS, for short) is a pair L=〈𝔻,𝕀(𝔻),ℒ〉, where ℒ:𝕀(𝔻)→Aφ is a labeling function that for every pair of meeting intervals [a,b],[b,c]∈𝕀(𝔻), ℒ([a,b])Rφℒ([b,c]). Second, we say that L is fulfilling if and only if for every temporal formula 〈A〉ψ∈TF(φ) and every interval [a,b]∈𝕀(𝔻), if 〈A〉ψ∈ℒ([a,b]), then there exists c>b such that ψ∈ℒ([b,c]). Clearly, there is a close relationship between models for a formula φ and fulfilling labeled structures for it. Indeed, we can easily prove that φ is satisfiable on a model M and interval [a,b] if and only if there exists a fulfilling labeled structure L, based on the same domain as M, and such that φ∈ℒ([a,b]). Moreover, because of the simple structure of the fragment A, satisfiability of A-formulas over Fin is reducible to initial satisfiability, that is, satisfiability over the interval [0,1]. So, we can now say that φ is finitely satisfiable if and only if there exists a fulfilling labeled structure L such that φ∈ℒ([0,1]).


#### 6.3.2. Eliminating Points

Since fulfillingLISs satisfying φ may be arbitrarily large, we must find a way to finitely establish their existence. In the following, we give a bound on the size of finite-fulfilling LISs that must be checked for satisfiability, when searching for finite φ-models. To prove this result, we take advantage of the following two fundamental properties of LISs: (1) the labeling of a pair of intervals [a,b],[c,b] with the same right endpoint b must agree on temporal formulae (since every right neighbor of [a,b] is also a right neighbor of [b,c], we have that for every existential formula 〈A〉ψ∈TF(φ), 〈A〉ψ∈ℒ([a,b]) if and only if 〈A〉ψ∈ℒ([c,b]) and similarly for universal formulas); (2)(|TF(φ)|/2) right-neighboring intervals suffice to fulfill the existential formulas belonging to the labeling of an interval [a,b] (the number of right-neighboring intervals which are needed to fulfill all existential formulae of ℒ([a,b]) is bounded by the number of 〈A〉-formulas in TF(φ), and, at worst, different existential formulae are satisfied by different right-neighboring intervals). By exploiting these properties, we can define, for every point a in a fulfilling labeled structure L the set REQ(a) (of requests) of all and only the temporal formulas belonging to the labeling of the intervals ending at a, and REQ(φ) as the set of all possible sets of requests, so that |REQ(φ)|=2((TF(φ)/2)). We are ready to prove our main result. Indeed, we now prove that, if m=(|TF(φ)|/2) and if L is a finite-fulfilling LIS that satisfies φ, then there exists a finite-fulfilling LIS  L¯ that satisfies φ as well and for every a∈𝔻¯∖{1},  REQ(a) occurs at most m times. To see this, assume L does not respect the given condition, so assume that for some a∈𝔻, different from 1,  REQ(a)=R occurs more than m times. We now define a sequence of LISs  L=L0,L1,…, each one of which is fulfilling and progressively smaller, and such that the last one of the sequence meets the condition on the number of occurrences of R. Our first step consists in turning L0 into L1, in such a way that one of the points that presented the set of requests R has been eliminated. Assume that a1<a2<⋯<an(n>m)  are the points in L with set of requests R; the LIS  L1 is defined over the domain 𝔻1=𝔻0∖{a1}, and in such a way that ℒ1 is the projection on the remaining intervals of ℒ. The structure so-defined L1 is obviously a finite LIS, but it is not necessarily fulfilling. In fact, the removal of a1 causes the removal of all intervals beginning or ending at a1. While the removal of intervals beginning at a1 is not critical (as the requests possibly satisfied by them have been removed as well), there can be some points a<a1 such that some formulas 〈A〉ψ∈REQ(a) are fulfilled in L0, but they are not fulfilled in L1 anymore. We fix such defects (if any) one-by-one by properly redefining ℒ1. Let a<a1 and 〈A〉ψ∈REQ(a) such that ψ∈ℒ0([a,a1]) and that there is no a′∈𝔻∖{a1} such that ψ∈ℒ1([a,a′]). Since REQ(a) contains at most m  〈A〉-formulas, there exists at least one point ai∈{a2,…,an} such that the atom ℒ1([a,ai]) either fulfills no 〈A〉-formulas or it fulfills only 〈A〉-formulae which are also fulfilled by some other atom of the same type. Let ai one of such points. We can redefine ℒ1([a,ai]) by putting ℒ1([a,ai])=ℒ0([a,a1]), thus fixing the problem with 〈A〉ψ∈REQ(a). Notice that, since REQ(a1)=REQ(ai)=R, such a change has no impact on the right-neighboring intervals of [a,ai]. In a similar way, we can fix the other possible defects caused by the removal of a1. We repeat such a process until we are left with exactly m distinct points where R occurs, defining, as we said at the beginning, a sequence of LISs. The last one of such a sequence, L¯, is, clearly, a fulfilling LIS that satisfies φ, and no set of requests occurs more than m times on it.


#### 6.3.3. The Result

It is now straightforward to observe that we have reduced the finite satisfiability problem for aA-formula φ to the search of a labeled structure whose dimension is exponential, at most, in the length of φ; a nondeterministic, sound, complete, and terminating searching procedure can be now devised, allowing us to conclude that our problem is, not only decidable, but also in NEXPTIME.


## 6.1. Minimal Complete and Maximal Incomplete Sets of Allen’s Relations inLin

### 6.1.1.  Preliminaries

Let us start by making precise the notions seen in Section3. Let S⊆AL. We say that FO+S  definesr∈AL over Lin, denoted by FO+S→Linr, if there exists FO+S-formula φ(x,y) such that φ(x,y)↔r(x,y) is valid on the class of concrete interval structures of signature (S∪{r}) based on linear orders. Note that FO+S→Linr for all r∈S. As an example, FO+{m}→Cb, as the formula ∃z(m(x,z)∧m(z,y))↔b(x,y) is a valid formula. As we have noticed, for each r∈AL, FO+{r}→ri; indeed, we have that ri(x,y)↔r(y,x) is always valid. Thus, we limit our attention to the set AL+={m,b,s,f,d,o}. Now, we say that S is complete overLin if and only if FO+S→Linr for all r∈AL+. Moreover, we say that S is a minimal complete set overLin, denoted by mcs (resp., maximally incomplete set overLin, denoted by MIS) if and only if it is complete (resp., incomplete) over Lin, and every proper subset (resp., every strict superset) of S is incomplete (resp., complete) over the same class.


### 6.1.2.  Minimal Completeness

The following relation will be useful:r=m∨b. Notice that FO+{r}→m, since we have m(x,y)↔r(x,y)∧¬∃k(r(x,k)∧r(k,y)). Now, the case S={m} has been proved in [30] for the class of all unbounded dense linear orders; it is easy to check that no essential use of density or of the unboundedness is made. As for the case S={s,f}, consider the following definability equation:
(11)r(x,y)⟷∃k(s(x,k)∧f(y,k))∧¬∃k(f(k,x)∧s(k,y)).
We denote the right-hand part of the formula by ϕ(x,y). Assume first that ℱ⊨φ[[a,b],[c,d]]. We wish to show that ℱ⊨r([a,b],[c,d]), that is, b≤c. Suppose, by way of contradiction, that c<b. By assumption, there exists an interval k=[k1,k2] such that a=k1<b<k2 and k1<c<d=k2. Then a<c<b and c<b<d, hence [c,b]f[a,b] and [c,b]s[c,d], contradicting ℱ⊨¬∃k(f(k,[a,b])∧s(k,[c,d])). Conversely, suppose that ℱ⊨r([a,b],[c,d]), that is, a<b≤c<d. Then the interval k=[a,d] witnesses the first conjunct of ϕ. Moreover, any interval [a′,b] finishing [a,b] is disjoint from [c,d] and hence does not start it. The case S={o,s} can be dealt with by means of the following equations:
(12)r(x,y)⟷¬o(x,y)∧∀z(s(y,z)→¬o(x,z))∧({∨∃k(s(x,k)∧o(k,y))}∃k(s(x,k))∧¬∃k(s(y,k))∧¬∃k(s(k,y))∨∃k1∃k2(s(x,k1)∧s(y,k2)∧o(k1,k2))∨∃k(s(x,k)∧o(k,y))).
The intuition is that we consider three cases; namely, (1)y is a unit interval ending with the greatest (end) point in the linear order, (2)y does not end with the greatest point in the linear order, and (3)y is not a unit interval. It should be clear these cases are exhaustive, since the disjunction of (2) and (3) is equivalent to the negation of (1). The top, middle, and lower disjuncts in the last conjunct of the formula will hold, respectively, in cases (1), (2), and (3). As for the case S={o,f} we have that, since oi is definable in terms of o, it becomes precisely symmetric to the case {o,s}, and we can obtain ri (the inverse relation of r, defined above) in terms of oi and f, which allows us to define mi and hence m. In the case S={s,d}, we first define o, and then we obtain completeness from the completeness of {o,s}; to define o, it is sufficient to consider the following definability equation:
(13)o(x,y)⟷∃k(s(x,k)∧¬d(y,k)∧∃w(d(w,k)∧s(w,y)))∧∃w(s(w,y)∧∀k(d(x,k)→d(w,k))).
The case S={f,d} is symmetric to {s,d}, and in the case S={s,b}, we can show that {s,b} can define d, and then completeness will follow from the completeness of {s,d} which was proven above. This can be done via showing that {s,b} can define r′=d∨f. (Note that r′([a,b],[c,d]) if and only if d([a,b],[c,d])∨f([a,b],[c,d]) if and only if c<a<b≤d.) It is then immediate to see that the following definition is correct:
(14)d(x,y)⟷∃k(s(x,k)∧r′(k,y)).
It thus remains for us to show how to define r′ in terms of s and b, which can be done by means of the following definition:
(15)r′(x,y)⟷ψ(x,y)∧∃z(s(z,y))∧∀z((s(z,x)∨z=x)→¬s(z,y))∧∀k(b(y,k)→b(x,k))∧(¬∃k(s(y,k))∨∃k(s(x,k))),
where
(16)ψ(x,y):=(¬∃k(b(k,y))∧∀z(¬∃k(b(k,z))→same_beg(z,y)))∨(∃k(b(k,x))∧∀z(b(z,y)→b(z,x))),same_beg(z,y):=z=y∨s(z,y)∨s(y,z).
Finally, the case S={f,b} is symmetric to the previous one.


### 6.1.3.  Maximal Incompleteness

We first prove the incompleteness in the caseS={s}. Consider the structure ℱ=〈𝕀(ℚ),s〉, where ℚ is the set or rational numbers with their usual ordering. Define ζ:𝕀(ℚ)→𝕀(ℚ) such that
(17)ζ:[a,b]↦[a,a+2·|b-a|].
In other words, the image of any interval [a,b] under ζ has the same beginning point, but double the length of [a,b]. We claim that ζ is an automorphism of the structure ℱ. It is clear that ζ is a bijection. Further, [a1,b1]s[a2,b2] if and only if a1=a2 and b1<b2, that is, if and only if a1=a2 and a1+2·|b1-a1|<a2+2·|b2-a2|, which happens if and only if ζ([a1,b1])sζ([a2,b2]). Now, we show that b is not respected, for which it is enough to observe that, since ζ([0,1])=[0,2] and ζ([2,3])=[2,4], for all formulas φ(x,y) of FO+{s} we have that ℱ⊨φ([0,1,2,3]) if and only if ℱ⊨φ([0,2,2,4]), but at the same time [0,1]b[2,3] and ¬([0,2]b[2,4]). A symmetric construction proves the incompleteness of the case S={f}. For the case S={o,b,d}, it suffices to consider the structure ℱ=〈𝕀(𝔻),o,b,d〉 where 𝔻 is the subset {-1,0,1} of ℤ with the usual ordering. An automorphism of this structure can be defined by taking ζ:𝕀(𝔻)→𝕀(𝔻) such that ζ([-1,1])=[-1,1], ζ([-1,0])=[0,1], and ζ([0,1])=[-1,0]. These results suffice to prove the correctness of Table 2.


## 6.1.1.  Preliminaries

Let us start by making precise the notions seen in Section3. Let S⊆AL. We say that FO+S  definesr∈AL over Lin, denoted by FO+S→Linr, if there exists FO+S-formula φ(x,y) such that φ(x,y)↔r(x,y) is valid on the class of concrete interval structures of signature (S∪{r}) based on linear orders. Note that FO+S→Linr for all r∈S. As an example, FO+{m}→Cb, as the formula ∃z(m(x,z)∧m(z,y))↔b(x,y) is a valid formula. As we have noticed, for each r∈AL, FO+{r}→ri; indeed, we have that ri(x,y)↔r(y,x) is always valid. Thus, we limit our attention to the set AL+={m,b,s,f,d,o}. Now, we say that S is complete overLin if and only if FO+S→Linr for all r∈AL+. Moreover, we say that S is a minimal complete set overLin, denoted by mcs (resp., maximally incomplete set overLin, denoted by MIS) if and only if it is complete (resp., incomplete) over Lin, and every proper subset (resp., every strict superset) of S is incomplete (resp., complete) over the same class.


## 6.1.2.  Minimal Completeness

The following relation will be useful:r=m∨b. Notice that FO+{r}→m, since we have m(x,y)↔r(x,y)∧¬∃k(r(x,k)∧r(k,y)). Now, the case S={m} has been proved in [30] for the class of all unbounded dense linear orders; it is easy to check that no essential use of density or of the unboundedness is made. As for the case S={s,f}, consider the following definability equation:
(11)r(x,y)⟷∃k(s(x,k)∧f(y,k))∧¬∃k(f(k,x)∧s(k,y)).
We denote the right-hand part of the formula by ϕ(x,y). Assume first that ℱ⊨φ[[a,b],[c,d]]. We wish to show that ℱ⊨r([a,b],[c,d]), that is, b≤c. Suppose, by way of contradiction, that c<b. By assumption, there exists an interval k=[k1,k2] such that a=k1<b<k2 and k1<c<d=k2. Then a<c<b and c<b<d, hence [c,b]f[a,b] and [c,b]s[c,d], contradicting ℱ⊨¬∃k(f(k,[a,b])∧s(k,[c,d])). Conversely, suppose that ℱ⊨r([a,b],[c,d]), that is, a<b≤c<d. Then the interval k=[a,d] witnesses the first conjunct of ϕ. Moreover, any interval [a′,b] finishing [a,b] is disjoint from [c,d] and hence does not start it. The case S={o,s} can be dealt with by means of the following equations:
(12)r(x,y)⟷¬o(x,y)∧∀z(s(y,z)→¬o(x,z))∧({∨∃k(s(x,k)∧o(k,y))}∃k(s(x,k))∧¬∃k(s(y,k))∧¬∃k(s(k,y))∨∃k1∃k2(s(x,k1)∧s(y,k2)∧o(k1,k2))∨∃k(s(x,k)∧o(k,y))).
The intuition is that we consider three cases; namely, (1)y is a unit interval ending with the greatest (end) point in the linear order, (2)y does not end with the greatest point in the linear order, and (3)y is not a unit interval. It should be clear these cases are exhaustive, since the disjunction of (2) and (3) is equivalent to the negation of (1). The top, middle, and lower disjuncts in the last conjunct of the formula will hold, respectively, in cases (1), (2), and (3). As for the case S={o,f} we have that, since oi is definable in terms of o, it becomes precisely symmetric to the case {o,s}, and we can obtain ri (the inverse relation of r, defined above) in terms of oi and f, which allows us to define mi and hence m. In the case S={s,d}, we first define o, and then we obtain completeness from the completeness of {o,s}; to define o, it is sufficient to consider the following definability equation:
(13)o(x,y)⟷∃k(s(x,k)∧¬d(y,k)∧∃w(d(w,k)∧s(w,y)))∧∃w(s(w,y)∧∀k(d(x,k)→d(w,k))).
The case S={f,d} is symmetric to {s,d}, and in the case S={s,b}, we can show that {s,b} can define d, and then completeness will follow from the completeness of {s,d} which was proven above. This can be done via showing that {s,b} can define r′=d∨f. (Note that r′([a,b],[c,d]) if and only if d([a,b],[c,d])∨f([a,b],[c,d]) if and only if c<a<b≤d.) It is then immediate to see that the following definition is correct:
(14)d(x,y)⟷∃k(s(x,k)∧r′(k,y)).
It thus remains for us to show how to define r′ in terms of s and b, which can be done by means of the following definition:
(15)r′(x,y)⟷ψ(x,y)∧∃z(s(z,y))∧∀z((s(z,x)∨z=x)→¬s(z,y))∧∀k(b(y,k)→b(x,k))∧(¬∃k(s(y,k))∨∃k(s(x,k))),
where
(16)ψ(x,y):=(¬∃k(b(k,y))∧∀z(¬∃k(b(k,z))→same_beg(z,y)))∨(∃k(b(k,x))∧∀z(b(z,y)→b(z,x))),same_beg(z,y):=z=y∨s(z,y)∨s(y,z).
Finally, the case S={f,b} is symmetric to the previous one.


## 6.1.3.  Maximal Incompleteness

We first prove the incompleteness in the caseS={s}. Consider the structure ℱ=〈𝕀(ℚ),s〉, where ℚ is the set or rational numbers with their usual ordering. Define ζ:𝕀(ℚ)→𝕀(ℚ) such that
(17)ζ:[a,b]↦[a,a+2·|b-a|].
In other words, the image of any interval [a,b] under ζ has the same beginning point, but double the length of [a,b]. We claim that ζ is an automorphism of the structure ℱ. It is clear that ζ is a bijection. Further, [a1,b1]s[a2,b2] if and only if a1=a2 and b1<b2, that is, if and only if a1=a2 and a1+2·|b1-a1|<a2+2·|b2-a2|, which happens if and only if ζ([a1,b1])sζ([a2,b2]). Now, we show that b is not respected, for which it is enough to observe that, since ζ([0,1])=[0,2] and ζ([2,3])=[2,4], for all formulas φ(x,y) of FO+{s} we have that ℱ⊨φ([0,1,2,3]) if and only if ℱ⊨φ([0,2,2,4]), but at the same time [0,1]b[2,3] and ¬([0,2]b[2,4]). A symmetric construction proves the incompleteness of the case S={f}. For the case S={o,b,d}, it suffices to consider the structure ℱ=〈𝕀(𝔻),o,b,d〉 where 𝔻 is the subset {-1,0,1} of ℤ with the usual ordering. An automorphism of this structure can be defined by taking ζ:𝕀(𝔻)→𝕀(𝔻) such that ζ([-1,1])=[-1,1], ζ([-1,0])=[0,1], and ζ([0,1])=[-1,0]. These results suffice to prove the correctness of Table 2.


## 6.2. Undecidability of HS inFin

### 6.2.1.  Intuition

The satisfiability problem for HS has been shown undecidable when interpreted in nearly any interesting class of linearly ordered sets [6, 37]. The argument presented there was innovative at that time; it was based on a clever reduction from the Halting Problem for Turing machines to the satisfiability problem for HS. On the other hand, the argument is long and complex and, probably, a bit difficult to visualize. In the recent past, as we have seen in this paper, smaller and smaller fragments of HS have been proved to be undecidable as well, and in most cases a simpler argument structure has been used, based on a reduction from the “right” tiling problem. Tiling problems [36, 64] are a class of problems based on the same idea and conveniently modulated in order to represent a particular complexity class or a particular undecidability degree. In general, an instance of tiling problem consists of a set of tile types T, that one can imagine as squared tiles with a color on each border, and (a portion of) the integer plane, and its asks to find, if exists, a function f from T to the points in the plane that respects the colors, that is, if two tiles share a side, that side must be of the same color; depending on the particular tiling problem, additional constraints might be added. The one we need here is known as Finite Tiling Problem (FTP), proposed in the literature in different, yet closely related, versions. Here we refer to the one introduced and shown to be undecidable in [65], and we formally define it as the problem of establishing whether there exist two natural numbers k and l such that a finite set of tile types T, containing two distinguished tile types t0 and tf, can correctly tile the finite plane {0,…,k}×{0,…,l}, under the additional restriction that f(0,0)=t0 and f(k,l)=tf.


### 6.2.2.  The Reduction

Reducing the FTP to the satisfiability problem for HS corresponds to write a (parametric-in-T) HS-formula φFTP which is satisfiable if and only if T can tile the finite plane {0,…,k}×{0,…,l} for some k and l. As FTP is undecidable, no length limits for φFTP are needed; if we were proving instead that a particular fragment ℱ is hard for some complexity class, the reduction formula should be polynomial in length to preserve the complexity. Formulas of HS are built over an (unconstrained) set 𝒜𝒫 of propositional letters, in which we can assume to have enough letters to our purpose. The idea is that φFTP axiomatizes the existence of a sequence of levels (denoted by the letter lev), which is initiated by a symbol * and composed by a finite number of tiles (denoted by t). Each tile is connected to the corresponding one by a letter corr, and corrs do not start, finish, or are contained in any other corr, which leaves as the only option, a one-to-one correspondence between tiles and, also, levels with the same number of tiles. To ensure this, we just need to make sure that corrs do not skip any level, nor are inside any level. To finalize the encoding, we assert that meeting tiles (those which share a vertical side) agree on their colors, as well as corresponding tiles (sharing an horizontal side), that is, those connected by a corr. Our encoding, therefore, will make use of, among others, the propositional letters *,tile,corr,lev,t0,tf,t1,…,tk, plus two special letters levs and levf to denote the first and the last level. Moreover, letters of type ti are assumed to have colors r(ti),l(ti),u(ti), and d(ti). To simplify the encoding, it is convenient to put tiles and *s on intervals of the type [a,a+1], which, on finite orders, are easily captured by [B]⊥.


### 6.2.3.  The Encoding

The formulaφFTP is the conjunction of the following formulas: (18)φ1≡〈A〉*∧〈A〉(lev∧levs)∧〈L〉(lev∧levf),φ2≡[U]((levs∨levf)→lev),φ3≡[U](((*∨tile)→[B]⊥)∧([B]⊥→(*∨tile))),φ4≡[U](lev→(〈B〉*∧[D]([B]⊥→tile)∧[E]([B]⊥→tile))),φ5≡[U](*→¬tile),φ6≡[U](levs→¬levf),φ7≡[U](levs→[A]¬levs∧[L]¬levs),φ8≡[U](levf→[A¯]¬levf∧[L]¬levf),φ9≡[U](lev→(¬(〈D〉lev∨〈B〉lev∨〈E〉lev))),φ10≡[U](lev→〈A〉(lev∨levf)),φ11≡⋀z∈{s,f}[U](levz→[D](tile→tilez)),φ12≡⋀z∈{s,f}[U](levz→[E](tile→tilez)),φ13≡[U](tile∧¬tiles→(〈A〉corr∧〈A¯〉corr)),φ14≡[U](tiles→〈A〉corr),φ15≡[U](tilef→〈A¯〉corr),φ16≡[U](*→¬〈A〉corr),φ17≡[U](corr→¬(〈B〉(〈A〉*∧〈B〉〈A〉*))),φ18≡[U](corr→¬(〈B〉corr∨〈D〉corr∨〈E〉corr)),φ19≡[U](tile→⋁(t∈T)t),φ20≡〈A〉〈A〉(tile∧t0),φ21≡〈L〉(levs∧〈E〉(tile∧tf)),φ22≡[U](⋀ti∈T((ti∧¬〈A〉*)→〈A〉⋁tjr(ti)=l(tj)ti)),φ23≡[U](⋀(ti∈T)({⋁tju(ti)=d(tj)ti}(ti∧〈A〉corr)→[A](corr→〈A〉⋁tju(ti)=d(tj)ti))).


## 6.2.1.  Intuition

The satisfiability problem for HS has been shown undecidable when interpreted in nearly any interesting class of linearly ordered sets [6, 37]. The argument presented there was innovative at that time; it was based on a clever reduction from the Halting Problem for Turing machines to the satisfiability problem for HS. On the other hand, the argument is long and complex and, probably, a bit difficult to visualize. In the recent past, as we have seen in this paper, smaller and smaller fragments of HS have been proved to be undecidable as well, and in most cases a simpler argument structure has been used, based on a reduction from the “right” tiling problem. Tiling problems [36, 64] are a class of problems based on the same idea and conveniently modulated in order to represent a particular complexity class or a particular undecidability degree. In general, an instance of tiling problem consists of a set of tile types T, that one can imagine as squared tiles with a color on each border, and (a portion of) the integer plane, and its asks to find, if exists, a function f from T to the points in the plane that respects the colors, that is, if two tiles share a side, that side must be of the same color; depending on the particular tiling problem, additional constraints might be added. The one we need here is known as Finite Tiling Problem (FTP), proposed in the literature in different, yet closely related, versions. Here we refer to the one introduced and shown to be undecidable in [65], and we formally define it as the problem of establishing whether there exist two natural numbers k and l such that a finite set of tile types T, containing two distinguished tile types t0 and tf, can correctly tile the finite plane {0,…,k}×{0,…,l}, under the additional restriction that f(0,0)=t0 and f(k,l)=tf.


## 6.2.2.  The Reduction

Reducing the FTP to the satisfiability problem for HS corresponds to write a (parametric-in-T) HS-formula φFTP which is satisfiable if and only if T can tile the finite plane {0,…,k}×{0,…,l} for some k and l. As FTP is undecidable, no length limits for φFTP are needed; if we were proving instead that a particular fragment ℱ is hard for some complexity class, the reduction formula should be polynomial in length to preserve the complexity. Formulas of HS are built over an (unconstrained) set 𝒜𝒫 of propositional letters, in which we can assume to have enough letters to our purpose. The idea is that φFTP axiomatizes the existence of a sequence of levels (denoted by the letter lev), which is initiated by a symbol * and composed by a finite number of tiles (denoted by t). Each tile is connected to the corresponding one by a letter corr, and corrs do not start, finish, or are contained in any other corr, which leaves as the only option, a one-to-one correspondence between tiles and, also, levels with the same number of tiles. To ensure this, we just need to make sure that corrs do not skip any level, nor are inside any level. To finalize the encoding, we assert that meeting tiles (those which share a vertical side) agree on their colors, as well as corresponding tiles (sharing an horizontal side), that is, those connected by a corr. Our encoding, therefore, will make use of, among others, the propositional letters *,tile,corr,lev,t0,tf,t1,…,tk, plus two special letters levs and levf to denote the first and the last level. Moreover, letters of type ti are assumed to have colors r(ti),l(ti),u(ti), and d(ti). To simplify the encoding, it is convenient to put tiles and *s on intervals of the type [a,a+1], which, on finite orders, are easily captured by [B]⊥.


## 6.2.3.  The Encoding

The formulaφFTP is the conjunction of the following formulas: (18)φ1≡〈A〉*∧〈A〉(lev∧levs)∧〈L〉(lev∧levf),φ2≡[U]((levs∨levf)→lev),φ3≡[U](((*∨tile)→[B]⊥)∧([B]⊥→(*∨tile))),φ4≡[U](lev→(〈B〉*∧[D]([B]⊥→tile)∧[E]([B]⊥→tile))),φ5≡[U](*→¬tile),φ6≡[U](levs→¬levf),φ7≡[U](levs→[A]¬levs∧[L]¬levs),φ8≡[U](levf→[A¯]¬levf∧[L]¬levf),φ9≡[U](lev→(¬(〈D〉lev∨〈B〉lev∨〈E〉lev))),φ10≡[U](lev→〈A〉(lev∨levf)),φ11≡⋀z∈{s,f}[U](levz→[D](tile→tilez)),φ12≡⋀z∈{s,f}[U](levz→[E](tile→tilez)),φ13≡[U](tile∧¬tiles→(〈A〉corr∧〈A¯〉corr)),φ14≡[U](tiles→〈A〉corr),φ15≡[U](tilef→〈A¯〉corr),φ16≡[U](*→¬〈A〉corr),φ17≡[U](corr→¬(〈B〉(〈A〉*∧〈B〉〈A〉*))),φ18≡[U](corr→¬(〈B〉corr∨〈D〉corr∨〈E〉corr)),φ19≡[U](tile→⋁(t∈T)t),φ20≡〈A〉〈A〉(tile∧t0),φ21≡〈L〉(levs∧〈E〉(tile∧tf)),φ22≡[U](⋀ti∈T((ti∧¬〈A〉*)→〈A〉⋁tjr(ti)=l(tj)ti)),φ23≡[U](⋀(ti∈T)({⋁tju(ti)=d(tj)ti}(ti∧〈A〉corr)→[A](corr→〈A〉⋁tju(ti)=d(tj)ti))).


## 6.3. Decidability of the FragmentA in theFin

Let us now consider the problem of proving that satisfiability ofA over Fin is decidable in NEXPTIME.


### 6.3.1. Preliminary Definitions

We start with some useful definitions. Letφ be an A-formula to be checked for satisfiability and let 𝒜𝒫 be the set of its propositional letters. The closureCL(φ) of φ is the set of all subformulae of φ and of their negations (we identify ¬¬ψ with ψ). The set of temporal requests of φ is the set TF(φ) of all temporal formulae in CL(φ), that is, TF(φ)={〈A〉ψ,[A]ψ∈CL(φ)}. By induction on the structure of φ, we can easily prove that for every formula φ, |CL(φ)|≤2·|φ|, while TF(φ)∣≤2·(|φ|-1). A φ-atom is a set A⊆CL(φ) such that: (1) for every ψ∈CL(φ), ψ∈A if and only if ¬ψ∉A; (2) for every ψ1∨ψ2∈CL(φ), ψ1∨ψ2∈A if and only if ψ1∈A or ψ2∈A. We denote the set of all φ-atoms by Aφ; clearly, |Aφ|≤2|φ|. Now, atoms are connected by the natural binary relation; in fact, we can define Rφ as a binary relation over Aφ in such a way that for every pair of atoms A,A′∈Aφ, ARφA′ if and only if for every [A]ψ∈CL(φ), if [A]ψ∈A, then ψ∈A′. At this point, we can define a class of extended models, called fulfilling labeled structures, as follows. First, a φ-labeled structure (LIS, for short) is a pair L=〈𝔻,𝕀(𝔻),ℒ〉, where ℒ:𝕀(𝔻)→Aφ is a labeling function that for every pair of meeting intervals [a,b],[b,c]∈𝕀(𝔻), ℒ([a,b])Rφℒ([b,c]). Second, we say that L is fulfilling if and only if for every temporal formula 〈A〉ψ∈TF(φ) and every interval [a,b]∈𝕀(𝔻), if 〈A〉ψ∈ℒ([a,b]), then there exists c>b such that ψ∈ℒ([b,c]). Clearly, there is a close relationship between models for a formula φ and fulfilling labeled structures for it. Indeed, we can easily prove that φ is satisfiable on a model M and interval [a,b] if and only if there exists a fulfilling labeled structure L, based on the same domain as M, and such that φ∈ℒ([a,b]). Moreover, because of the simple structure of the fragment A, satisfiability of A-formulas over Fin is reducible to initial satisfiability, that is, satisfiability over the interval [0,1]. So, we can now say that φ is finitely satisfiable if and only if there exists a fulfilling labeled structure L such that φ∈ℒ([0,1]).


### 6.3.2. Eliminating Points

Since fulfillingLISs satisfying φ may be arbitrarily large, we must find a way to finitely establish their existence. In the following, we give a bound on the size of finite-fulfilling LISs that must be checked for satisfiability, when searching for finite φ-models. To prove this result, we take advantage of the following two fundamental properties of LISs: (1) the labeling of a pair of intervals [a,b],[c,b] with the same right endpoint b must agree on temporal formulae (since every right neighbor of [a,b] is also a right neighbor of [b,c], we have that for every existential formula 〈A〉ψ∈TF(φ), 〈A〉ψ∈ℒ([a,b]) if and only if 〈A〉ψ∈ℒ([c,b]) and similarly for universal formulas); (2)(|TF(φ)|/2) right-neighboring intervals suffice to fulfill the existential formulas belonging to the labeling of an interval [a,b] (the number of right-neighboring intervals which are needed to fulfill all existential formulae of ℒ([a,b]) is bounded by the number of 〈A〉-formulas in TF(φ), and, at worst, different existential formulae are satisfied by different right-neighboring intervals). By exploiting these properties, we can define, for every point a in a fulfilling labeled structure L the set REQ(a) (of requests) of all and only the temporal formulas belonging to the labeling of the intervals ending at a, and REQ(φ) as the set of all possible sets of requests, so that |REQ(φ)|=2((TF(φ)/2)). We are ready to prove our main result. Indeed, we now prove that, if m=(|TF(φ)|/2) and if L is a finite-fulfilling LIS that satisfies φ, then there exists a finite-fulfilling LIS  L¯ that satisfies φ as well and for every a∈𝔻¯∖{1},  REQ(a) occurs at most m times. To see this, assume L does not respect the given condition, so assume that for some a∈𝔻, different from 1,  REQ(a)=R occurs more than m times. We now define a sequence of LISs  L=L0,L1,…, each one of which is fulfilling and progressively smaller, and such that the last one of the sequence meets the condition on the number of occurrences of R. Our first step consists in turning L0 into L1, in such a way that one of the points that presented the set of requests R has been eliminated. Assume that a1<a2<⋯<an(n>m)  are the points in L with set of requests R; the LIS  L1 is defined over the domain 𝔻1=𝔻0∖{a1}, and in such a way that ℒ1 is the projection on the remaining intervals of ℒ. The structure so-defined L1 is obviously a finite LIS, but it is not necessarily fulfilling. In fact, the removal of a1 causes the removal of all intervals beginning or ending at a1. While the removal of intervals beginning at a1 is not critical (as the requests possibly satisfied by them have been removed as well), there can be some points a<a1 such that some formulas 〈A〉ψ∈REQ(a) are fulfilled in L0, but they are not fulfilled in L1 anymore. We fix such defects (if any) one-by-one by properly redefining ℒ1. Let a<a1 and 〈A〉ψ∈REQ(a) such that ψ∈ℒ0([a,a1]) and that there is no a′∈𝔻∖{a1} such that ψ∈ℒ1([a,a′]). Since REQ(a) contains at most m  〈A〉-formulas, there exists at least one point ai∈{a2,…,an} such that the atom ℒ1([a,ai]) either fulfills no 〈A〉-formulas or it fulfills only 〈A〉-formulae which are also fulfilled by some other atom of the same type. Let ai one of such points. We can redefine ℒ1([a,ai]) by putting ℒ1([a,ai])=ℒ0([a,a1]), thus fixing the problem with 〈A〉ψ∈REQ(a). Notice that, since REQ(a1)=REQ(ai)=R, such a change has no impact on the right-neighboring intervals of [a,ai]. In a similar way, we can fix the other possible defects caused by the removal of a1. We repeat such a process until we are left with exactly m distinct points where R occurs, defining, as we said at the beginning, a sequence of LISs. The last one of such a sequence, L¯, is, clearly, a fulfilling LIS that satisfies φ, and no set of requests occurs more than m times on it.


### 6.3.3. The Result

It is now straightforward to observe that we have reduced the finite satisfiability problem for aA-formula φ to the search of a labeled structure whose dimension is exponential, at most, in the length of φ; a nondeterministic, sound, complete, and terminating searching procedure can be now devised, allowing us to conclude that our problem is, not only decidable, but also in NEXPTIME.


## 6.3.1. Preliminary Definitions

We start with some useful definitions. Letφ be an A-formula to be checked for satisfiability and let 𝒜𝒫 be the set of its propositional letters. The closureCL(φ) of φ is the set of all subformulae of φ and of their negations (we identify ¬¬ψ with ψ). The set of temporal requests of φ is the set TF(φ) of all temporal formulae in CL(φ), that is, TF(φ)={〈A〉ψ,[A]ψ∈CL(φ)}. By induction on the structure of φ, we can easily prove that for every formula φ, |CL(φ)|≤2·|φ|, while TF(φ)∣≤2·(|φ|-1). A φ-atom is a set A⊆CL(φ) such that: (1) for every ψ∈CL(φ), ψ∈A if and only if ¬ψ∉A; (2) for every ψ1∨ψ2∈CL(φ), ψ1∨ψ2∈A if and only if ψ1∈A or ψ2∈A. We denote the set of all φ-atoms by Aφ; clearly, |Aφ|≤2|φ|. Now, atoms are connected by the natural binary relation; in fact, we can define Rφ as a binary relation over Aφ in such a way that for every pair of atoms A,A′∈Aφ, ARφA′ if and only if for every [A]ψ∈CL(φ), if [A]ψ∈A, then ψ∈A′. At this point, we can define a class of extended models, called fulfilling labeled structures, as follows. First, a φ-labeled structure (LIS, for short) is a pair L=〈𝔻,𝕀(𝔻),ℒ〉, where ℒ:𝕀(𝔻)→Aφ is a labeling function that for every pair of meeting intervals [a,b],[b,c]∈𝕀(𝔻), ℒ([a,b])Rφℒ([b,c]). Second, we say that L is fulfilling if and only if for every temporal formula 〈A〉ψ∈TF(φ) and every interval [a,b]∈𝕀(𝔻), if 〈A〉ψ∈ℒ([a,b]), then there exists c>b such that ψ∈ℒ([b,c]). Clearly, there is a close relationship between models for a formula φ and fulfilling labeled structures for it. Indeed, we can easily prove that φ is satisfiable on a model M and interval [a,b] if and only if there exists a fulfilling labeled structure L, based on the same domain as M, and such that φ∈ℒ([a,b]). Moreover, because of the simple structure of the fragment A, satisfiability of A-formulas over Fin is reducible to initial satisfiability, that is, satisfiability over the interval [0,1]. So, we can now say that φ is finitely satisfiable if and only if there exists a fulfilling labeled structure L such that φ∈ℒ([0,1]).


## 6.3.2. Eliminating Points

Since fulfillingLISs satisfying φ may be arbitrarily large, we must find a way to finitely establish their existence. In the following, we give a bound on the size of finite-fulfilling LISs that must be checked for satisfiability, when searching for finite φ-models. To prove this result, we take advantage of the following two fundamental properties of LISs: (1) the labeling of a pair of intervals [a,b],[c,b] with the same right endpoint b must agree on temporal formulae (since every right neighbor of [a,b] is also a right neighbor of [b,c], we have that for every existential formula 〈A〉ψ∈TF(φ), 〈A〉ψ∈ℒ([a,b]) if and only if 〈A〉ψ∈ℒ([c,b]) and similarly for universal formulas); (2)(|TF(φ)|/2) right-neighboring intervals suffice to fulfill the existential formulas belonging to the labeling of an interval [a,b] (the number of right-neighboring intervals which are needed to fulfill all existential formulae of ℒ([a,b]) is bounded by the number of 〈A〉-formulas in TF(φ), and, at worst, different existential formulae are satisfied by different right-neighboring intervals). By exploiting these properties, we can define, for every point a in a fulfilling labeled structure L the set REQ(a) (of requests) of all and only the temporal formulas belonging to the labeling of the intervals ending at a, and REQ(φ) as the set of all possible sets of requests, so that |REQ(φ)|=2((TF(φ)/2)). We are ready to prove our main result. Indeed, we now prove that, if m=(|TF(φ)|/2) and if L is a finite-fulfilling LIS that satisfies φ, then there exists a finite-fulfilling LIS  L¯ that satisfies φ as well and for every a∈𝔻¯∖{1},  REQ(a) occurs at most m times. To see this, assume L does not respect the given condition, so assume that for some a∈𝔻, different from 1,  REQ(a)=R occurs more than m times. We now define a sequence of LISs  L=L0,L1,…, each one of which is fulfilling and progressively smaller, and such that the last one of the sequence meets the condition on the number of occurrences of R. Our first step consists in turning L0 into L1, in such a way that one of the points that presented the set of requests R has been eliminated. Assume that a1<a2<⋯<an(n>m)  are the points in L with set of requests R; the LIS  L1 is defined over the domain 𝔻1=𝔻0∖{a1}, and in such a way that ℒ1 is the projection on the remaining intervals of ℒ. The structure so-defined L1 is obviously a finite LIS, but it is not necessarily fulfilling. In fact, the removal of a1 causes the removal of all intervals beginning or ending at a1. While the removal of intervals beginning at a1 is not critical (as the requests possibly satisfied by them have been removed as well), there can be some points a<a1 such that some formulas 〈A〉ψ∈REQ(a) are fulfilled in L0, but they are not fulfilled in L1 anymore. We fix such defects (if any) one-by-one by properly redefining ℒ1. Let a<a1 and 〈A〉ψ∈REQ(a) such that ψ∈ℒ0([a,a1]) and that there is no a′∈𝔻∖{a1} such that ψ∈ℒ1([a,a′]). Since REQ(a) contains at most m  〈A〉-formulas, there exists at least one point ai∈{a2,…,an} such that the atom ℒ1([a,ai]) either fulfills no 〈A〉-formulas or it fulfills only 〈A〉-formulae which are also fulfilled by some other atom of the same type. Let ai one of such points. We can redefine ℒ1([a,ai]) by putting ℒ1([a,ai])=ℒ0([a,a1]), thus fixing the problem with 〈A〉ψ∈REQ(a). Notice that, since REQ(a1)=REQ(ai)=R, such a change has no impact on the right-neighboring intervals of [a,ai]. In a similar way, we can fix the other possible defects caused by the removal of a1. We repeat such a process until we are left with exactly m distinct points where R occurs, defining, as we said at the beginning, a sequence of LISs. The last one of such a sequence, L¯, is, clearly, a fulfilling LIS that satisfies φ, and no set of requests occurs more than m times on it.


## 6.3.3. The Result

It is now straightforward to observe that we have reduced the finite satisfiability problem for aA-formula φ to the search of a labeled structure whose dimension is exponential, at most, in the length of φ; a nondeterministic, sound, complete, and terminating searching procedure can be now devised, allowing us to conclude that our problem is, not only decidable, but also in NEXPTIME.



---

*Source: 616087-2012-10-14.xml*