Machine-checking the Timed Interval Calculus

Jeremy E. Dawson ^{⋆} and Rajeev Goré ^{⋆⋆}

Department of Computer Science and Automated Reasoning Group Australian National University, Canberra ACT 0200, Australia

                  http://users.rsise.anu.edu.au/~jeremy/
                   http://users.rsise.anu.edu.au/~rpg/

Abstract. We describe how we used the interactive theorem prover Isabelle to formalise and check the laws of the Timed Interval Calculus (TIC). We also describe some important corrections to, clarifications of, and flaws in these laws, found as a result of our work. Keywords: reasoning about time, automated reasoning, theorem proving

1 Introduction

Reasoning about time plays a fundamental role in artificial intelligence and computer science. Various approaches have been taken to formalise such reasoning. A logic-based approach leads to propositional temporal logics [5] while a more direct approach leads to various calculi for reasoning about time explicitly [1, 13, 4]. The logical approaches have an in-built rigour due to soundness and completeness results with respect to rigorous semantics. The direct methods are more intuitive and easier to use for practitioners who are not always well-versed with formal logic. Nevertheless, the logical consistency of such direct methods is paramount for applications. For example, the Timed Interval Calculus (TIC) has been used in the formal development of a real-time system [10].

Following Fidge et al. [4], Wabenhorst [12] gives a rigorous semantics for the TIC in terms of our usual set-theoretic understanding of time, points and intervals. He states 18 “laws” designed to enable convenient proofs about the TIC, and gives proofs of some important theorems about the TIC. We used the proof assistant Isabelle to formalise and check the logical rigour of these laws with respect to their semantics. It might seem that the validity of the laws (and, even more so, many of our lemmas) is intuitively obvious. However, the “devil is in the detail”, and rigorous formalisations such as ours have often exposed bugs, even in refereed publications. Indeed, we found problems with the laws given in [4] and [12], once again showing the worth of machine-checked proofs.

Various authors have already formalised another interval calculus called the Duration Calculus [13]. Heilmann’s [6] proof assistant Isabelle/DC is built using Isabelle and SVC (Stanford Validity Checker), while Skakkebæk’s [11] PC/DC (Proof Checker for Duration Calculus) is built upon PVS.

⋆ Supported by an Australian Research Council Large Grant ⋆⋆ Supported by an Australian Research Council QEII Fellowship

However, we know of only one other attempt to formalise the TIC. In [2], Cerone describes an implementation of the TIC in the theorem prover Ergo. This work differs from ours in the following important respects. Cerone provides an extensive axiomatisation of the time domain, whereas we use the theory of the reals provided with Isabelle/HOL. In respect of concatenation, our work is based on the definition given by Wabenhorst, from which we proved more powerful results which were more convenient to use. Cerone assumes more powerful axioms, which are not proved to be derivable from Wabenhorst’s formulation. If, therefore, they were in fact not derivable from Wabenhorst’s formulation, this would not become apparent from the work in [2]. In fact, Cerone’s axiom I9 appears to allow concatenation of two intervals which are both open at their common endpoint, though this difference from [12] is not commented on. Cerone sets up a special syntax and many axioms relating to lifting functions and predicates over the time and interval domains, which make definition of Wabenhorst’s special brackets easier. Finally, [2] deals with proofs of only 5 laws.

In the remainder of § 1 we introduce the TIC, Isabelle, and Wabenhorst’s laws in some detail. In § 2 we describe our formalisation of the laws and the problems we encountered. In § 3 we conclude. The full code of our machine-implementation

can be found at http://rsise.anu.edu.au/~jeremy/tic/tic-files/.

Acknowledgements: We are extremely grateful to Axel Wabenhorst for his prompt clarifications, and to Brendan Mahony for bibliographic pointers.

1.1 The Timed Interval Calculus

The Timed Interval Calculus (TIC) is introduced by Fidge et al. [4] as a formal method for reasoning about time-dependent behaviour. As in other timed-trace formalisms, a time-dependent variable is modelled by a function from the set of real numbers. The TIC allows us to reason about (non-empty and finite) time intervals over some domain of time 𝕋. Time intervals are represented as all time points in 𝕋 between some start-point a and some end-point b. There are then four possible choices depending upon whether the end-points are included or excluded from this interval. For example, the notation (a, b] indicates all time intervals between a and b which exclude a but include b.

