Machine-checking the Timed Interval Calculus

Jeremy Dawson & Rajeev Goré Automated Reasoning Group and

Dept. of Computer Science Australian National University

Canberra, Australia

jeremy@csl.anu.edu.au   rpg@csl.anu.edu.au

Dawson supported by an ARC Large Grant Goré supported by an ARC QEII Fellowship

Machine-checking TIC - overview

TIC — for reasoning about sets of intervals Many laws provided, complex to prove Isabelle — can machine-check proofs We tried to verify the laws of TIC Errors discovered through inability to formalize laws or to complete proofs Corrected in latest version of TIC TR

Reasoning about time

Reasoning about times/durations of events is a complex and specialized field

For example in Interval Algebra (Allen, 1983) 13 possibilities for the relative configuration of two intervals. Extended to 25 by considering relative duration of two intervals, in IN DU (Pujari et al, 1999).

Therefore, special calculi developed to reason about them

Reasoning Logically or Explicitly

Calculi can be logical or explicit

eg PLTL, with defined semantics and rules, soundness and completeness shown

eg Interval Algebra, algebra for reasoning about relative configuration of intervals

Logical approach — soundness and completeness (relative to semantics) by metalogic proof

Explicit approach — proved correct using properties of reals (for TIC, we used density and completeness of reals), no proof of completeness

The Timed Interval Calculus

Developed by Fidge et al, following Millerchip et al. Sets of finite, non-empty intervals, distinguishing open and closed endpoints. Variables as timed traces, defined everywhere, but references to time avoided. Laws for reasoning given by Fidge et al, and by Wabenhorst Some laws quite complex

Isabelle/HOL

Isabelle – a proof framework, natural deduction style eg from current subgoal, get new subgoal

\frac{P ∧ Q}{R}  \frac{P Q}{R}

on the screen

P & Q ==> R     [| P ; Q |] ==> R

Also has unification and term-rewriting Higher-order logic (HOL) Uses Isabelle’s strong polymorphic typing Typical FP constructs such as datatype

TIC — Interval sets

Time domain 𝕋 — we use the reals ℝ Let P be a predicate, let α and ω denote the start-point and end-point of intervals. (-P -] (left-open-and-right-closed intervals)

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

∀I ∈ (-P -], ∀x ∈ I, x “satisfies” P. Note that P may also depend on the endpoints α and ω of the interval, or its length δ = ω − α. Some laws require P independent of α, ω, δ (“α, ω and δ do not occur free in P ”)

TIC — Interval sets ctd

