The Logic of Time Structures: Temporal and Nonmonotonic Features

1. Introduction

One approach to the representation of time related knowledge is to embed the time factor in the operational or model-theoretic semantics of the representation. This is the approach in the situation calculus ( [McCarthy & Hayes 1969], [Hayes 1971] ), in truth maintenance systems, in computation models, in tense logics ( [Halpern & Shoham 1986] ), and in some com­ puter music systems ( [Schottstaedt 1983], [Cointe & Rodet 1983] ).

Another approach is to make time explicit in the language. Examples are the reified temporal logics of [Allen 1984], [McDermott 1982], [Dean & McDermott 1987] , and [Shoham 1987a]; also the Horn-clause logic of [Kowalski & Sergot 1986] and the first order logic of [Haugh 1987].

We imbed into a first order logic a representation language that combines atemporal knowledge with time stamps in a hierarchical fashion . The syntactic unit of the representation language is called a time structure; it resides in our logic as a term. A consequence of this is that the implementation of our formalism with logic pro­ gramming techniques will be relatively straightforward.

Each time structure describes a chronology of events . The time stamps result in an encoding of tem­ poral logic that is similar to that of [Shoham 1987a]. Furthermore, each time structure can play the role of a 'world' in a modal logic, resulting in an unusual encoding of modal logic; unusual because a world is referenced by its explicit representation as a term, rather than by a con­ stant through which certain facts are indexed. Since our 'worlds' are terms, they can be ordered, and we can Neil V. Murray Dept. of Computer Science State Univ. of N.Y. at Albany Albany, NY 12222

t This research was supported in part under grant CCR8600848 awarded by the National Science Foundation.

enforce a preference criterion on that ordering. In this way, we can achieve the effect of nonmonotonic reason­ ing.

In Section 2 we give our view of temporal domains; The operators (i.e., interpreted symbols) of our logic are introduced in Section 3. Section 4 is a discussion of semantics; in particular, the semantics of the interpreted non-logical symbols. In Section 5 we compare the logic of time structures with Shoham's classical interval temporal logic, and its nonmonotonic version. [Shoham 1987b ]. We conclude with an example of reasoning with chrono­ logical minimization. Proofs of lemmas and theorems are omitted and can be found in [Balaban & Murray 1988].

2. Domain of Discourse

The temporal world that we describe has no abso­ lute time line. It is built from atemporal objects that, when combined with time points, form histories. His­ tories can be combined together to form more complex histories. Each history has its own private time line. The entire domain of discourse consists of atemporal objects, temporal objects (time points), and histories. We now describe each of these types in some detail.

2.1. Atemporal and temporal objects

Atemporal objects are domain elements that, viewed in isolation, are durationless. Of course, in reality 'durationless objects' do not exist, but this is a common abstraction.

We assume a set of temporal objects called time points, that is totally ordered and that contains an object called Zero.

We distinguish objects, actions, and processes not by means of distinct types, but through the temporal behavior of such entities represented as histories.

2.2. Histories

The building block for histories, called an elemen­ tary combination, is the association (p, td) of an atem­ poral object p with a temporal object td. The pair (p, td) can be thought of as the set of all occurrences of p such that if p starts at some time point t, it clips at time point t + td. We call td the duration of the elementary combina­ tion (p, td) ·

A history is a collection of time-stamped histories, or time stamped elementary combinations. A history has its own time line and the histories that occur within it have their own time lines. But the Zero of these time lines is displaced from the Zero of the composite history by their corresponding time stamps. Elementary combi­ nations have no self time lines.

2.3. Formal Definition

Here, a brief formal description of our domain of discourse is given. We have a non-empty domain D of atemporal objects, and a domain T of time points that is totally ordered and that contains Zero. Time points and objects can be combined to form the set H of histories as follows:

