The Completeness of a Natural System for Reasoning with Time Intervals

1 Introduction The Interval Calculus

The representation of time by means of intervals rather than points has a history in philosophical studies of time (e.g. [Ham71 , vBenB!J, Hu.m78, Dow79, Rop79, New80]). James Allen defined a calculus of time intervals in {All8!Jj, by considering binary relations on pairs of real numbers definable using only the natural ordering on the real num­ bers. He investigated the use of the calculus for repre­ senting time in the context of planning {All84, AllKau.85, PelAll86]. Allen and Pat Hayes have investigated the first­ order logical formulation of interval theories in {AllHay85, AllHay87.1, AllHay87.2]. A modal logic using similar in­ terval concepts was introduced in [HalSho86].

Ladkin and Maddux {LadMad87.1] showed that Allen had defined the primitives of a proper relation algebra in the sense of Tarski {JonTar52], and showed that there is, up to isomorphism, a unique countable representation of this algebra. This representation is derived from the set of pairs of rational numbers, in the same way that Allen used the pairs of real numbers to define his calculus. We also showed that there is a canonical translation of an arbitrary finite relation algebra into a first-order theory, so a first­ order axiomatisation of the Interval Calculus is obtained. This theory is complete, countably categorical (i.e. has a unique countable model up to isomorphism), and decid­ able (by Vaught's Test) [LadMad87.1, ChaKei7!J].

·This work has been partially supported by U.S. Navy under con­ tract N00039-86-C-0221 , and by Rome Air Development Center under U.S. Government contract F30602-84-C-0109. The views and conclu­ sions expressed in this paper are those of the au thor and should not be interpreted as representing the official policies, either expressed or implied, of Kestrel Institute, the U.S. Navy, or RADC.

The Completeness of a Nat ural System for Reasoning with Time Intervals*

Peter Ladkin Kestrel Institute 1801 Page Mill Road Palo Alto, Ca 94304-1216

Recently, we showed in [Lad87.4] that this theory ad­ mits elimination of quantifiers (any statement in the the­ ory is equivalent to a quantifier-free statement in the same theory), and gave an explicit decision procedure for the theory.

We use the expression Interval Calcu.lu.J to refer to either the algebraic or the first-order formulation, and we use the expression Interval Algebra to refer specifically to just the relation-algebraic formulation of the calculus.

The first-order Interval Calculus theory is stronger than the first-order axiomatisation of intervals in {AllHay85, AllHay87.1, AllHay87.2]. The Interval Calculus entails the density of the underlying ordering {LadMad87.1]. We characterised precisely all the models of the Allen-Hayes theory in [Lad87. !J], as pairs of distinct, ordered points over an arbitrary, not necessarily dense, unbounded lin­ ear order. We showed in {Lad87.4] that the Allen-Hayes theory is decidable, but at the time of writing we do not yet have a really practical decision procedure for it, in contrast to the situation for the Interval Calculus (for ex­ ample, the Allen-Hayes theory does not admit quantifier elimination).

Allen was particularly concerned with constraint sat­ isfaction techniques in the Interval Calculus, and he pre­ sented an algorithm for detecting a limited class of incon­ sistencies in {All89]. Vilain and Kautz have shown that constraint satisfaction in the Calculus is NP-hard in gen­ eral {VilKau.86]. Ladkin and Maddux extended Allen's constraint propagation algorithm so that it detects in­ consistencies missed by his algorithm [LadMad87.2]. The decision procedure of {Lad87.4] combines quantifier elimi­ nation techniques with Allen's algorithm, as extended by Ladkin-Maddux, to decide arbitrary first-order formulas.

Background to This Paper

In our work, we have considered the use of the Interval Calculus for reasoning about all aspects of time. Two of our major concerns are, firstly, that using intervals with­ out gaps (convex intervals) makes it hard to reason about interruptable processes, where the more natural model would use intervals with gaps; and, secondly, that it is of­ ten unnatural to use pairs of real numbers for representing intervals of real time, especially when standard everyday time units are needed, as in project management or real­ time programming.

The first concern led-us to a taxonomy of binary rela­ tions on intervals that had gaps, called unions-of-convex intervals {Lad86.1}. We refer to this system as the Ex­ tended Interval Calculw. We provided an example of the use of the Extended Interval Calculus for the high­ level specification and synthesis of concurrent processes in {Lad87.1}. The second concern led to a system of inter­ val time units {Lad86.£j, which can represent all kinds of standard time intervals such as years, days, and picosec­ onds in a natural manner, and we introduced primitive operations for building up arbitrary intervals, both con­ vex and non-convex, from these interval time units. We refer to this time unit system as the TUS. Another system for constructing time units was presented in {LeMcFo86j.

We show here that the TUS contains a canonical model for the Interval Calculus. Specifically, the definable part of the TUS which refers to convex intervals (the convex TUS) is a countable representation of the Interval Alge­ bra. Since there is, up to isomorphism, only one count­ able representation of the Interval Algebra (or, countable model of the Interval Calculus), the convex TUS is canon­ ical in the following sense: if a statement in the Interval Calculus is not a theorem of the Calculus, then there is a counterexample to that statement in the convex TUS, and if a statement in the language of the Interval Calculus is true for all the intervals in the convex TUS, then it is a theorem of the Interval Calculus. These facts follow from theorems in {LadM ad87.1 ].

The representation of time intervals in the TUS is richly structured, compared with a pairs-of-points repre­ sentation. For example, there is a natural notion of dura­ tion that may be imposed {Lad86.£j, which is essential for real-time reasoning.

We present in this paper a one-to-one mapping from time units to pairs of rational numbers, to show canon­ icality of the convex TUS. The decision procedure in {Lad87.11j can make use of the map to provide a model within the TUS of an arbitrary satisfiable collection of first-order constraints in the Interval Calculus. We refer the reader to {Lad87.4] and sequels.

The TUS and the Interval Calculus have been imple­ mented at Kestrel Institute, as part of the ongoing task of implementing and using the Extended Interval Calculus. The full decision procedure for the Interval Calculus has not yet been implemented. Currently, the TUS is used as the base for the time package in a prototype project management system developed at Kestrel Institute.

Organisation

Section 2 introduces the time unit system from {Lad86.£j, and defines the language used for the statement of the main result. Section 3 contains the main result, and Sec­ tion 4 is a summary.

2 The Time Unit System

The TUS was introduced in {Lad86. 2] by example. There are ba3ic time units, which are sequences of integers of a certain sort, and a binary operator convexify, which en­ ables us to build arbitrary convex intervals from the basic units. The full TUS includes other structure needed for the Extended Interval Calculus {Lad86.2j, which need not concern us here. We are concerned only with that part of the TUS which deals with convex intervals. We introduce this by example, and later give a more formal definition via the language I and the associated theory :r . .J is the convex part of the TUS defined by the axioms given in {Lad86.£j, or, alternatively, may be obtained from I by using the algebraic methods in this paper.

The Convex Part of the TUS

We represent the ba.,ic time intervals in the TUS by se­ quences of integers. Each element of the sequence repre­ sents a particular year, month, day, hour, minute, 3econd .... , The first element represents the year, the next is the month in that year, the third is the day, etc. We illustrate the system down to seconds, hence our sequences will have lengths of up to six elements. The system is clearly ex­ tendable to smaller units such as microseconds and pi­ coseconds, indeed needs to be extendable to arbitrarily small units of time in order to prove our main theorem. It was indicated in {Lad86.2j that the system is adequate for defining other kinds of intervals that are not basic inter­ ~als such as WEEKS and CENTURIES, providing there IS some logic programming ability in the implementation language.

Some example real-time intervals in this system are:

• [1986] representing the year 1986
• [1986,3) representing the month of March, 1986
• [1986,3,21] representing the day of 21st March, 1986
• [1986,3,21, 7] representing the hour starting at 7am on 21st March, 1986
• [1986,3,21,7,30) representing the minute starting at 7:30am on 21st March, 1986 ·
• [1986,3,21, 1 ,30,32] representing the 33rd second of 7:30am on 21st March, 1986 (the first second starts at 0)

In addition to the basic sequences that represent fixed units of clock time, we need to be able to make arbi­ trary convex time intervals. The operator convexify ac­ complishes this.

convexify(i,j) = the 3mallest convex interval that contains both i and j

• convexify([1987),[1999]) =the interval containing all of the years from 1987 to the end of the century
• convexify([1987,1), [1987,12]) = the interval from January 1987 through December 1987, i.e. the year 1987.

Thus convexify([1987,1), [1987,12)) = [1987).

• convexify([1987,3,2,8), [1987,3,2,11]) = the (Amer­ ican) working morning of Monday March 2 1986, from Sam until noon (the hour of llam extends up until noon).

Axioms for convexify were given in {Lad86.£}. For the purposes of this paper, the intuitive definition and illus­ trations given above should suffice.

3 The Main Result

In this section, we introduce the languages I and I 1 , and the associated theory .J, of the TUS. We thus present the TUS as a formal theory, but of course this theory is about time intervals. We choose this method of presenta­ tion because we wish to later map the TUS intervals into pairs-of-rational-numbers, for the main theorem. It is eas­ iest to do this by presenting the theory as a language of terms, with an axiomatised equality on those terms (which we indicate first intuitively, and later give a more formal presentation), and then defining the mapping to the set of pairs-of-rational-numbers, by means of the language, in a way which preserves the equality on those terms. This is a standard technique from Universal Algebra, see e.g. {BurSan81}.

We in fact obtain our results for a more general family of languages, 9". The result for .J is an instance of the general result .

The Language I

We need to distinguish between actual convex time inter­ vals, and term" in the language for denoting time intervals. This is because, as we saw, we can have two different terms denoting the same time interval, e.g. convexify([1987,1), [1987,12]) and [1987).

To be more precise, our language I for time units has constants for some finite sequences of integers, (which we denote by e.g. [a,b,c] for the 3-element sequence whose first element is the integer a, whose second is the integer b, and whose third is the integer c); contains the binary operator symbol conv (to stand for the convexify opera­ tor); and contains a standard set of punctuation symbols for constructing terms from these constants and the oper­ ator (which we write prefix). The term" of this language are obtained in the standard manner from the sequence constants and conv.

The precise collection of finite sequences that we want to denote are just those that denote actual parts of years, months, days, etc. The technical definition is straightfor­ ward, but detailed:

• the first item is an arbitrary (positive or negative) integer, i.e. a member of Z, the set of integers.
• the second item is an integer between 1 and 12, in­ clusive,
• the third item depends on the first and second items, and is always an integer between 1 and 31 (we have to allow for 28, 29 and 30 day months).
• similarly for the hour elements, minute elements,

We shall use the convention that when we want to refer to a term, we write it in boldface, and when we use a term to refer to an interval, we write it in lightface. For those familiar with the use/mention distinction, this means that we we in lightface, and mention in boldface.

So convezify({1987,1}, {1987,1£/) is the same interval as {1987}, but conv((1987,1], (1987,12]) is not the same term as (19S7] . .J contains the statement (conv([1987,1], (1987,12]) = (1987]} as a theorem, since the intervals denoted by these two terms are the same in­ terval.

.J is just the theory in the language I which is ob­ tained by considering which terms in I refer to the same interval. In other words, .J is the theory of the equality relation obtained from considering the equations true of the operator convexify. This theory .J was axiomatised in {Lad86.£}, p358.

The sublanguage of I which we are most interested in is the language I 1 which consists of all the sequence constants from I along with those terms of the form conv(i, j}, where i and j are sequence constants (i.e. there are no iterated applications of conv in tenns in I 1 ).

The importance of the sublanguage I 1 is that every convex interval in the TUS may be represented by a term in I 1 · In other words, iterated applications of the convex­ ify operator may be replaced by a single application of convezify to ba.sic intervals. This fact is stated precisely in the following lemma:

Lemma 1 For every term t E I, there u a term t1 E I 1 , .such that .J contain.s the .statement t = t 1 a.s a theorem.

The Sets QP of Sequences

We define the set of sequences 9", where /J is an infinite collection of functions ft. /2, ..... and f,. is of arity k, for each k. (For simplicity, we identify the arguments to fl, with a single sequence of length k, so we shall write f~e(o) where 01 is a sequence of length k)

We define g~, the set of sequences of length k in {i", by induction.

• 9t is the empty set. (i.e. 9~' does not contain the empty sequence).
• 9f = {[n] : n E Z} (i.e. the sequences of length one have integer ele­ ments) .
• 9t+t ={a---. ['y] : a E 9t & 'Y E Z,} where ---. is concatenation of sequences, p = /J,( a), and z, is the ring of integer~ mod p, i.e. the set {0, 1, .... , (p- 1)}.
• 9~' = U"9t (i.e. the union of all the 9t).

Intuitively, 9~' is a collection of sequences of the form (at, a2, .. ... ,an], where at is an integer, (at, a2, ..... , an-t] is also a sequence in 9'', and an can be any integer from 0 to (p- 1), where the value of p depends on the values at, a2, .... . ,an-t ·

Example: Jl is a collection of constant functions, say fk(a) = Pk for each k. Then (}~' is the collection of se­ quences of the form (at, a2, .. ... ,an], where at is an integer, and a~e is an integer mod Pk, i.e. 0 :s; ak < Pk, for each 1 < k :s; n .

Example: Jl is the collection of functions defining the calendar used for the time unit system, i.e. It is the con­ stant function 12 (there are 12 months in any year) ;

!l((a, 1]) = 31, f 2((a, 2]) = 28 if either a is not divisible by 4, or a E {100, 200, 300}, f 2((a, 2]) = 29 in these other cases, f 2((a, 3]) = 31, h((a, 4]) = 30, ... etc;

/3 is the constant function 24 (there are 24 hours in any day) ; .. . etc.

9~' in this example is almost the collection of basic se­ quences in the language I . The difference is that the se­ quence elements in I, after the first, start at 1 and go up to some value, (say 1 to 31 for the days in the first month) whereas those in 9~' start at 0 (and would go from 0 to 30 in the case of the first month). The two can be mapped onto each other simply by performing the translation

We assume that this translation is always implicitly per­ formed, and refer to the basic units in I as being an ex­ ample of a 9"'.

The Mapping of Q~-' into Pairs of Rational Numbers

In order to obtain the main result, we map 9"' into the set of pairs of rational numbers

Q x Q = {(a,b) : a< b & a, b E Q} (Q is the set of rational numbers) in a canonical way.

We define the mapping rp. : 9"'-+ (Q X Q) by induction on the length of the sequence (at, a2, .. ... ,an] as follows:

• (n]~-+ (n,n + 1) i.e. single-element sequences are mapped to pairs of consecutive integers
• Suppose (at,a2, ..... ,an]~-+ (a, b). Let p = fn([at, a2, ..... ,an]) . Let h = (b- a)+ p. Then (at, a2, .... . , an~ 0]~--+ (a, a+ h) , (at, a2, ..... ,an, 1]~--+ (a+ h, a+ 26), (at, a2, .. .. . ,an, (p- 1)]~--+ (a+ (p- 1) X h, b) . I.e. we divide the interval (a, b) into p equal parts, and then map the sequences extending [at, a 2 , ..... , an] by one element, into the equal parts, consecut ively.

By results in {LadMad81.1}, Q x Q is a representation of the Interval Algebra, and hence a model of the Interval Calculus. 9"' can inherit the interval relations from Q x Q in the following way:

Let R be one of the interval relations, which we write infix. Then we can define the relation R on sequences in 9"' from its values on elements of Q x Q by means of the equivalence

We call this the ~tru.ctu.re inherited from Q X Q via r~-~ This does not yet turn 9~' into a representation of the Interval Algebra, since, by results in [LadMad81.1}, it is necessary that for each relation R of the Interval Calculus, and each object a in the representation, there must exist an object b such that aRb. And, it is easy to observe that there is no sequence ,8 E 9"' such that , under the structure inherited from Q x Q via f"', ([n] starts ,8), or ((n] ends ,8), or ((n] during ,8), for any sequence (n]. Hence we need to extend the system 9"' to provide such ,8 for the sequences of length 1.

The Extension of Q~'

Let I:~' be the set of all terms of the form conv(i, j) where i, j E 9"' . These terms are intended to represent the con­ vexify operator on intervals represented as sequences. We saw that many terms can represent the · same convex in­ terval, so we need a way of picking just one term that names a given convex interval. First, we define the map­ ping W"', which associates a pair of rational numbers with each term in I:"':

Then

We now use a standard technique from Universal Al­ gebra (see e.g. [Bu.rSan81}) in order to get the domain, and the mapping, that we want .

We consider the equivalence relation :::; defined on terms t1 and t 2 in E~' as follows:

We denote the collection of equivalence classes by (E~' / :::;). We define

6~' is known as the kernel of the mapping Ill~' .

We can now factor the map Ill~' through the equivalence relation :::;, in the standard way, so it becomes a map 9~': 6~' 1-+ Q x Q by defining, for each 1 E 6~':

Note that 9"(1) is well-defined, since for a given/, for all t E / , ll!~'(t) has the same value, by definition of the equivalence :::;.

We can now extend r~' to a mapping (}~' U 6~' -+ Q x Q by setting P('Y) = 9"(1) if 1 E 6~'. (}~' U 6~' inherits the relation structure from Q x Q by the same technique we used for(}~'.

The technique of factoring a mapping through its ker­ nel, while mathematically appropriate, doesn't necessarily give a good idea of what the kernel looks like, i.e. precisely when it is that two terms name the same convex interval. We have already addressed this issue for the case of .:J, by referring to the axiomatisation in {Lad86.£}. The axioms in fact axiomatise the inherited structure as we present it here, and can be regarded as a first-order presentation of the same structure that we are here presenting alge­ braically.

Another way of accomplishing the same factorisation is just to pick a canonical representative of each equivalence class, and let 6~' instead be just the collection of canonical members. We now extend r~' by setting r"('Y) = 111"(1) if 1 E 6~', to obtain the same effect as we did with the equivalence classes. There are many ways of picking a canonical representative of each equivalence class, and in fact this is the technique we used in the implementation of the time unit system at Kestrel.

We can now state the Main Theorem:

Theorem 1 (}~' U 6~' i.s a countable repre.sentation of the Interval Algebra under the .structure inherited from Q X Q via r~' .

Sketch of Proof: By results in {LadMad87.1, JonTar5£, Mad78}, it is sufficient to show

• the two sets

are both countable, dense, linear orderings under the standard order, and are thus each isomorphic to the whole of Q;

• for each relation R of the Interval Calculus, and each a E (}~'U6~', there exists {j E (}~'U6~' such that aRb, under the structure inherited from Q x Q via P.

It is tedi~us but straightforward to verify these properties. End of Proof Sketch.

From now on, we shall use the notation (}~' U 6~' am­ biguously for both the set, and the representation of the Interval Calculus obtained by inheriting the structure from Q x Q via r~'. There should be no confusion engendered by this systematic ambiguity.

Corollary 1 (}~'U6~' i.s i.somorphic to the pair.s-of-rational.s repre.sentation of the Interval Calculu.s

Proof: By results of {LadMad87.1}, all countable repre­ sentations of the Interval Algebra are isomorphic. End of Proof.

Corollary 2 .:J i.s i.somorphic to the pair.s-of-rational.s rep­ re.sentation of the Interval Calculu.s

Proof: We use a systematic abuse of language in the statement of the Corollary. .:J is technically a theory, but may be considered as a structure by taking the equiva­ lence classes of terms under the equality relation axioma­ tised by .:J, and the inherited structure from the mapping into Q x Q. We have noted in an earlier example that I 1 is an instance of {;~' u 6~'' providing that the implicit translation is made for the sequence elements of I 1 · Hence the corollary follows. End of Proof.

4 Summary

We have described the convex part of a time unit system, TUS, which implements the Interval Calculus introduced by James Allen {All83}. We have presented a theorem which has as a consequence that the convex part of the TUS is a canonical model for the Interval Calculus, in the sense that if a statement in the Interval Calculus is not a theorem, then there is a counterexample to that statement in the TUS, and any statement true of all of the intervals in the convex part of the TUS is a theorem of the Interval Calculus. This theorem relies heavily on results of {LadMad87.1}. We noted that we can obtain models in the TUS of arbitrary satisfiable first-order constraints in the Interval Calculus, via the decision procedure of {Lad87.4}, and the mappings constructed in this paper.