(-P -), [-P -), [-P -] are defined similarly eg (-P -) is set of left-and-right-open intervals For [-P -], non-emptiness condition is α ≤ ω. The right-open intervals [(-P -) are defined by [(-P -) ≡ [-P -) ∪ (-P -) [(-P -], (-P -)], [-P -)], [(-P -)] defined likewise.

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 = ∅.

for sets X and Y of intervals, their concatenation X; Y is obtained by joining x ∈ X with y ∈ Y wherever possible.

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.

The modalities ◇ and □

[(-◇P -)] — set of intervals within which P holds somewhere. Complicated by P depending on endpoints. So definition requires P on a subinterval [(-◇P -)] ≡ ([(-true -)]; [(-P -)]; [(-true -)]∪

[(-true -)]; [(-P -)] ∪ [(-P -)]; [(-true -)] ∪ [(-P -)]) [(-□P -)] ≡ 𝕀 \ [(-◇P -)], need not equal [(-P -)]. Equality if α, ω and δ do not occur free in P.

Verification Overview

Used Isabelle theory HOL + Real (theory Real develops ℝ from first principles, and contains lots of lemmas) Formalised TIC definitions in terms of ℝ Tried to prove all the TIC laws Lots of tedious machinery needed — simple definitions, tedious proofs (case for powerful calculus)

Verification — Machinery

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

datatype bndty (“bound and type”) to indicate value of endpoint and whether open or closed functions ubt (“upper bound, type”) and lbt

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

function setof gives the actual set which an

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

Negation Rules

Further functions negint, which negates an interval, negbt, which negates a bound btopp which turns an Open bound into a Closed one, and vice versa

negint_OC = "negint (OC ?beg ?end) =
   CO (- ?end) (- ?beg)" : thm
negbt_Open = "negbt (Open ?x) = Open (- ?x)"
btopp_Closed = "btopp (Closed ?x) = Open ?x"

Saves redoing proofs, for example

neg_cat = "negint ` (?S ;; ?T) =
  negint ` ?T ;; negint ` ?S" : thm
law7f = "(?S ;; ?T) ;; ?U <= ?S ;; (?T ;; ?U)"

Upper/Lower Bound Conditions

For t ∈ (α … ω], t must satisfy α < t and t ≤ ω. These conditions are the “lower (upper) bound condition”, ubc and lbc

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

Lemma 1 (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 ?I) =
   (lbc (lbt ?I) ?x & ubc (ubt ?I) ?x)" : thm

Such conditions can be related by “lifted” implication --->, which provides a reflexive and anti-symmetric ordering.

liftimp =
  "?p ---> ?q == ALL s. ?p s --> ?q s" : thm

Bound Conditions (2)

Lemma 2 (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"

Bound Conditions (3)

Lemma 3 (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)"
ubc_neg = "ubc (negbt ?b) ?x = lbc ?b (- ?x)"

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

Some Non-Trivial Results

Lemma 4 (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 ?I Int setof ?J = {}) =
((ALL s:setof ?I. ALL t:setof ?J. s < t) |
(ALL s:setof ?I. ALL t:setof ?J. t < s))"

Concatenation

Proofs were considerably more difficult

We defined a predicate abuts to indicate that two intervals meet exactly, so that they may be joined. We proved other characterisations.

Lemma 5 (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.

Concatenation — characterization

define concatenation (of sets of intervals) by

cat_def = "?X ;; ?Y == {I.  EX x:?X.  EX y:?Y.
   setof I = setof x Un setof y &
     (ALL a:setof x. ALL b: setof y. a < b)}" : thm

Associativity difficult to prove. First attempt

used abuts_un_disj. Subsequently used abuts_bnds
and single_cat'.

Lemma 6 (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.

Law 10 (Wabenhorst)

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.

What does “not free in S and T ” mean?

We have proved it when S and T are of the form (eg) [(-P -], [(-Q-], and α ,ω and δ are not free in P.

Also proved a more complicated law, involving conditions on S and T.

Law restated in Version 1.2 of Wabenhorst.

Law 13 (Fidge et al)

Law 13 (Fidge et al) (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-)]

Not true as it stands (if, say, s = 0, then all intervals of length s 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.

Laws 13 & 14 (Wabenhorst)

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. …

Appendix A of 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.

Tried to prove a related result but discovered a counterexample, based on a predicate P satisfying the finite variability property, but hardly “finitely variable”.

Finite variability property

Predicate P has the finite variability property if there exists a duration ξ > 0 such that

[(-¬P -)]; [(-◇P -)]; [(-¬P -)] ⊆ [(-δ >= ξ-)]

Define P as (δ > 0 ∧ t is rational). Then [(-P -)] = ∅ (as a non-zero interval contains rationals and irrationals), [(-¬P -)] = [-δ = 0-].

Therefore likewise [(-◇P -)] = ∅, and so P trivially satisfies the finite variability property.

Is this P really “finitely variable”?

Version 1.2 (Sept 2002) of Wabenhorst contains a different definition.

Conclusion

Verification effort worthwhile — several errors found. Errors discovered only in formalisation or proof (overlooked in careful reading). Real number proofs difficult, even with preproved lemmata (about [least] upper bounds, completeness and density of reals) Isabelle/HOL arith_tac useful, up to a point. Interval reasoning needs special purpose calculus