• (a) The empty set (/) is a history called the empty his­ tory.
• (b) For i E r, an arbitrary indices set, hiEH U EC, and tiET: h ={(hi. tJ I iEr} E H;

h is the history in which the time line of sub-history hi is displaced by ti.

The entire domain of discourse U consists of (D U T U EC U H) . We assume a set F of total functions Uk- U. No a priori restrictions are placed on these functions, except that they are total and have a signature indicating the sub-domains corresponding to their argu­ ments and to their range. In other words, the functions of F must be well-typed with respect to D, T, EC, and H.

The need for 'inter-typed' functions arises from the non-homogeneous nature of U. Elementary combinations are obtained by a function whose signature is: D X T - EC; histories require the signature { (Hi U ECi) X Di)}iEr - H. A duration function would have the signature H - T; atemporal functions like "angry" would be of type D - D.

3. Time Structures

In correspondence to the four types in U, there are four kinds of terms: primitive terms that denote atemporal objects, time terms that denote time points, elementary pairs that denote elementary combinations, and time structures that denote histories. All are terms of first order logic.

Given:

C = a set of constant symbols.

S = {d,t,ec,h}- sort symbols, that correspond to the three types D, T, EC, H.

0 E C - denoting the Zero object ofT.

NIL E C - denoting the empty history (/) in H.

v = a set of variables.

FS = a set of function symbols.

