\documentclass{slides}

\usepackage{amsmath}
\usepackage{latexsym}
\usepackage{amssymb}
% \usepackage{exptrees}

\newenvironment{heading}{\noindent\centering\large\bf}{\par}
\newenvironment{Heading}{\noindent\centering\Large\bf}{\par}
\newtheorem{thm}{Theorem}%[chapter]
\newtheorem{lemma}[thm]{Lemma}
\newtheorem{defn}[thm]{Definition}
\newtheorem{cor}{Corollary}[thm]


\newcommand\true{\textit{true}}
\newcommand\false{\textit{false}}
\newcommand\1{\textbf{1}}
\newcommand\II{\mathbb{I}}
\newcommand\BB[1]{[(\mbox{-}#1\mbox{-})]}
\newcommand\BC[1]{[(\mbox{-}#1\mbox{-}]}
\newcommand\CB[1]{[\mbox{-}#1\mbox{-})]}
\newcommand\BO[1]{[(\mbox{-}#1\mbox{-})}
\newcommand\OB[1]{(\mbox{-}#1\mbox{-})]}
\newcommand\CC[1]{[\mbox{-}#1\mbox{-}]}
\newcommand\CO[1]{[\mbox{-}#1\mbox{-})}
\newcommand\OC[1]{(\mbox{-}#1\mbox{-}]}
\newcommand\OO[1]{(\mbox{-}#1\mbox{-})}

\newcommand\comment[1]{}

\begin{document}

\begin{slide}
  \begin{Heading}
  {Machine-checking the Timed Interval Calculus}
  \end{Heading}

\begin{center}
\begin{tabular}{c}
\normalsize Jeremy Dawson \& Rajeev Gor\'e \\
\mbox{} \\
{Automated Reasoning Group and} \\
{Dept.\ of Computer Science} \\
{Australian National University} \\
{Canberra, Australia} \\
\mbox{} \\
{\tt jeremy@csl.anu.edu.au} \quad
{\tt rpg@csl.anu.edu.au} \\
\end{tabular}

Dawson supported by an ARC Large Grant \\
Gor\'e supported by an ARC QEII Fellowship

\end{center}
\end{slide}

\begin{slide}
\begin{heading}
Machine-checking TIC - overview
\end{heading}

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

\end{slide}

\begin{slide}
  \begin{heading}
  Reasoning about time
  \end{heading}

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 $\mathcal{INDU}$ (Pujari et al, 1999).

Therefore, special calculi developed to reason about them
\end{slide}

\begin{slide}
\begin{heading}
Reasoning Logically or Explicitly
\end{heading}

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 

\end{slide}

\begin{slide}
\begin{heading}
The Timed Interval Calculus
\end{heading}

Developed by Fidge et al,
following Millerchip et al.

Sets of \emph{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
\end{slide}

\begin{slide}
\begin{heading}
Isabelle/HOL
\end{heading}

Isabelle -- a proof framework, natural deduction style

eg from current subgoal, get new subgoal
$$\frac {P \land Q} R \qquad \frac {P \quad Q} R$$

on the screen \\
\texttt{P \& Q ==> R} \qquad \texttt{[| P ; Q |] ==> R} 

Also has unification and term-rewriting

Higher-order logic (HOL)

Uses Isabelle's strong polymorphic typing

Typical FP constructs such as \texttt{datatype}

\end{slide}

\begin{slide}
\begin{heading}
TIC --- Interval sets 
\end{heading}

Time domain $\mathbb T$ --- we use the reals $\mathbb R$


Let $P$ be a predicate, let $\alpha$ and $\omega$ 
denote the start-point and end-point of intervals.

$\OC P$ (\emph{left-open-and-right-closed} intervals)
\begin{eqnarray*}
\OC P & \equiv & \{(\alpha \ldots \omega] \, | \;
\alpha, \omega : \mathbb T \,\land\, \alpha < \omega \,\land\, \\
 & & \forall t \in (\alpha \ldots \omega] P (t, \alpha, \omega)\} 
\end{eqnarray*}

$\forall I \in \OC P$, $\forall x \in I$, $x$ ``satisfies'' $P$.
Note that $P$ may also depend on the endpoints $\alpha$ and $\omega$
of the interval, or its length $\delta = \omega - \alpha$.

Some laws require $P$ independent of $\alpha$, $\omega$, $\delta$ \\
(``$\alpha$, $\omega$ and $\delta$ do not occur free in $P$'')
\end{slide}

\begin{slide}
\begin{heading}
TIC --- Interval sets ctd
\end{heading}

$\OO P$, $\CO P$, $\CC P$ are defined similarly

eg $\OO P$ is set of \emph{left-and-right-open} intervals

For $\CC P$, non-emptiness condition is $\alpha \leq \omega$.

The \emph{right-open} intervals $\BO P$ are defined by $\BO
P \equiv \CO P \cup \OO P$

$\BC P$, $\OB P$, $\CB P$, $\BB P$ defined likewise.

\end{slide}

\begin{slide}
\begin{heading}
Concatenation of sets of intervals
\end{heading}

Two intervals $x$ and $y$ can be joined if they meet with no overlap
or gap, that is, $x \cup y$ is an interval and $x \cap y = \emptyset$.

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

\begin{eqnarray*}
X ; Y & \equiv & \{x \cup y \, | \, x \in X \,\land\, y \in Y \,\land\, 
  x \cup y \in \mathbb I \,\land\, \\
  & & \forall t_1 \in x\ \forall t_2 \in y\ t_1 < t_2\}
\end{eqnarray*}

Exceptionally, \1 is used for $\{\emptyset\}$, which may be an operand
for, and is an identity of, the concatenation operator.

\end{slide}

\begin{slide}
\begin{heading}
The modalities $\Diamond$ and $\Box$
\end{heading}
$\BB {\Diamond P}$ --- set of intervals within which $P$ holds somewhere.

Complicated by $P$ depending on endpoints.

So definition requires $P$ on a subinterval
% which may be at the left- and/or right-hand end of the
% interval, or both, or neither. 
\begin{eqnarray*}
\lefteqn{ \BB {\Diamond P} \equiv 
(\BB \true ; \BB P ; \BB \true \cup }
 \\ & & \BB \true ; \BB P \cup \BB P ; \BB \true \cup \BB P )
\end{eqnarray*}

$\BB {\Box P} \equiv \mathbb I \setminus \BB {\Diamond P}$, 
need not equal $\BB P$.
Equality if $\alpha$, $\omega$ and $\delta$ do not occur free in $P$.

\end{slide}

\begin{slide}
\begin{heading}
Verification Overview
\end{heading}

Used Isabelle theory HOL + Real
(theory Real develops $\mathbb R$ from first principles,
and contains \emph{lots} of lemmas)

Formalised TIC definitions in terms of $\mathbb R$

Tried to prove all the TIC laws

Lots of tedious machinery needed ---
simple definitions, tedious proofs
(case for powerful calculus)

\end{slide}

\begin{slide}
\begin{heading}
Verification --- Machinery
\end{heading}

\begin{verbatim}
datatype interval = CC real real | CO real real 
                  | OC real real | OO real real
\end{verbatim}

datatype \verb|bndty| (``bound and type'')
to indicate value of endpoint and whether open or closed 

functions \verb|ubt| (``upper bound, type'') and \verb|lbt|

\begin{verbatim}
datatype bndty = Closed real | Open real
ubt_CC = "ubt (CC ?beg ?end) = Closed ?end" 
\end{verbatim}

function \texttt{setof} gives the actual set which an
\texttt{interval} defines:
\begin{verbatim}
setof_OC = "setof (OC ?beg ?end) =
            {x.?beg < x & x <= ?end}" : thm
\end{verbatim}

\end{slide}

\comment{
\begin{slide}
\begin{heading}
Verification --- Machinery (2)
\end{heading}

\begin{lemma}
\begin{enumerate}
\renewcommand\theenumi{(\roman{enumi})}
\renewcommand\labelenumi\theenumi
\item On non-empty intervals, the function \texttt{setof} is 1-1.
\item The upper and lower bounds of an interval (including their types,
ie, \texttt{Closed} or \texttt{Open}) determine the interval.
\end{enumerate}
\end{lemma}
\begin{verbatim}
setof_cong = "[| nonempty ?int1; 
    setof ?int1 = setof ?int2 |] ==> 
  ?int1 = ?int2" : thm
bts_unique = "[| lbt ?int1 = lbt ?int2; 
  ubt ?int1 = ubt ?int2 |] ==> ?int1 = ?int2" 
\end{verbatim}

\end{slide}
}

\begin{slide}
\begin{heading}
Negation Rules
\end{heading}

Further functions  \\
\indent \verb|negint|, which negates an interval, \\
\indent \verb|negbt|, which negates a bound \\
\indent \verb|btopp| which turns an
\texttt{Open} bound into a \texttt{Closed} one, and vice versa

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

Saves redoing proofs, for example

\begin{verbatim}
neg_cat = "negint ` (?S ;; ?T) = 
  negint ` ?T ;; negint ` ?S" : thm
law7f = "(?S ;; ?T) ;; ?U <= ?S ;; (?T ;; ?U)" 
\end{verbatim}


\end{slide}

\begin{slide}
\begin{heading}
Upper/Lower Bound Conditions
\end{heading}

For $t \in (\alpha \ldots \omega]$, 
$t$ must satisfy $\alpha < t$ and $t \leq \omega$. 
These conditions are the ``{l}ower ({u}pper)
{b}ound {c}ondition'',
\verb|ubc| and \verb|lbc|

\begin{verbatim}
ubc_Closed =
   "ubc (Closed ?end) ?x = (?x <= ?end)" : thm
\end{verbatim}

\begin{lemma}[\texttt{bnd\_conds}]
A point lies in an interval if and only if it satisfies the
lower and upper bound conditions for the interval.
\end{lemma}
\begin{verbatim}
bnd_conds = "(?x : setof ?I) =
   (lbc (lbt ?I) ?x & ubc (ubt ?I) ?x)" : thm
\end{verbatim}

Such conditions can be related by
``lifted'' implication \verb|--->|, which provides a
reflexive and anti-symmetric ordering.
\begin{verbatim}
liftimp = 
  "?p ---> ?q == ALL s. ?p s --> ?q s" : thm
\end{verbatim}

\end{slide}

\comment{}
\begin{slide}
\begin{heading}
Bound Conditions (2)
\end{heading}

\begin{lemma}
\begin{description}
\item[(\texttt{ubc\_cong})] The function \texttt{ubc} is 1-1.
\item[(\texttt{ubc\_linear})]
The relation \verb|--->| is linear on conditions of the form \texttt{ubc} $s$.
\item[(\texttt{ubc\_rel})] If $x$ satisfies the upper bound condition for an
interval, and $y \leq x$, then $y$ satisfies the upper bound condition for the
interval.
\end{description}
\end{lemma}
\begin{verbatim}
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" 
\end{verbatim}

\end{slide}

\begin{slide}
\begin{heading}
Bound Conditions (3)
\end{heading}

\begin{lemma}
\begin{description}
\item[(\texttt{ubc\_opp})]
Let $b$ be a bound, and $b'$ its opposite (ie,
\verb|Open| instead of \verb|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$.
\item[(\texttt{ubc\_neg})]
Let $b$ be a bound, and $b'$ its negation (eg,
if $b$ is \verb|Open| $z$ then $b'$ is \verb|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$.
\end{description}
\end{lemma}
\begin{verbatim}
ubc_opp = "ubc (btopp ?b) ?x = (~ lbc ?b ?x)" 
ubc_neg = "ubc (negbt ?b) ?x = lbc ?b (- ?x)" 
\end{verbatim}

Results using properties of real numbers often required many easy
lemmata and a proof by cases: e.g.\ \mbox{\texttt{ubc x ---> ubc y}}
has four cases of which one is:
\begin{verbatim}
"(ubc (Closed ?x) ---> ubc (Open ?y)) = 
  (?x < ?y)" : thm
\end{verbatim}

\end{slide}


\begin{slide}
\begin{heading}
Some Non-Trivial Results
\end{heading}

\begin{lemma}
\begin{description}
\item[(\texttt{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 \in S$ and any $z$, if $x \leq z \leq y$ then $z \in S$.
\item[(\texttt{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.
\end{description}
\end{lemma}
\begin{verbatim}
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))" 
\end{verbatim}
\end{slide}

\begin{slide}
\begin{heading}
Concatenation
\end{heading}

Proofs were considerably more difficult

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

\begin{lemma}
\begin{description}
\item[(\texttt{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.
\item[(\texttt{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$.
\item[(\texttt{abuts\_betw\_char})]
If $A$ and $B$ are intervals, and $a \in A, b \in B$, then
$A$ and $B$ abut iff for any $c$ such that $a \leq c \leq b$,
$c$ is in exactly one of $A$ and $B$.
% \item[(\texttt{abuts\_UnL})]
% If $A, B, C$ are sets, $b \in B$ and $\forall a \in A. a \leq b$
% then $B$ and $C$ abut iff $(A \cup B)$ and $C$ abut.
\end{description}
\end{lemma}
\comment{
  \begin{verbatim}
  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
  \end{verbatim}
  }

\end{slide}

\begin{slide}
\begin{heading}
Concatenation --- characterization
\end{heading}

define concatenation (of \emph{sets} of intervals) by
\begin{verbatim}
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
\end{verbatim}

\comment {
We prove an alternative characterisation \verb|cat_abuts|.
\begin{lemma}
\begin{description}
\item [(\texttt{mem\_cat\_UN})]
$x \in A ; B$ if and only if there exist $a \in A, b \in B$
such that $x \in \{a\} ; \{b\}$.
\item [(\texttt{cat\_abuts})] $x \in \{a\} ; \{b\}$ if and only if $a
  \cup b$ is an interval and, if $a$ and $b$ are non-empty, they abut.
\end{description}
\end{lemma}
\begin{verbatim}
mem_cat_UN =
  "(?x : ?A;;?B) = (EX a:?A. EX b:?B. ?x : {a};;{b})" : thm
cat_abuts = "?A ;; ?B = {I.  EX a:?A.  EX b:?B.
  setof I = setof a Un setof b &
  (nonempty a & nonempty b --> abuts (setof a) (setof b))}" : thm
\end{verbatim}
}

Associativity difficult to prove.
First attempt used \verb|abuts_un_disj|.
Subsequently used \verb|abuts_bnds| and \verb|single_cat'|.

\begin{lemma}
\begin{description}
\item[(\texttt{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$.
\item[(\texttt{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.
\end{description}
\end{lemma}

\end{slide}

\begin{slide}
\begin{heading}
Law 10 (Wabenhorst)
\end{heading}

Law 10 (Concatenate intersection)

$(S \cap T) ; U \subseteq (S ; U) \cap (T ; U)$ and \\
$U ; (S \cap T) \subseteq (U ; S) \cap (U ; T)$  \\
Equality holds in the first case
if $\omega$ and $\delta$ are not free in $S$ and $T$, 
and in the second case
if $\alpha$ and $\delta$ 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) $\BC{P}$, $\BC{Q}$,
and $\alpha$ ,$\omega$ and $\delta$ 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.
\end{slide}

\begin{slide}
\begin{heading}
Law 13 (Fidge et al)
\end{heading}
Law 13 (Fidge et al) (Concatenate duration)

If $\alpha$, $\omega$ and $\delta$ are not free in $P$, \\
$r \geq 0$ and $s \geq 0$, where $r > 0$ or $s > 0$, then \\
\mbox{
$\BB {P \land \delta = r + s} =
  \BB {P \land \delta = r} ; \BB {P \land \delta = s}$}

Not true as it stands 
(if,
say, $s = 0$, then all intervals of length $s$ are 
closed at both ends, and yet $\BB {P \land \delta = 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$.

\end{slide}

\begin{slide}
\begin{heading}
Laws 13 \& 14 (Wabenhorst)
\end{heading}

Law 13 (Induction on Lengths)

Let $H(X)$ be a formula
containing $X : \mathbb{P I} \cup \1$, but no occurrence of
negation or the complement of $X$. 
Let $P$ be a predicate for which
  the finite variability property holds. \ldots

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
% (so that a formula would become an abstract syntax tree)
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''.
\end{slide}

\begin{slide}
\begin{heading}
Finite variability property
\end{heading}
Predicate $P$ has the \emph{finite variability property}
if there exists a duration $\xi > 0$ such that
$$\BB {\lnot P} ; \BB {\Diamond P} ; \BB {\lnot P} \subseteq
  \BB {\delta >= \xi}$$

% \end{slide}
% 
% \begin{slide}
% \begin{heading}
% Problem with the finite variability property
% \end{heading}
Define $P$ as
($\delta > 0 \ \land \ t $ is rational).
Then $\BB{P} = \emptyset$ (as a non-zero interval contains
rationals and irrationals),
$\BB{\lnot P} = \CC{\delta = 0}$.

Therefore likewise $\BB {\Diamond P} = \emptyset$,
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.

\end{slide}

\begin{slide}
\begin{heading}
Conclusion 
\end{heading}

\textbf{Verification effort worthwhile} --- several errors found.

Errors discovered only in formalisation or proof 
(overlooked in careful reading).

Real number proofs difficult, even with pre-proved lemmata
(about [least] upper bounds, completeness and density of reals)

Isabelle/HOL \verb|arith_tac| useful, up to a point.

Interval reasoning needs special purpose calculus

\end{slide}

\end{document}