The main specification format in TIC is a notation for defining the set of all time intervals in which some predicate P is everywhere true. The predicate may depend not only on the particular time point but also on the endpoints or length of the interval. The notation uses special brackets to distinguish the four possible choices for including and excluding end-points. Fidge et al. [4] give 13 laws which capture fundamental properties of time intervals defined via the TIC notation. In [12] Wabenhorst gives 18 such laws, including most of those in [4]. The correctness of these laws is the focus of our work.

1.2 Isabelle/HOL

Isabelle is an automated proof assistant [8]. Its meta-logic is an intuitionistic typed higher-order logic, sufficient to support the built-in inference steps of higher-order unification and term rewriting. Isabelle accepts inference rules of the form “from α_{1}, α_{2}, …, α_{n}, infer β” where the α_{i} and β are expressions of the Isabelle meta-logic, or are expressions using a new syntax, defined by the user, for some “object logic”. In practice most users would build on one of the comprehensive “object logics” already supplied [9].

We use the most commonly used Isabelle object logic, Higher Order Logic (HOL), which is an Isabelle theory based on the higher-order logic of Church [3] and the HOL system of Gordon [7]. Thus it includes quantification and abstraction over higher-order functions and predicates. The HOL theory uses Isabelle’s own type system and function application and abstraction: that is, object-level types and functions are identified with meta-level types and functions. Isabelle/HOL contains constructs found in functional programming languages (such as datatype and let) which greatly facilitates re-implementing a program in Isabelle/HOL, and then reasoning about it. However limitations (not found in, say, Standard ML itself) prevent defining types which are empty or which are not sets, or functions which may not terminate.

Due to space limitations, we assume that the reader has some familiarity with Isabelle and logical frameworks in general.

1.3 TIC definitions and laws

As stated previously, 𝕋 is some fixed domain of time points, typically the reals (our proofs use the completeness and density of the reals). The set of all nonempty finite time intervals over this domain is 𝕀. Following Fidge et al. [4], Wabenhorst [12] defines several symbols – the following definitions are (or are close to) his. Suppose P is some predicate, and let α be the start-point and ω be the end-point of our intervals.

Let (-P -] be the set (of left-open-and-right-closed intervals)

(-P -] ≡ {(α … ω] | α, ω : 𝕋 ∧ α < ω ∧ ∀t : (α … ω]P (t, α, ω)}

Thus all intervals in (-P -] are non-empty, and for every interval I ∈ (-P -] and every x ∈ I, x satisfies P. Note that predicate P may also depend on the endpoints α and ω of the interval, whose length ω − α is often abbreviated by δ.