[ 1 E FS - describing elementary histories.

· E FS - describing histories. · is called the tem­ poral concatenation operator.

Terms: Defined as usual, with sort restrictions taken into account as follows:

The sort of constants and variables is their signa­ ture; the sort of f(tt. ... ,t0 ) is the last element of the signatm:e of f, where the ith element of sig(f) must agree with the sort of tio l~i~n .

We discuss the terms of sorts d, t, ec, and h below. We express functions of arity one or greater as lower case identifiers; variables are also lower case but are italicized; constants are functions of zero arity and may be upper or lower case; the time structure operators appear in bold­ face.

3.1. Primitive Terms and Time Terms

Primitive terms are terms of sort d. They denote atemporal objects. Time terms are terms with sort t. One distinguished time term is the constant 0; it denotes the time point Zero.

3.2. Elementary Pairs

An elementary pair is a sort ec term of the form [p, td]; it associates a non-negative time term ~ with a primi­ tive term p. It denotes the elementary combination (p', td'), where p', ~· are the denotations of p, td, respec­ tively. For example, the elementary pair [FIDO­ BARKS,35] can denote the elementary combination of fido barking, that clips at time point t + 35, if it starts at time point t.

3.3. Time Structures

Time structures are terms of sort h that denote his­ tories; they include (not exclusively) NIL and all terms generated by · . Some examples are:

NIL denotes the empty history.

·([p,d],t,NIL) denotes the history {((p',d'),t')}, where p', d', and t' are the denotations of p, d, and t, respec­ tively.

·([p, d1], t, ·([q, d2],0,NIL)) denotes the history {((p', dt'), t'), ((q', d2'), 0)}

·(·( [p,d], t1, NIL), t2, NIL) denotes a single element history: { ({ ((p', d'), t1'), }, t2')}

·([p,d], t,ts) denotes: {((p',d'), t')}Uh, where his any history (possibly unbounded or infinite).

·( ts, 2*t, ·( ts, t, NIL) ) denotes histories of the form: { (h, 2·t'), (h, t') }, i.e. a pattern of histories. ·

The following axioms characterize the basic proper­ ties of the · operator.

.:..A 7 x:.;.io..:..m=-+lf: The denotation of every sort ec term is that of some term:

Axiom (·h): The denotation of every non NIL sort h term is that of some · term:

Note that this · term is unique up to repetitions and commutativity.

Idem potence:

We define the intended meaning of NIL, [ ], and · terms in Section 4. The intended meaning of all other h terms is defined in terms of these via equality axioms.

3.4. Operators

By an "operator", we mean a symbol that has a well-defined signature and whose definition is fiXed. An operator plays the same role as any function symbol except that it is interpreted. We have already introduced · and [ ]; beyond those, we discuss only the time opera­ tors here; many others are introduced in [Balaban & Murray 1988).

The self-clip time of a time structure ts is written clipu1t(ts); intuitively it is the latest point on the time line of ts at which one of its constituents clips. The self-start time of ts, written start.w1(ts) is similarly defined; the duration, written duratlon(ts), is their difference.

The operators clip(tst.ts2) and start(tst.ts2), com­ pute the more useful relative clip and start times for a time structure or an elementary pair tst that occurs within ts2· Note that each occurrence of tst in ts2 has a relative start and clip time. Therefore, these operators yield a list of time points.

The Interval operator computes a list of pairs of time points that describe intervals during which a given time structure is "playing" within another time structure. Interval is definable from start and clip (see [Balaban & Murray 1988]).

4. Semantics of Time Structures

We assume a standard . first order logic syntax including the usual logical symbols: v, 3 , 1\, V, -., ->, and -· Predicates begin with an upper case character, and we use the notation from Section 2 otherwise.

An equality and total ordering predicate are charac­ terized by appropriate axioms. We avoid introducing a sort symbol b, and a type B" of boolean values; the signa­ ture of a predicate is taken as just the tuple of its argu­ ment sorts, and the sort is understood as boolean. We extend our syntax as follows:

P is a set of predicates that includes ~ and =.

n We extend sgn as follows: sgn: p<nl - .X S, where 1=t sgn(~) = (t,t), and sgn(=) is (d,d), (t,t), (ec,ec), or (h,h) . (we use"=" in the obvious polymorphic way.)

Our principle axiomatic temporal relation is the completion of a time structure over a given interval within a context time structure. The notion of completion is similar to the TRUE notation of [Shoham 1987a]. It is, later on, used to define additional temporal relations, and to classify temporal behaviors of time structures. The notion of completion is expressed by a predicate "C", where C(tt. t2, tst. ts2) means tst occurs as a sub-time structure or sub-elementary pair within ts2, and it starts and clips at tt and t2 , respectively. The signature of C is (t,t,h,h).

The C predicate reflects the time structure operator Interval and is defined as follows :

where "c" denotes a term level connective: &, v, ~. , and CL denotes the corresponding logic level connective (in the case of-, there is no Pt. and CL is unary) . Axiom (C2) defines the term level connectives to be merely abbreviations for non-atomic formulas involving the C predicate. But we might add the condition c=F- to the premise of (C2); then inconsistent information could be represented within a time structure and yet allow the logi­ cal system to remain consistent. Note that keeping the implication uni-directional, the strong law of the excluded middle does not apply to completion of primitive terms: It is not the case that for every primitive term and every interval, either the primitive term or its negation com­ pletes over a time structure (otherwise, NIL, for example, cannot be a legitimate time structure).

As a 1-st order theory, our logic admits the regular 1-st order semantics, within the type restrictions. We now define the notions of intended (standard) interpreta­ tion, and model.

An intended interpretation is a domain and denotation function (U,T), where

• U = D U T U EC U H, and D, T, EC, H are mutu­ ally disjoint .
• D = is the Herbrand Universe defined ~y all constant symbols having a signature in .X S X { d}, 1-t for all n > 0.

T a non-empty set of time points.

Zero E T

EC a set of elementary combinations over D and T (section 2.4).

H a set of histories over EC and T (section 2.4).

T a denotation function as follows :

Maps constants of signature t to elements of T.

Maps constants whose signature is d to themselves.

Maps 0 to Zero.

Maps ~ to Time-order.

Maps= to the equality relation on U.

Maps NIL to (/) (the empty history) .

Maps [ ] to a function: D X T - EC that maps d E D and t E T to the pair (d,t).

Maps · to a function: (H U EC) X T X H - H, defined by:

The time structure operators like start, clip, interval, etc., are assigned their history counter-parts.

A variable assignment is partitioned as follows:

A simple-variable assignment is an assignment to the variables of signature d, t and ec.

An h-variable assignment is an assignment to the variables of signature h.

An interpretation I and a h-variable assignment V form a model to a theory in the logic of time structures, if they satisfy:

1. Axioms (·NIL) (·cmt), (·h) and (·idp); the equality axioms for =, the total ordering axioms for ~. and axioms defining the time structure operators.
2. Axioms for the arithmetic time functions, and the list functions; see [Balaban & Murray 1988]).
3. Axioms (C1), (C2).
4. The proper formulas of the theory for every simple­ variable assignment.

The notions of satisfiability, validity, logical consequence are defined as usual.

4.1. Characterization of Temporal Behaviors

Taking C as our main predicate reflects the interval based nature of our calculus. However, we believe that there is a need also for point-wise characterization of temporal behavior. For that purpose we introduce a predicate, called P (PLAYS), where P(t, tsl> ts2) stands for "the time structure ts1 plays at time point t in time structure ts2."

Note that the subject of the point-wise truth is a time structure tsh and a context time structure ts2. This reflects the view underlying our formalism, that a "fact" (i.e., some a temporal object) cannot "hold" or be "true", unless it is part of some time structure. Hence, it is, always, a time structure about which we wish to state some point-wise truth .

The C and P predicates have the following properties:

1. A time structure is playing at every time along an interval on which it completes:

1. A time structure does not complete on any proper subinterval of an interval on which it completes:

Note that by the last property, point-wise comple­ tion is still different from playing (which is always point­ wise) : On every point of the interval [tl> t2], ts1 plays but does not complete!

The issue of whether to analyze the truth of some entity over time intervals or over time points has been discussed at some length in the literature of temporal log­ ics in AI [Allen 1984], [McDermott 1982], and [Shoham 1987a]. Using the C and P predicates, we are able to handle both.

5. Related Work

The most well known treatments of temporal infor­ mation in AI are the works of Allen, McDermott, Sho­ ham, Kowalski, and Haugh. Shoham's logics seem to subsume the other above mentioned works. Therefore, we compare our logic to his .

First we show that every formula of Shoham's first order interval temporal logic can be simulated by a for­ mula in the logic of time structures that has the context time structure as a free variable. This simulation can be further augmented to apply to Shoham's monotonic modal logic of Temporal Knowledge - but this is an option that we do not pursue. Instead, we show that the preference criterion on mod~ls of the modal logic of Temporal Knowledge, called chronologically more ignorant, can be formulated as a first order formula, involving comparison of time structures. A major pro­ perty of this simulation is that it avoids problems associ­ ated with the chronological minimization of models of Shoham's classical interval logic; problems that caused Shoham to switch to the more sophisticated modal logic of chronological ignorance. We conclude with an exam­ ple that demonstrates the simulation, in the logic of time structures, of nonmonotonic reasoning in Shoham's modal logic of chronological ignorance.

5.1. Shoham's Classical Interval Temporal Logic

Shoham's logic contains, variables, constant sym­ bols, predicates, logical connectives and quantifiers, that are analogous to those of the logic of time structures, with minor modifications. His logic makes a syntactic dis­ tinction between variables and terms denoting time points versus those denoting domain objects, whereas we made only a semantic one. Also, in the classical version, Sho­ ham assumes only a partial ordering on the set of time points, not a total ordering as we did . Our comparison applies only to totally ordered sets of time points. Note, that in the modal version, Shoham assumes the structure of the integers, i.e., a total ordering.

A special construct of Shoham's logic is TRUE(tl> t2, p) where t1 and t2 are time terms, and pis a predication. This is just notation for the interval-predication pair <<t1 ,t2>, p>. The semantics of the logic will assign, under a given interpretation and variable assignment, a set of time intervals to the predica­ tion p. If <t1> t2> is in this set, then TRUE(ti> t2, p) is true under this interpretation and assignment. Notice that in this interval logic, there is one world containing a single time line, and all formulas are related to this one time line. Therefore, in this comparison, we will restrict formulas to refer to a single time structure as the fourth argument of the C predicate.

Corresponding to a set of wffs 4> of Shoham's logic, we have the wff 4>1 (ts) where 4>1 of our logic is the follow­ ing set of translated wffs:

1. If 4> is t1 = t2, or t1 ;$ t2, for temporal terms th tz, then 4>1 is 4>.
2. For a predication p (without negation), if 4> is TRUE(ti> t2, p ), then 4>1(ts) is C(th t2, [p,t2-t1], ts).
3. If 4> 1 and 4> 2 are wffs, then (4> 1 A 4> 2 )1(ts) is 4> \(ts) A 4> 2 1(ts).
4. The cases for disjunction, negation, and quantifiers are similar.

We want now to prove that the translation preserves satisfiability, and logical implication. For that purpose we first relate the notions of interpretations in the two logics. We look only at interpretations in the logic of time structures that satisfy all the apriori require­ ments for being a model : The assignments to the special symbols 0, NIL, [ ], ·, ~. =, C, to the arithmetic time functions, to list functions, and to the time structure operators, must satisfy their axioms and "definitions".

Such interpretations are regular interpretations.

Definition· Given I, a regular time structure interpreta­ tion + variable assignment (to all variables), ts, a variable of signature h, and J, an interval logic interpretation + variable assignment. We say that (I, ts) corresponds to J if:

1. I and J have the same set of time points, with the same ordering; assignments in I to constants and variables of signature t is the same as the assign­ ments in J to time point symbols and to temporal variables.
2. The assignment to ts in I satisfies: For all time terms th t2, and predication p in the interval logic:

In the following lemma we restrict the time struc­ tures to include only the symbols appearing in a given set IJr of wffs. The notion of correspondence between interpretations turns into IJF-correspondence.

Lemma 1. Given IJr, a set of time structure wffs, we assume that the language of time structures includes only the symbols in IJr. Then, for every regular time struc­ ture interpretation + variable assignment I, and a signa­ ture h variable ts, there exists a IJF-corresponding interval logic interpretation + 'variable assignment J, and vice­ versa.

Comment· The restriction on the language of time structures is needed because we have to split the function n symbols of signature .X SX{ d} in the logic of time struc·=1 tures, into predicates and function symbols in the interval logic.

Lemma 2. Every pair of ~ and ~1(ts), a set of wffs in the interval logic, and its translation into the time structure logic, is equi-satisfiable.

Corollary: If J and (I, ts) are ~ccorresponding interpretations, then

5.2. Chronological Ignorance In Time Structures

Shoham introduces two versions of chronological minimization. First, for a given set S of primitive propo­ sitions, he defines a preference criterion called chrono­ logically smaller in S, on models of the classical interval logic. Intuitively, a model Mz is chronologically smaller in S than a model M1 if, for all propositions in S, they 'agree' up to a certain time point to, and at t0 M1 has information about a proposition in S, that Mz does not. The problem with this preference criterion is its depen­ dency on the set S, whose selection seems to depend on the desired conclusions. To solve this problem, Shoham introduces a logic called CI (Chronological Ignorance), which is a nonmonotonic version of a modal logic of tem­ poral knowledge. The nonmonotonicity of CI results from a preference criterion on Kripke structures, called chronologically more ignorant. The idea behind this cri­ terion is similar to the previous one, but now the minimi­ zation involves all kn.mYn. propositions. This idea could not be applied directly to the classical interval logic (i.e., take S as the set of all propositions), since in classical logic for every proposition p, either p or its negation is true over any given interval (the strong law of excluded middle), thereby turning every model into a chronologi­ cally minimal one.

In this section we try to incorporate the chronologi­ cally more ignorant criterion described above, into the (first order) logic of time structures. The idea is that his­ tory Hz is chronologically more ignorant than history HJ. if they 'agree' up to a certain time point to, and H1 has information at to that Hz does not. This relation between histories is captured by the predicate ?, called chronolog­ ically more ignorant. The predicate is defined by the fol­ lowing first order formula:

Definition - The chronologically more ignorant predicate:

Note that, as with Shoham's latter chronologically more ignorant criterion, our chronological preference predicate is defined with respect to .all primitive terms, not just terms within a given set of propositional primitive terms. The reason we can do that, within the scope of first order logic, is that the strong law of excluded middle does not apply to time structures: it is not the case that for any primitive proposition, either it completes over a given interval, or its (term level) negation completes over that interval.

A chronologically maximally ignorant history with respect to a given theory is characterized by the CMI predicate as follows :

Definition- Given IJF(ts), a formula in the logic of time structures. The CMI predicate, with respect to IJr is defined by:

The following three claims summarize the relation­ ship between the nonmonotonic version of Shoham's clas­ sical logic, defined by the chronologically smaller in S preference criterion, to the logic of time structures. All claims refer to a formula ~ of the interval logic, and to ~1 , its translation into the logic of time structures. The set S is ~ as the set of all primitive terms in ~1 ·

Lemma 3. Let J; and (I, tsJ, for i=l,2, be ~~­ corresponding interpretations and variable assignments. Then,

Jz is chronologicall>' smaller in S than Jt. (denoted J1 Cs Jz iff I r ts1 $ tsz

That is, the correspondence between interpretations preserves the chronologically smaller relationship.

Lemma 4. If J and (I, ts) are ~1-corresponding interpretations and variable assignments, then

J is a chronologically smallest in S model of ~ iff I F CMI<t> 1 (ts).

Theorem 2. ~ Fcs 4> iff ~1(ts) II {definitions of ?, CMI<t> 1 } II CMI<t> 1 (ts) F 4>1(ts)

We have shown that the notion of chronological ignorance can be implemented in the logic of time struc­ tures, using first order tools alone. Below, we present an example of chronological ignorance based reasoning in our logic.

6. An Example

Shoham characterizes two major problems in rea­ soning about change; the solutions he suggests are within his modal logic of chronological ignorance [Shoham 1987b ].

The qualification problem is "the problem of having to specify too many conditions in order to make even a single prediction about the future" . The extended predic­ tion problem is "the difficulty of predicting things about extended periods of time in the future" . Shoham claims that the extended prediction problem subsumes the famous frame or persistence problem.

We consider the Yale shooting example, which is now firmly established in the AI folklore. In [Balaban & Murray 1988], we provide two formulations of this example in our logic that address, respectively, qualification and extended prediction. Here we present the latter formulation which is a generalization of the former . The set of time points is assumed to have the structure of the integers.

Point-wise facts that are expected to persist (like C(1,1,[loaded,O],ts) ) are interval-wise statements, with unspecified upper time points. The CMI criterion forces these statements to be clipped at the latest possible time, i.e., to persist as long as possible. The frame axiom is, of course, dropped. This formulation is similar to Shoham's potential histories formulation.

There are six axioms:

1. 3 v, d C(1, v, [loaded,d], ts)
2. C(5, 5, [pull-trigger,O], ts)
3. v t, d
4. C(t, t, [pull-trigger ,0], ts) ~ -.P(t+ 1, [loaded,d], ts)
5. C(t, t, [emptied-manually,O], ts) ~ -.P(t+1, [loaded,d], ts)
6. v t, d

where <I> is the conjunction of denials of 'abnormalities' like -,P(t,[vaccum,d),ts) .

1. Definition of;;:
2. Definition of CMI~, with it taken as the conjunction of formulas 1 to 4 above.

Under this formulation, the "expected results" are obtained. Although we have no knowledge about per­ sistence of propositions over time, we can conclude that loading persists up to time point 5, and causes the noise at time 6.

7. Conclusion

We have shown that we can formulate Shoham's notion (in his classical interval logic) of chronological ignorance. Clearly, we can formulate his preference cri­ terion on Kripke structures by a preference criterion on models of the logic of time structures. But then we end up with a nonmonotonic logic built on a first order one, rather than on a modal logic. We prefer capturing these notions with purely first order formulas involving time structures.

The main point here is not the imitation of Shoham's work, but that we have implemented some kind of model preference mechanism through axio~s in a first order logic. Should we desire an entirely different prefer­ ence criterion, we might only require a new axiom set; we need not build a new logic, define its semantics, and design its inference or model-building engine from scratch. Furthermore, because of our particular encoding of temporal knowledge, the strong law of the excluded middle does not hold in any of our "worlds." Thus we have not been forced away from first order and toward modal logic.