The left-and-right-open intervals (-P -), the left-closed-and-right-open intervals [-P -) and the left-and-right-closed intervals [-P -] are defined similarly, though for [-P -] the non-emptiness condition is α ≤ ω. The right-open intervals [(-P -) are defined by [(-P -) ≡ [-P -) ∪ (-P -), and [(-P -], (-P -)], [-P -)] and [(-P -)] are defined correspondingly as the right-closed, left-open, left-closed and left-and-right-open-or-closed intervals respectively. In the Isabelle code [(-P -) is represented as [(-P-), and the others likewise.

To reason about adjacent intervals, Wabenhorst defines concatenation of sets of intervals. Two intervals x and y can be joined if they meet with no overlap or gap, that is, x ∪ y is an interval and x ∩ y = ∅. Then, for sets X and Y of intervals, their concatenation X; Y is obtained by joining x ∈ X with y ∈ Y wherever this is possible. Thus

X; Y ≡ {x ∪ y | x : X ∧ y : Y ∧ x ∪ y : 𝕀 ∧ ∀t_{1} : x ∀t_{2} : y t_{1} < t_{2}}

Exceptionally, 1 is used for {∅}, which may be an operand for, and is an identity of, the concatenation operator. Finally, \overline{S} means S ∪ 1.

A predicate P is defined to have the finite variability property if there exists a duration ξ > 0 such that [(-¬P -)]; [(-◇P -)]; [(-¬P -)] ⊆ [(-δ >= ξ-)].

Wabenhorst [12] gives 18 laws for the Timed Interval Calculus, as shown in Figure 1. Fidge et al. [4] give 13 laws, most of which are included in Wabenhorst’s 18 laws. The remaining two are shown in Figure 2.

A common special case for [(-P -)] (etc) is where predicate P takes a single argument, and does not involve the endpoints of the interval: the latter is expressed by the condition “if α, ω and δ do not occur free in P ” (e.g. Law 11).

However in formalising the laws, we noticed a similar phrase in Law 10 involving arbitrary sets of intervals S, T, U. We saw this as meaningless, except in the special case where S, T, U have a form such as [-P -] or (-P -) — see § 2.1.

2 Verification of the laws

As can be seen from Figure 1, Wabenhorst’s laws are really statements about the special notation of TIC. The semantics of this notation is its underlying meaning in terms of sets of time intervals over 𝕋, which is stated to be the real numbers ℝ. To verify these laws, we must confirm that they are correct with respect to this underlying semantics, so we had to reason formally about real numbers. We used the real number libraries for Isabelle/HOL, which include theorems relating to least upper bounds and completeness and density of the reals.

The datatype interval, defined below, uses the two endpoints of the interval, and an indicator of whether the interval is closed or open at these endpoints:

datatype interval =
         CC real real | CO real real | OC real real | OO real real

This datatype allows (many different values representing the) empty interval, so many of our theorems include the additional condition that the interval(s) concerned are non-empty. The set of all non-empty intervals is 𝕀, written in Isabelle as II. We wrote numerous functions for reasoning about aspects of intervals: the types and short-hand notations for some of these are shown in Figure 3. We describe many of these in what follows at appropriate places.

We found it streamlined some proofs to be able to consider each end of an interval separately. Thus we defined a datatype bndty to take a real bound and indicate whether an interval is open or closed at that bound, and functions ubt (“upper bound and type”) and lbt, for example:

datatype bndty = Closed real | Open real
ubt_CC = "ubt (CC ?beg ?end) = Closed ?end" : thm

The function setof gives the actual set which an interval defines:

setof_OC = "setof (OC ?beg ?end) = {x.?beg < x & x <= ?end}" : thm

Law 1 (Monotonicity) If for all α, ω and δ in 𝕋 and all t : (α … ω]

P (t, α, ω) ⇒ Q(t, α, ω), then (-P -] ⊆ (-Q-]. Law 2 (True and false) [(-true-)] = 𝕀 and [(-false-)] = ∅ Law 3 (And) [(-P -)] ∩ [(-Q-)] = [(-P ∧ Q-)] Law 4 (Or) [(-P -)] ∪ [(-Q-)] ⊆ [(-P ∨ Q-)] Law 5 (Not) [(-¬P -)] ⊆ 𝕀\[(-P -)] Law 6 (Concatenation monotonicity) If S ⊆ S′ and T ⊆ T′ then S; T ⊆ S′; T′. Law 7 (Concatenation associativity) (S ; T) ; U = S ; (T ; U) Law 8 (Concatenation zero and unit) S; ∅ = ∅; S = ∅ and S; 1 = 1; S = S. Law 9 (Concat. union) (S ∪T); U = (S; U)∪(T; U) and S; (T ∪U) = (S; T)∪(S; U) Law 10 (Concatenate intersection) (S ∩ T); U ⊆ (S; U) ∩ (T; U) and U; (S ∩ T) ⊆

(U; S) ∩ (U; T) Equality holds in the first case if ω and δ are not free in S and T, and in the second case if α and δ are not free in S and T.

Law 11 (Concatenate property) If α, ω and δ do not occur free in P, then

[(-P ∧ δ > 0-)] = [(-P -)]; [(-P -)]. Law 12 (Always) If α, ω and δ are not free in P, then [(-□P -)] = [(-P -)]. Law 13 (Induction on Lengths) Let H(X) be a formula containing X : ℙ𝕀∪1, but

no occurrence of negation or the complement of X. Let P be a predicate for which the finite variability property holds. If

(a) H(1) and

(b) H(X) ⇒ H(X ∪ (X; [(-P -)]) ∪ (X; [(-¬P -)]))

then H(\overline{𝕀}). Law 14 (Induction on Histories) Let H(X) be a formula containing X : ℙ𝕀, but

no occurrence of negation or the complement of X. Let P be a predicate for which the finite variability property holds. If

(a) H([(-ω < 0-)]) and

(b) H(X) ⇒ H(X ∪ (X; [(-P -)]) ∪ (X; [(-¬P -)]))

then H([(-α < 0-)]). Law 15 (Ignore Prefix) Suppose that there exists r : 𝕋 such that for all

I : [(-α < r-)], {I}; S ⊆ {I}; T. Then S ⊆ T. Law 16 (Distribute Intersection) If α, ω and δ are not free in P, then

[(-P -)] ∩ (S; T) = ([(-P -)] ∩ S); ([(-P -)] ∩ T). Law 17 (Endpoints) If α, ω and δ are not free in P and Q, and if P or Q is finitely

variable, then

[(-P ∨ Q-)] = \overline{[(-P ∨ Q-)]}; ([(-P -)] ∪ [(-Q-)]) = ([(-P -)] ∪ [(-Q-)]); \overline{[(-P ∨ Q-)]} Law 18 (Implicit Duration) If α, ω and δ are not free in P and Q, then

[(-P ∧ δ > r-)] ⊆ \overline{[(-true-)]}; [(-Q-)] ⇔ [(-P ∧ δ > r-)] ⊆ \overline{[(-δ ≤ r-)]}; [(-Q-)]

Fig. 1. Laws for the Timed Interval Calculus

Law 11 (Concatenate fixed intersection) If r ≥ 0 then

\begin{aligned}& ((S ∩ [(-δ = r-)); T) ∩ ((U ∩ [(-δ = r-)); V) = (S ∩ U ∩ [(-δ = r-)); (T ∩ V) \\ & & (S; (U ∩ (-δ = r-)])) ∩ (T; (V ∩ (-δ = r-)])) = (S ∩ T); (U ∩ V ∩ (-δ = r-)]) \end{aligned}

Similarly with [(- … -) and (- … -)] replaced by [(- … -] and [- … -)] respectively. Law 13 (Concatenate duration) If α, ω and δ are not free in P, r ≥ 0 and s ≥ 0,

where r > 0 or s > 0, then [(-P ∧ δ = r + s-)] = [(-P ∧ δ = r-)]; [(-P ∧ δ = s-)]

Fig. 2. Additional Laws of Fidge et al.

consts
  setof        :: "interval => real set"
  nonempty     :: "interval => bool"
  negint       :: "interval => interval"
  emptyint     :: "interval"
  no_aod       :: "([real] => bool) => ([real, real, real] => bool)"
  OCints       :: "([real, real, real] => bool) => interval set" ("'(-_-]")
  cat          :: "[interval set, interval set] => interval set"
                  ("_;; _" [75, 76] 75)
  clp, crp     :: "interval set => bool"
  ubt          :: "interval => bndty"
  lbt          :: "interval => bndty"
  btopp, negbt :: "bndty => bndty"
  ubc          :: "bndty => real => bool"
  lbc          :: "bndty => real => bool"
  realval      :: "bndty => real"
  "--->"       :: "['a => bool, 'a => bool] => bool"     (infixr 25)

Fig. 3. Various Functions for Reasoning About Intervals

Lemma 1. (i) On non-empty intervals, the function setof is 1-1. (ii) The upper and lower bounds of an interval (including their types, ie, Closed

or Open) determine the interval.

setof_cong = "[| nonempty ?int1; setof ?int1 = setof ?int2 |]
   ==> ?int1 = ?int2" : thm
bts_unique = "[| lbt ?int1 = lbt ?int2; ubt ?int1 = ubt ?int2 |]
   ==> ?int1 = ?int2" : thm

It was frequently convenient to use a theorem relating to the upper bound of an interval and use the theorem relating to the upper bound of the negated interval, rather than prove from scratch the corresponding theorem for the lower bound. So we defined a function negint, which negates an interval, and a function negbt, which negates a bound, by, for example:

negint_O = "negint (OC ?beg ?end) = CO (- ?end) (- ?beg)" : thm
negbt_Open = "negbt (Open ?x) = Open (- ?x)" : thm

Thus we have lemmata such as the following.

Lemma 2. The upper bound of the negation of A is the negation of the lower

bound of A.  ubt_neg = "ubt (negint ?A) = negbt (lbt ?A)" : thm

In discussing concatenation of intervals, we are interested in pairs (A, B) of intervals such that (for example) ubt A = Closed r and lbt B = Open r since such intervals meet with no overlap or gap at r. We therefore defined a function btopp which “opposes” an Open bound into a Closed one, and vice versa.

btopp_Closed = "btopp (Closed ?x) = Open ?x" : thm

For a point t to lie within an interval like (α … ω], it must satisfy α < t and t ≤ ω. We refer to these two conditions as the “lower (upper) bound condition”. Just as we found it convenient to consider separately the lower and upper bounds of an interval, we found it convenient to consider separately these two conditions satisfied by points within an interval. So we defined further functions ubc and lbc (one clause of the definition is given below), and proved the lemma bnd_conds.

ubc_Closed = "ubc (Closed ?end) ?x = (?x <= ?end)" : thm

Lemma 3 (bnd conds). A point lies in an interval if and only if it satisfies the lower and upper bound conditions for the interval.

bnd_conds = "(?x : setof ?intvl) =
   (lbc (lbt ?intvl) ?x & ubc (ubt ?intvl) ?x)" : thm

We then needed facilities to manipulation these conditions. Firstly a “lifted” implication --->, which provides a reflexive and anti-symmetric ordering.

liftimp         = "?p ---> ?q == ALL s. ?p s --> ?q s" : thm
liftimp_refl'   = "?s = ?t ==> ?s ---> ?t" : thm
liftimp_antisym = "[| ?t ---> ?s; ?s ---> ?t |] ==> ?s = ?t" : thm

Relation ---> is also transitive, but we do not use this. It is not generally linear, but the result ubc_linear and the others shown below were useful.

Lemma 4. (ubc cong) The function ubc is 1-1. (ubc linear) The relation ---> is linear on conditions of the form ubc s. (ubc rel) If x satisfies the upper bound condition for an interval, and y ≤ x,

then y satisfies the upper bound condition for the interval.

ubc_cong   = "ubc ?t = ubc ?s ==> ?t = ?s" : thm
ubc_linear = "(ubc ?t ---> ubc ?s) | (ubc ?s ---> ubc ?t)" : thm
ubc_rel    = "[| ubc ?b ?x; ?y <= ?x |] ==> ubc ?b ?y" : thm

Several results related these functions to ones previously described, e.g.:

Lemma 5. (ubc opp) Let b be a bound, and b′ its opposite (ie, Open instead of Closed, or vice versa). Consider b as a lower bound and b′ as an upper bound. Then x is within b′ if and only if x is not within b.

(ubc neg) Let b be a bound, and b′ its negation (eg, if b is Open z then b′ is Open (−z)). Consider b as a lower bound and b′ as an upper bound. Then x is within b′ if and only if −x is within b.

   ubc_opp = "ubc (btopp ?b) ?x = (~ lbc ?b ?x)" : thm
   ubc_neg = "ubc (negbt ?b) ?x = lbc ?b (- ?x)" : thm

Results using properties of real numbers often required many easy lemmata and a proof by cases: e.g. ubc x ---> ubc y has four cases of which one is:

   "(ubc (Closed ?x) ---> ubc (Open ?y)) = (?x < ?y)" : thm

We now give results which, though in some cases intuitively quite simple, were more difficult to prove because our mental model of an interval includes some aspects which are not part of the definition. Therefore we had to prove some results about intervals which we needed to use later. The theorem betw_char, which was quite difficult to prove, gives a characterisation of finite intervals. The result disj_alt is related to the manner in which concatenation is defined.

Lemma 6. (betw char) A set S is an interval if and only if it is bounded above and below and satisfies the condition that for any x, y ∈ S and any z, if x ≤ z ≤ y then z ∈ S.

(disj alt) If I_{1} and I_{2} are disjoint intervals, then either every point in I_{1} is less than every point in I_{2}, or vice versa.

betw_char = "(EX intvl. setof intvl = ?S) =
 ((EX ub. isUb UNIV ?S ub) & (EX lb. isLb UNIV ?S lb) &
  (ALL x y z. x <= z & z <= y & x : ?S & y : ?S --> z : ?S))" : thm
disj_alt = "(setof ?I1 Int setof ?I2 = {}) =
   ((ALL t1:setof ?I1. ALL t2:setof ?I2. t1 < t2) |
    (ALL t1:setof ?I1. ALL t2:setof ?I2. t2 < t1))" : thm

2.1 Concatenation

Proving results about concatenation of interval sets was considerably more difficult. We defined a predicate abuts to indicate that two intervals meet exactly, so that they may be joined. The definition is abuts_def, but we found that some other characterisations of abuts were more useful. Note that ?S *<= ?x means ∀y ∈ S.y ≤ x. Proving these results was surprisingly tedious and difficult.

Lemma 7. (abuts def) Two sets A and B abut iff the upper bound x of A is

the lower bound of B, and x is in one but not both. (abuts un disj) Two non-empty intervals A and B abut iff their union is an

interval and all points in A are less than all points in B. (abuts betw char) If A and B are intervals, and a ∈ A, b ∈ B, then A and B

abut iff for any c such that a ≤ c ≤ b, c is in exactly one of A and B. (abuts UnL) If A, B, C are sets, b ∈ B and ∀a ∈ A.a ≤ b then B and C abut iff

(A ∪ B) and C abut.

abuts_def = "abuts ?A ?B == EX x.
   isLub UNIV ?A x & isGlb UNIV ?B x & (x : ?A) = (x ~: ?B)" : thm
abuts_un_disj = "[| nonempty ?A; nonempty ?B |] ==>
   abuts (setof ?A) (setof ?B) =
      ((EX C. setof C = setof ?A Un setof ?B) &
       (ALL a:setof ?A. ALL b:setof ?B. a < b))" : thm
abuts_betw_char = "[| ?a : setof ?A; ?b : setof ?B; ?a <= ?b |]
   ==> abuts (setof ?A) (setof ?B) = (ALL c.
    ?a <= c & c <= ?b --> (c : setof ?A) = (c ~: setof ?B))" : thm
abuts_UnL = "[| ?b : ?B; ?A *<= ?b |] ==>
   abuts ?B ?C = abuts (?A Un ?B) ?C" : thm

Here Un is the set union operation in Isabelle/HOL, while Int (used later) is the set intersection operation. We use “;;” to stand for the TIC concatenation operator “;”, and define concatenation (of sets of intervals) by

cat_def = "?X ;; ?Y == {intvl.  EX x:?X.  EX y:?Y.
   setof intvl = setof x Un setof y &
     (ALL t1:setof x. ALL t2: setof y. t1 < t2)}" : thm

We prove an alternative characterisation cat_abuts. The easy lemma mem_cat_UN relates {a}; ; {b} to A; ; B where A and B are sets of intervals and a and b are intervals.

Lemma 8. (mem cat UN) x ∈ A; B if and only if there exist a ∈ A, b ∈ B such

that x ∈ {a}; {b}. (cat abuts) x ∈ {a}; {b} if and only if a ∪ b is an interval and, if a and b are

non-empty, they abut.

mem_cat_UN =
  "(?x : ?A;;?B) = (EX a:?A. EX b:?B. ?x : {a};;{b})" : thm
cat_abuts = "?A ;; ?B = {intvl.  EX a:?A.  EX b:?B.
  setof intvl = setof a Un setof b &
  (nonempty a & nonempty b --> abuts (setof a) (setof b))}" : thm

The proof of Law 7 (Concatenate associativity) turned out to be more difficult than most of the others. Our first proof was achieved using cat_abuts,

abuts_un_disj, abuts_UnL, and a corresponding result abuts_UnR.

Subsequently we found an easier approach. We used abuts_bnds to characterise when two intervals can be joined, and single_cat' to describe the result of joining them. It was straightforward but tedious to then prove single_cat3l', and the similar result single_cat3r', differing only in containing (?x :{?A} ;;({?B} ;; {?C})). Proving Law 7 was then straightforward.

Lemma 9. (abuts bnds) Two non-empty intervals A and B abut iff the upper

bound of A is the opposite of the lower bound of B. (single cat') Two non-empty intervals B and C can be concatenated to form

a third interval A iff they abut (as above) and A, B have the same lower bound, and A, C have the same upper bound.

abuts_bnds = "[| nonempty ?A; nonempty ?B |]  ==>
 abuts (setof ?A) (setof ?B) = (ubt ?A = btopp (lbt ?B))" : thm
single_cat' = "[| nonempty ?B; nonempty ?C |] ==>
 (?A : {?B} ;; {?C}) = (lbt ?A = lbt ?B
     & ubt ?A = ubt ?C & ubt ?B = btopp (lbt ?C))" : thm
single_cat3l' = "[| nonempty ?A; nonempty ?B; nonempty ?C |] ==>
 (?x : {?A} ;; {?B} ;; {?C}) = (lbt ?x = lbt ?A
     & ubt ?x = ubt ?C & ubt ?A = btopp (lbt ?B)
     & ubt ?B = btopp (lbt ?C))" : thm

As mentioned above, Law 10 as stated was meaningless, something which we found as soon as we started to think about how we would formalise the law in Isabelle, showing the value of a detailed formalisation. We felt that the “⊆” parts were correct, but that the statement “Equality holds … if ω and δ are not free in S and T ” is not meaningful. References to ω and δ makes sense only in the context of a function P (of t, α, and ω), which arises when the forms of S and T are drawn from [(-.-)], [(-.-], [(-.-), [-.-)], [-.-], [-.-), (-.-)], (-.-], and (-.-).

We have therefore proved a version of Law 10 where both S and T are of the same form, and that form is one of [(-.-)], [(-.-], [(-.-), [-.-)], [-.-], [-.-), (-.-)], (-.-], and (-.-). We are currently formalising the cases in this version of Law 10 where S and T are of different forms.

Alternatively, changing Law 10 to allow S, T and U to be arbitrary avoids the question of references to α, δ and ω altogether, but letting S = {[1 … 2]}, T = {[1 … 3]}, U = [(-true-)] gives a counter-example to this version of Law 10.

Finally, we also tried to replace Law 10 by a more complex law. We defined a predicate clp of a set of intervals (“Closed under taking Left Part”) to mean that for x ∈ S, if y is a non-empty interval which has the same left endpoint but a lower right endpoint, then y ∈ S. Under the assumption that S and T satisfy this condition, we then proved equality of one of the clauses of Law 10 as below:

clp_def = "clp ?S == ALL s:?S.  ALL a:II.
 (ubc (ubt a) ---> ubc (ubt s)) & lbt s = lbt a --> a : ?S" : thm
law10ra = "[| ?S <= II; ?T <= II; clp ?S; clp ?T |] ==>
 (?S Int ?T) ;; ?U = ?S ;; ?U Int ?T ;; ?U" : thm

But condition clp is too strong: [(-P -)] satisfies it, but [(-P -] and [(-P -) do not.

Law 11 was formulated as follows. It uses no_aod whose argument is a predicate P which depends only on t, not on α or ω. The % symbol is Isabelle’s notation for the function abstraction operator λ.

law11 = "[(-%t a w. ?P t & 0 < w - a-)] =
         [(-no_aod ?P-)] ;; [(-no_aod ?P-)]" : thm
no_aod_def = "no_aod ?Q ?t ?a ?w == ?Q ?t" : thm

The forward direction required 4 cases (is the interval open or closed at either end) and the reverse 16 cases (using the form of each of the two intervals).

We also considered Laws 11 and 13 of [4] (see Figure 2), which concern concatenation of sets of intervals and are different from any of Wabenhorst’s laws. We proved Law 11. However we found that Law 13 is wrong as it stands – it requires the stronger assumption r > 0 and s > 0. For if, say, s = 0, then the only intervals of length s are those which are closed at both ends, and yet [(-P ∧ δ = r + s-)] can contain intervals which are open at the right-hand end. We proved the law with the stronger assumption r > 0 and s > 0.

2.2 The modality □

The modality ◇ is used to express the notion of a property holding somewhere within an interval, and [(-◇P -)] is used for the set of intervals within which P holds somewhere. The definition uses the fact that, in that case, P will hold on a subinterval, which may be at the left- and/or right-hand end of the interval, or both, or neither. Thus [(-◇P -)] ≡

([(-true-)]; ; [(-P -)]; ; [(-true-)] ∪ [(-true-)]; ; [(-P -)] ∪ [(-P -)]; ; [(-true-)] ∪ [(-P -)])

Wabenhorst also defines [(-□P -)] ≡ 𝕀 \ [(-◇P -)], noting it is not generally equal to [(-P -)]. Law 12 states that equality holds if α, ω and δ do not occur free in P, and, again, this is expressed using the function no_aod. Again, the proof involved a large number of cases, depending on whether a point not satisfying P is in the interior or either end of a larger interval, and whether that larger interval is closed or open at each endpoint.

2.3 The remaining laws

Laws 13, 14 and 17 involves the finite variability property, which is intended to put a lower limit on the time within which a property can change from false to true to false again. Clearly, if either P or Q has such a lower limit, then any interval within which, at each time, either P or Q holds, is a concatenation of sub-intervals within each of which either P holds or Q holds. Law 17 gives a weaker variant of this statement. It was the most difficult of the laws to prove.

Laws 13 and 14 refer to a formula H(X) containing X but “no occurrence of negation or the complement of X”. In Appendix A of [12], Wabenhorst defines the language allowed for the construction of H( ). To check Laws 13 and 14, we would have to formalise this language in Isabelle/HOL and define its semantics.

However, in attempting to prove a related result we discovered a counterexample to Law 13. Let the predicate P be defined as δ > 0 ∧ t is rational. Then [(-P -)] = ∅ (since any non-zero interval contains rationals and irrationals), and [(-¬P -)] = [-δ = 0-]. Therefore likewise [(-◇P -)] = ∅, and so P trivially satisfies the finite variability property. Define H(X) ≡ X ⊆ S, where S is the minimal set of intervals such that the conditions (a) and (b) of Law 13 are satisfied. Then, we find that H(X) can hold only where all intervals in X are of length zero.

Now such a P hardly seems “finitely variable”, so there appears to be a problem with the definition of finite variability. Law 17, which also uses “finitely variable”, does not suffer from this problem because the requirement “α, ω and δ are not free in P ” prevents us from using such a P as a counterexample.

Laws 15 and 16 were easy. However Law 18 was difficult: formalising the proof revealed that the cases when r = 0 and r < 0, which each require separate treatment, were overlooked in the informal proof given in the appendix of [12].

3 Conclusion and Further Work

We have demonstrated the value of formalising the Timed Interval Calculus, highlighting certain issues which need to be addressed in a formal treatment, but which were overlooked in the informal treatment. The process of formalising the TIC led to the discovery that Law 10 is incorrect as it stands, that Law 13 (and probably Law 14 likewise) is incorrect due to a problem with the definition of finite variability, that Law 13 of [4] requires stronger assumptions, and that the proof of Law 18 required a clarification. While all other laws have been verified in Isabelle, Wabenhorst’s Laws 10, 13 and probably 14, require revision and present a danger to those who might use them blindly.

We are currently formalising the cases in Law 10 where S and T are of different forms (see § 2.1). We also need to fix the definition of “finite variability”, formalise, in Isabelle, the language for expressing H(X), and then check Wabenhorst’s Laws 13 and 14 in Isabelle.

An interesting open question is that of completeness: is every statement true of intervals provable using (a superset of) the laws ? This does not appear to have been investigated, and might be a considerable endeavour.

References

1. J F Allen. Towards a theory of action and time. Artif. Intel. 23:123–154, 1984.

2. A Cerone. Axiomatisation of an Interval Calculus for Theorem Proving. In C J Fidge (Ed), CATS’00: Elect. Notes in Theor. Comp. Sci. 42, Elsevier 2001.

3. A Church. A formulation of the simple theory of types. JSL, 5:56–68, 1940.

4. C J Fidge, I J Hayes, A P Martin, A K Wabenhorst, A Set-Theoretic Model for Real-Time Specification and Reasoning. In J Jeuring (Ed), Proc. MPC’98, LNCS 1422:188–206, Springer, 1998.

5. R I Goldblatt, Logics of Time and Computation, CSLI Lecture Notes Number 7, Center for the Study of Language and Information, Stanford, 1987.

6. S T Heilmann, Proof Support for Duration Calculus, PhD thesis, Dept. of Inf. Tech., Tech. Univ. of Denmark, Jan. 1999. See http://www.sth.dk/sth/.

7. M J C Gordon and T F Melham. Introduction to HOL: a Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.

8. L C Paulson. The Isabelle Reference Manual. Comp. Lab., Univ. of Cambridge,

1999. See http://www.cl.cam.ac.uk/Research/HVG/Isabelle/docs.html

9. L C Paulson. Isabelle’s Logics. Computer Lab. Univ. of Cambridge, 1999. See

http://www.cl.cam.ac.uk/Research/HVG/Isabelle/docs.html

10. B P Mahony and C Millerchip and I J Hayes. A boiler control system: A case study in timed refinement. International Invitational Workshop - Design and Review of Software Controlled Safety-Related Systems, Ottawa, June, 1993.

11. J Skakkebæk, A verification assistant for a real-time logic, PhD thesis, TR 150, Dept. of Computer Science, Technical University of Denmark, 1994.

12. A Wabenhorst. Induction in the Timed Interval Calculus. Technical Report 99-36, SVRC, University of Queensland, 1999.

13. M R Hansen and Z Chaochen. Duration calculus, logical foundations. Formal Aspects of Computing, 9 (1997), 283–303.