%%
%%
\documentclass{llncs}
%\usepackage{makeidx}
%\usepackage{acmnew-xref}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
% \usepackage{exptrees}
\usepackage{url}
%\RequirePackage{mathptm}
%\RequirePackage{times}
%\RequirePackage{palatino}
\renewcommand{\today}{\number\day\
\ifcase\month\or
January\or February\or March\or April\or May\or June\or
July\or August\or September\or October\or November\or December\fi
\ \number\year}
%\setlength \parskip {1.0ex}
\setcounter{secnumdepth}2
\setcounter{tocdepth}2
\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble
\title{Machine-checking the Timed Interval Calculus }
\author{
Jeremy E.\ Dawson
\thanks{Supported by an Australian Research Council Large Grant
}
\ \ and \ \
Rajeev Gor\'e
% \thanks{Contact Author }
\thanks{Supported by an Australian Research Council QEII Fellowship
}
}
\institute{
Department of Computer Science and
Automated Reasoning Group
\\ Australian National University,
Canberra ACT 0200, Australia
\\ \url{http://users.rsise.anu.edu.au/~jeremy/} \ \
\url{http://users.rsise.anu.edu.au/~rpg/}
%\\ Tel: +61-2-6125-8606 \ \ Fax: +61-2-6125-8651
}
\newcommand\cfile{}
%\renewcommand{\thepage}{\roman{page}}
\newcommand\shrinklist[1]{
\setlength\parskip{#1\parskip}
\setlength\itemsep{#1\itemsep}
\setlength\itemindent{#1\itemindent}
\setlength\topsep{#1\topsep}
}
\newcommand\comment[1]{}
\newcommand\invrule[2]{
% for use in non-math mode, args interpreted in math mode
\begin{tabular}{@{}c@{}}
$ #1 $ \\ \hline \hline $ #2 $
\end{tabular}}
\newcommand\slrule[2]{ % similar to \frac, except
% for use in non-math mode, args interpreted in math mode
\begin{tabular}{@{}c@{}}
$ #1 $ \\ \hline $ #2 $
\end{tabular}}
%\newcommand\proof{\noindent\textbf{Proof.}}
\newcommand\src[1]{source file \texttt{#1}}
\newcommand\apsrc[1]{Appendix \ref{app:code}}
%\newcommand\seesrc[1]{(see source file \texttt{#1}, \apsrc{#1})}
\newcommand\seesrc[1]{(see source file \texttt{#1})}
%\newcommand\insrc[1]{in source file \texttt{#1} (see \apsrc{#1})}
\newcommand\insrc[1]{in source file \texttt{#1}}
\newcommand\page[1]{page~\pageref{#1}}
\newcommand\fig[1]{Fig.~\ref{fig:#1}}
\newcommand\ch[1]{Chapter~\ref{ch:#1}}
\newcommand\tbl[1]{Table~\ref{tbl:#1}}
\newcommand\thrm[1]{Theorem~\ref{thrm:#1}}
\newcommand\lem[1]{Lemma~\ref{lem:#1}}
\newcommand\ttl[1]{\tti{#1}\label{#1}}
\newcommand\ttdl[1]{\texttt{#1}\tti{#1}\label{#1}}
\newcommand\ttdef[1]{\texttt{#1}\tti{#1}}
\newcommand\tti[1]{\index{#1@\texttt{#1}}}
\newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}}
\newcommand\up[1]{\vspace{-#1ex}}
\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree
% automatically defined in LLNCS style
%\newtheorem{thm}{Theorem}%[chapter]
%\newtheorem{lemma}[thm]{Lemma}
%\newtheorem{defn}[thm]{Definition}
%\newtheorem{cor}{Corollary}[thm]
%\renewcommand\thecor{\thethm(\arabic{cor})}
% \pagestyle{myheadings}
% \pagestyle{plain}
\pagestyle{empty}
%% Title
\maketitle
\date{\today}
\begin{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.
\\[1ex]
Keywords: reasoning about time, automated reasoning, theorem
proving}
\end{abstract}
\sloppy
%% Here begins the main text
\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\file{}
\newcommand\hinput[1]{\renewcommand\file{#1.tex}
\markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
\input{#1}}
\section{Introduction}
\label{s-intro}
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 \cite{goldblatt-logics} while a more
direct approach leads to various calculi for reasoning about time
explicitly \cite{allen-intervals,duration-calculus,fidge-tic}. 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 \cite{mahony:boilerfull}.
Following Fidge et al.~\cite{fidge-tic}, Wabenhorst
\cite{wabenhorst-induction} 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 \cite{fidge-tic} and \cite{wabenhorst-induction},
once again showing the worth of machine-checked proofs.
Various authors have already formalised another interval calculus
called the Duration Calculus \cite{duration-calculus}. Heilmann's
\cite{heilmann-thesis} proof assistant Isabelle/DC is built using
Isabelle and SVC (Stanford Validity Checker), while Skakkeb\ae k's
\cite{skakkebaek-thesis} PC/DC (Proof Checker for Duration Calculus)
is built upon PVS.
However, we know of only one other attempt to formalise the TIC. In
\cite{cerone-axiomatisation}, 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 \cite{cerone-axiomatisation}. 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 \cite{wabenhorst-induction} 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,
\cite{cerone-axiomatisation} deals with proofs of only 5 laws.
In the remainder of \S~\ref{s-intro} we introduce the TIC, Isabelle,
and Wabenhorst's laws in some detail. In \S~\ref{s-verif} we describe
our formalisation of the laws and the problems we encountered. In
\S~\ref{s-concl} we conclude. % and indicate possible further work.
% The Isabelle verifications took approximately 100 person-hours to complete.
The full code of our machine-implementation can be found at
\url{http://rsise.anu.edu.au/~jeremy/tic/tic-files/}.
% via your favourite browser.
\paragraph{Acknowledgements:} We are extremely grateful to Axel
Wabenhorst for his prompt clarifications, and to Brendan Mahony for
bibliographic pointers.
\subsection{The Timed Interval Calculus}
The Timed Interval Calculus (TIC) is introduced by Fidge et
al.~\cite{fidge-tic} 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 $\mathbb{T}$. Time intervals
are represented as all time points in $\mathbb{T}$ 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.
%The TIC itself consists of numerous rules for reasoning
%about the behaviour of digital systems using this bracket notation.
Fidge et al.~\cite{fidge-tic} give 13 laws which capture
fundamental properties of time intervals defined via the TIC notation.
In \cite{wabenhorst-induction} Wabenhorst gives 18 such laws,
including most of those in ~\cite{fidge-tic}.
The correctness of these laws is the focus of our work.
% Further details are given in \S~\ref{s-wl}.
\subsection{Isabelle/HOL}
Isabelle is an automated proof assistant \cite{isabelle-ref}.
Its meta-logic is an intuitionistic typed higher-order logic,
% and typed $\lambda$-calculus,
sufficient to support the built-in inference steps of
higher-order unification and term rewriting.
Isabelle accepts inference rules of the form
``from $\alpha_1, \alpha_2, \ldots, \alpha_n, \mbox{ infer } \beta$''
where the $\alpha_i$ and $\beta$
are expressions of the Isabelle meta-logic,
or are expressions using a new syntax, defined by the user, for some
``object logic''. % $\mathcal F$.
% An Isabelle user can encode a particular calculus
% $\mathcal C _L$ for some logic $L$ as an ``object logic'' by using
% these rule templates to encode the set of inference rules of
% $\mathcal C _L$.
% %This is supplemented with the user's choice of
% %object logic in which to perform proofs.
% For example, if $\mathcal C _L$
% is a natural deduction calculus, then
% the $\alpha_i$ and $\beta$ will be formulae of $L$,
% whereas if $\mathcal C _L$ is a sequent calculus, then
% the $\alpha_i$ and $\beta$ will be sequents of $\mathcal C _L$.
% Such an encoding is called an ``object logic'', even though it is
% a (typically natural deduction or sequent) \emph{calculus} for some
% particular logic $L$.
In practice most users would build on one of the
comprehensive ``object logics'' already supplied \cite{isabelle-object}.
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 \cite{church-types} and the HOL system of Gordon
\cite{HOL-introduction}. Thus it includes quantification and
abstraction over higher-order functions and predicates. The
\texttt{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
\texttt{datatype} and \texttt{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.
\subsection{TIC definitions and laws} \label{s-wl}
As stated previously, $\mathbb T$ is some fixed domain of time points,
typically the reals
(our proofs use the completeness and density of the reals).
The set of all non-empty finite time intervals over this domain is $\mathbb I$.
Following Fidge et al.~\cite{fidge-tic},
Wabenhorst \cite{wabenhorst-induction} defines several symbols --
the following definitions are (or are close to) his.
Suppose $P$ is some predicate, and let $\alpha$ be the start-point
and $\omega$ be the end-point of our intervals.
Let $\OC P$ be the set (of \emph{left-open-and-right-closed}
intervals)
$$\OC P \equiv \{(\alpha \ldots \omega] \, | \;
\alpha, \omega : \mathbb T \land \alpha < \omega \land
\forall t : (\alpha \ldots \omega] P (t, \alpha, \omega)\}
$$
Thus all intervals in $\OC P$ are non-empty, and for every interval
$I \in \OC P$ and every $x \in I$, $x$ satisfies $P$. Note that
predicate $P$ may also depend on the endpoints $\alpha$ and $\omega$
of the interval, whose length $\omega - \alpha$ is often abbreviated
by $\delta$.
The \emph{left-and-right-open} intervals $\OO P$, the
\emph{left-closed-and-right-open} intervals $\CO P$ and the
\emph{left-and-right-closed} intervals $\CC P$ are defined similarly,
though for $\CC P$ the 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$, and $\BC P$, $\OB P$, $\CB P$ and $\BB P$
are defined correspondingly as the \emph{right-closed},
\emph{left-open}, \emph{left-closed} and
\emph{left-and-right-open-or-closed} intervals respectively. In the
Isabelle code $\BO P$ is represented as \verb|[(-P-)|, and the others
likewise.
To reason about adjacent intervals,
Wabenhorst defines concatenation of sets of intervals.
% We simplify this slightly to give the following definition.
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$.
Then, for sets $X$ and $Y$ of intervals, their concatenation $X ; Y$
is obtained by joining $x \in X$ with $y \in Y$ wherever this is
possible. Thus
$$X ; Y \equiv \{x \cup y \, | \, x : X \land y : Y \land x \cup y :
\mathbb I \land \forall t_1 : x\ \forall t_2 : y\ t_1 < t_2\}$$
Exceptionally, \1 is used for $\{\emptyset\}$, which may be an operand
for, and is an identity of, the concatenation operator. Finally,
$\overline S$ means $S \cup \1$.
% Law 8 gives the result of concatenation with \1.
A predicate $P$ is defined to have 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}$.
% \begin{definition}[Sets of time intervals]
% \end{definition}
Wabenhorst \cite{wabenhorst-induction}
gives 18 laws for the Timed Interval Calculus,
as shown in Figure~\ref{fig-wlaws}.
Fidge et al.~\cite{fidge-tic} give 13 laws, most of which are included in
Wabenhorst's 18 laws. The remaining two are shown in Figure~\ref{fig-flaws}.
\begin{figure}
\renewcommand\theenumi{\alph{enumi}}
\renewcommand\labelenumi{(\theenumi)}
\begin{description}
\item[Law 1 (Monotonicity)]
If for all $\alpha$, $\omega$ and $\delta$ in
$\mathbb T$ and all $t : (\alpha \ldots \omega]$
\newline
$P (t, \alpha, \omega) \Rightarrow Q (t, \alpha, \omega)$,
then $\OC P \subseteq \OC Q$.
\item[Law 2 (True and false)]
$\BB \true = \mathbb I$ and
$\BB \false = \emptyset$
\item[Law 3 (And)]
$\BB P \cap \BB Q = \BB {P \land Q}$
\item[Law 4 (Or)]
$\BB P \cup \BB Q \subseteq \BB {P \lor Q}$
\item[Law 5 (Not)]
$\BB {\lnot P} \subseteq \mathbb I \backslash \BB P$
\item[Law 6 (Concatenation monotonicity)]
If $S \subseteq S'$ and $T \subseteq T'$ then $S;T \subseteq S';T'$.
\item[Law 7 (Concatenation associativity)]
(S ; T) ; U = S ; (T ; U)
\item[Law 8 (Concatenation zero and unit)]
$S ; \emptyset = \emptyset ; S = \emptyset$ and
$S ; \1 = \1 ; S = S$.
\item[Law 9 (Concat.\ union)]
$(S \cup T) ; U = (S ; U) \cup (T ; U)$ and
$S ; (T \cup U) = (S ; T) \cup (S ; U)$
\item[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$.
\item[Law 11 (Concatenate property)]
If $\alpha$, $\omega$ and $\delta$ do not occur free in $P$,
then \mbox{$\BB {P \land \delta > 0} = \BB P ; \BB P$}.
\item[Law 12 (Always)]
If $\alpha$, $\omega$ and $\delta$ are not free in $P$,
then $\BB {\Box P} = \BB P$.
\item[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. If
\begin{enumerate}
\item $H( \1 )$ and
\item $H(X) \Rightarrow H (X \cup (X ; \BB P) \cup (X ; \BB {\lnot P}))$
\end{enumerate}
then $H (\overline{\II})$.
\item[Law 14 (Induction on Histories)]
Let $H(X)$ be a formula containing $X : \mathbb {P I} $,
but no occurrence of negation or the complement of $X$.
Let $P$ be a predicate for which the finite variability property holds. If
\begin{enumerate}
\item $H(\BB {\omega < 0})$ and
\item $H(X) \Rightarrow H (X \cup (X ; \BB P) \cup (X ; \BB {\lnot P}))$
\end{enumerate}
then $H (\BB {\alpha < 0})$.
\item[Law 15 (Ignore Prefix)]
Suppose that there exists $r : \mathbb T$ such that for all
\newline
$I : \BB {\alpha < r}$, $\{I\} ; S \subseteq \{I\} ; T$.
Then $S \subseteq T$.
\item[Law 16 (Distribute Intersection)]
If $\alpha$, $\omega$ and $\delta$ are not free in $P$,
then \\ $\BB P \cap (S ; T) = (\BB P \cap S) ; (\BB P \cap T)$.
\item[Law 17 (Endpoints)]
If $\alpha$, $\omega$ and $\delta$ are not free in $P$ and $Q$,
and if $P$ or $Q$ is finitely variable, then
\\ $\BB {P \lor Q} = \overline {\BB {P \lor Q}} ; (\BB P \cup \BB Q) =
(\BB P \cup \BB Q) ; \overline {\BB {P \lor Q}}$
\item[Law 18 (Implicit Duration)]
If $\alpha$, $\omega$ and $\delta$ are not free in $P$ and $Q$,
then
\\ $\BB {P \land \delta > r} \subseteq \overline {\BB \true} ; \BB Q
\Leftrightarrow
\BB {P \land \delta > r} \subseteq \overline {\BB {\delta \leq r}} ; \BB Q$
\end{description}
\caption{Laws for the Timed Interval Calculus}
\label{fig-wlaws}
\end{figure}
\begin{figure}
\begin{description}
\item[Law 11 (Concatenate fixed intersection)]
If $r \geq 0$ then\\
\begin{tabular}{ll}
& $((S \cap \BO {\delta = r}) ; T) \cap
((U \cap \BO {\delta = r}) ; V) =
(S \cap U \cap \BO {\delta = r}) ; (T \cap V)$
\\
\& & $(S ; (U \cap \OB {\delta = r})) \cap
(T ; (V \cap \OB {\delta = r})) =
(S \cap T) ; (U \cap V \cap \OB {\delta = r})$
\end{tabular}
Similarly with $\BO\ldots$ and $\OB\ldots$ replaced
by $\BC\ldots$ and $\CB\ldots$ respectively.
\item[Law 13 (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
$\BB {P \land \delta = r + s} =
\BB {P \land \delta = r} ; \BB {P \land \delta = s}$
\end{description}
\caption{Additional Laws of Fidge et al.}
\label{fig-flaws}
\end{figure}
A common special case for $\BB P$ (etc) is where
predicate $P$ takes a single argument,
and does not involve the endpoints of the interval:
%This is relevant in several laws, such as Law~11,
%and is
the latter is expressed by the condition
``if $\alpha$, $\omega$ and $\delta$ do not occur free in $P$''
(e.g.\ Law~11).
% However in commencing to formalise the laws we noticed that a similar
% phrase occurs in Law~10 in respect of arbitrary sets of intervals ($S,
% T, U$). We saw this as either meaningless or erroneous, and
% Wabenhorst has indicated (by email) that the part of the law giving a
% condition for equality should be limited to the case when $S$ and $T$
% have a form such as $\CC P$ or $\OO P$.\marginpar{\bf Axel!}
% % Details are discussed in \S~\ref{sec:concatenation}.
% See \S~\ref{sec:concatenation}.
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 $\CC P$ or $\OO P$ --- see
\S~\ref{sec:concatenation}.
%\marginpar{\bf Axel!}
\section{Verification of the laws}
\label{s-verif}
As can be seen from Figure~\ref{fig-wlaws},
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
$\mathbb T$, which is stated to be the real numbers $\mathbb R$.
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.
% We needed to prove a considerable number of lemmata, some with many cases.
The datatype \texttt{interval}, defined below, uses the two endpoints
of the interval, and an indicator of whether the interval is closed or
open at these endpoints:
\begin{verbatim}
datatype interval =
CC real real | CO real real | OC real real | OO real real
\end{verbatim}
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 $\mathbb I$, written in Isabelle as \verb|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~\ref{fig:various-functions}. 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 \verb|bndty| to
take a real bound and indicate whether an interval is open or closed
at that bound, and functions \verb|ubt| (``upper bound and type'') and
\verb|lbt|, for example:
\begin{verbatim}
datatype bndty = Closed real | Open real
ubt_CC = "ubt (CC ?beg ?end) = Closed ?end" : thm
\end{verbatim}
\begin{figure}[t]
\centering
\begin{verbatim}
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)
\end{verbatim}
\caption{Various Functions for Reasoning About Intervals}
\label{fig:various-functions}
\end{figure}
%\newpage
The 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}
\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" : thm
\end{verbatim}
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 \verb|negint|, which negates an interval,
and a function \verb|negbt|, which negates a bound, by, for example:
\begin{verbatim}
negint_O = "negint (OC ?beg ?end) = CO (- ?end) (- ?beg)" : thm
negbt_Open = "negbt (Open ?x) = Open (- ?x)" : thm
\end{verbatim}
Thus we have lemmata such as the following.
\begin{lemma}
The upper bound of the negation of $A$ is the negation of the lower bound of
$A$. \verb| ubt_neg = "ubt (negint ?A) = negbt (lbt ?A)" : thm|
\end{lemma}
In discussing concatenation of intervals, we are interested in pairs
$(A, B)$ of intervals such that (for example) $ \texttt{ubt}\ A =
\texttt{Closed}\ r$ and $ \texttt{lbt}\ B = \texttt{Open}\ r$ since
such intervals meet with no overlap or gap at $r$. We
therefore defined a function \verb|btopp| which ``\texttt{opp}oses" an
\texttt{Open} bound into a \texttt{Closed} one, and vice versa.
\begin{verbatim}
btopp_Closed = "btopp (Closed ?x) = Open ?x" : thm
\end{verbatim}
For a point $t$ to lie within an interval like $(\alpha \ldots
\omega]$, it must satisfy $\alpha < t$ and $t \leq \omega$. We refer
to these two conditions as the ``\texttt{l}ower (\texttt{u}pper)
\texttt{b}ound \texttt{c}ondition''. 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 \verb|ubc| and \verb|lbc| (one clause of the definition is
given below), and proved the lemma \verb|bnd_conds|.
\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 ?intvl) =
(lbc (lbt ?intvl) ?x & ubc (ubt ?intvl) ?x)" : thm
\end{verbatim}
We then needed facilities to manipulation these
conditions.
Firstly a ``lifted'' implication \verb|--->|, which provides a
reflexive and anti-symmetric ordering.
\begin{verbatim}
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
\end{verbatim}
Relation \verb|--->| is also transitive, but we do not use this.
It is not generally linear,
but the result \verb|ubc_linear|
and the others shown below were useful.
%Some other useful results are also shown.
\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" : thm
\end{verbatim}
Several
%more trivial but convenient
results related these functions
to ones previously described, e.g.:
\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)" : thm
ubc_neg = "ubc (negbt ?b) ?x = lbc ?b (- ?x)" : thm
\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}
We now
%proceed to the
give
results which, though in some cases intuitively
quite simple, were more difficult to prove
%. This seemed to be
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 \verb|betw_char|,
which was quite difficult to prove, gives a characterisation of finite
intervals. The result \verb|disj_alt| is related to the manner in
which concatenation is defined.
\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 ?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
\end{verbatim}
\subsection{Concatenation}
\label{sec:concatenation}
Proving results about concatenation of interval sets was considerably
more difficult. We defined a predicate \verb|abuts| to indicate that
two intervals meet exactly, so that they may be joined. The
definition is \verb|abuts_def|, but we found that some other
characterisations of \verb|abuts| were more useful. Note that
\texttt{?S *<= ?x} means $\forall y \in S. y \leq x$. Proving these
results was surprisingly tedious and difficult.
\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}
\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}
Here \texttt{Un} is the set union operation in Isabelle/HOL,
while \texttt{Int} (used later) is the set intersection operation.
We use ``\verb|;;|'' to stand for the TIC concatenation operator
``;'', and define concatenation (of \emph{sets} of intervals) by
\begin{verbatim}
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
\end{verbatim}
We prove an alternative characterisation \verb|cat_abuts|.
The easy lemma \verb|mem_cat_UN| relates $\{a\} ;; \{b\}$ to $A ;; B$
where $A$ and $B$ are sets of intervals and $a$ and $b$ are intervals.
\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 = {intvl. EX a:?A. EX b:?B.
setof intvl = setof a Un setof b &
(nonempty a & nonempty b --> abuts (setof a) (setof b))}" : thm
\end{verbatim}
The proof of Law 7 (Concatenate associativity) turned out to be
more difficult than most of the others.
Our first proof was achieved using
\verb|cat_abuts|, \verb|abuts_un_disj|,
\verb|abuts_UnL|, and a corresponding result \verb|abuts_UnR|.
Subsequently we found an easier approach. We used \verb|abuts_bnds| to
characterise when two intervals can be joined, and \verb|single_cat'|
to describe the result of joining them. It was straightforward but
tedious to then prove \verb|single_cat3l'|, and the similar result
\verb|single_cat3r'|, differing only in containing
\verb|(?x :{?A} ;;({?B} ;; {?C}))|.
Proving Law 7 was then straightforward.
\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}
\begin{verbatim}
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
\end{verbatim}
% As mentioned above, Law~10 as stated was erroneous, but we did not
% find the error via our actual formalisation. We felt that the
% ``$\subseteq$'' parts were correct, but that the statement ``Equality
% holds \ldots'' is either not meaningful or incorrect. When we emailed
% him for clarification, Wabenhorst stated that ``As the law is stated,
% $S$ and $T$ are arbitrary sets of intervals \ldots''. But he also gave
% a counter-example to show that, even on this understanding, the law is
% incorrect: let $S = \{[1 \ldots 2]\}$, $T = \{[1 \ldots 3]\}$, $U =
% \BB \true$. He suggested that the sentence about equality be
% restricted to cases where $S$ and $T$ are of the form $\OC P$, etc.
% \marginpar{\bf Axel!}
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 ``$\subseteq$'' parts were correct, but that the
statement ``Equality holds \ldots if $\omega$ and $\delta$ are not
free in $S$ and $T$ '' is not meaningful. References to $\omega$ and
$\delta$ makes sense only in the context of a function $P$ (of $t$,
$\alpha$, and $\omega$), which arises when the forms of $S$ and $T$
are drawn from $\BB{.}, \BC{.}, \BO{.}, \CB{.}, \CC{.}, \CO{.},
\OB{.}, \OC{.}$, and $\OO{.}$.
We have therefore proved a version of Law~10 where both $S$ and $T$
are of the \textit{same} form, and that form is one of $\BB{.},
\BC{.}, \BO{.}, \CB{.}, \CC{.}, \CO{.}, \OB{.}, \OC{.}$, and $\OO{.}$.
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 $\alpha$, $\delta$ and
$\omega$ altogether, but letting $S = \{[1 \ldots 2]\}$, $T = \{[1
\ldots 3]\}$, $U = \BB \true$ gives a counter-example to this version
of Law~10.
%\marginpar{\bf Axel!}
Finally, we also tried to replace Law~10 by a more complex law. We
defined a predicate \verb|clp| of a set of intervals (``Closed under
taking Left Part'') to mean that for $x \in S$, if $y$ is a non-empty
interval which has the same left endpoint but a lower right endpoint,
then $y \in 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:
%
\begin{verbatim}
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
\end{verbatim}
%
But condition \texttt{clp} is too strong: $\BB P$ satisfies
it, but $\BC P$ and $\BO P$ do not.
Law~11 was formulated as follows. It uses \verb|no_aod| whose
argument is a predicate $P$ which depends only on $t$, not on $\alpha$
or $\omega$. The \verb|%| symbol is Isabelle's notation for
the function abstraction operator $\lambda$.
\begin{verbatim}
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
\end{verbatim}
%It was proved using case analysis,
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).
% \subsection{Additional laws of Fidge et al.}
% As noted earlier, Fidge et al.~\cite{fidge-tic} gave 13 laws, of which
% most are contained in Wabenhorst's 18 laws.
We also considered Laws 11 and 13 of \cite{fidge-tic} (see
Figure~\ref{fig-flaws}), 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$ \emph{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 $\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$.
\subsection{The modality $\Box$}
The modality $\Diamond$ is used to express the notion of a property
holding somewhere within an interval, and $\BB {\Diamond 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 $\BB {\Diamond P} \equiv$
$$
(\BB \true ;; \BB P ;; \BB \true \cup \BB \true ;; \BB P \cup \BB P
;; \BB \true \cup \BB P )$$
Wabenhorst also defines $\BB {\Box P}
\equiv \mathbb I \setminus \BB {\Diamond P}$, noting it is not
generally equal to $\BB P$. Law~12 states that equality holds
if $\alpha$, $\omega$ and $\delta$ do not occur free in $P$,
and, again, this is expressed using the function \verb|no_aod|.
% \begin{verbatim}
% law12 = "BBbox (no_aod ?P) = [(-no_aod ?P-)]" : thm
% \end{verbatim}
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.
\subsection{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 \cite{wabenhorst-induction},
Wabenhorst defines the language allowed for the construction of $H(\_)$.
% For example, a set difference expression such as $Y \backslash X$
% clearly should not be allowed.
% written as $z \in Y \land z \not\in X$ or as $z \in Y \land z \in
% \textit{complement}(X)$.
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.
However, in attempting to prove a related result we discovered a
counterexample to Law~13.
Let the predicate $P$ be defined as
$\delta > 0 \ \land \ t $ is rational.
Then $\BB{P} = \emptyset$ (since any non-zero interval contains
rationals and irrationals),
and $\BB{\lnot P} = \CC{\delta = 0}$.
Therefore likewise $\BB {\Diamond P} = \emptyset$,
and so $P$ trivially satisfies the finite variability property.
Define $H(X) \equiv X \subseteq S$, where $S$ is the minimal set of
intervals such that the conditions \emph{(a)} and \emph{(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 ``$\alpha$, $\omega$ and $\delta$ are not free
in $P$'' prevents us from using such a $P$
%(and, obviously, any similar predicate)
as a counterexample.
%\marginpar{\bf Axel!}
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 \cite{wabenhorst-induction}.
\section{Conclusion and Further Work}
\label{s-concl}
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,
% , and that Laws 13 and 14 rely
% upon unstated assumptions about the language of the formula $H(X)$.
%We also discovered that
that Law~13 (and probably Law~14 likewise) is incorrect due to a
problem with the definition of finite variability, that Law~13 of
\cite{fidge-tic} 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 \textit{different} forms (see
\S~\ref{sec:concatenation}).
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.
%\marginpar{\bf Axel!}
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.
% The best way of dealing with the problems of Laws 13 and 14 remains
% open, and we hope to address this shortly.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here begins the end matter
% \newpage
% \input{bib}
\begin{thebibliography}{99}
\bibitem{allen-intervals}
J~F~Allen. Towards a theory of action and time.
Artif.\ Intel.\ 23:123--154, 1984.
\bibitem{cerone-axiomatisation} 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.
\bibitem{church-types}
A~Church.
\newblock A formulation of the simple theory of types.
\newblock {\em JSL}, 5:56--68, 1940.
\bibitem{fidge-tic}
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.
\bibitem{goldblatt-logics}
R~I~Goldblatt,
Logics of Time and Computation,
CSLI Lecture Notes Number 7, Center for the Study of
Language and Information, Stanford, 1987.
\bibitem{heilmann-thesis}
S~T~Heilmann, Proof Support for Duration Calculus,
PhD thesis, Dept.\ of Inf.\ Tech.,
Tech.\ Univ.\ of Denmark, Jan.\ 1999.
See \texttt{http://www.sth.dk/sth/}.
\bibitem{HOL-introduction}
M~J~C Gordon and T~F Melham.
\newblock {\em Introduction to HOL: a Theorem Proving Environment for Higher
Order Logic}.
\newblock Cambridge University Press, 1993.
\bibitem{isabelle-ref}
L~C Paulson.
\newblock {\em The Isabelle Reference Manual}.
\newblock Comp.\ Lab., Univ.\ of Cambridge, 1999.
See \texttt{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/docs.html}
\bibitem{isabelle-object}
L~C Paulson.
\newblock {\em Isabelle's Logics}.
\newblock Computer Lab.\, Univ.\ of Cambridge, 1999.
See \texttt{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/docs.html}
\bibitem{mahony:boilerfull}
B~P Mahony and C~Millerchip and I~J~Hayes.
\newblock {\em A boiler control system: A case study in timed refinement}.
\newblock {International Invitational Workshop - Design and Review of
Software Controlled Safety-Related Systems}, Ottawa, June, 1993.
\bibitem{skakkebaek-thesis}
J~ Skakkeb\ae k, A verification assistant for a real-time logic,
PhD thesis, TR 150, Dept.\ of Computer Science,
Technical University of Denmark, 1994.
\bibitem{wabenhorst-induction}
A~Wabenhorst. Induction in the Timed Interval Calculus.
Technical Report 99-36, SVRC, University of Queensland, 1999.
\bibitem{duration-calculus}
%Zhou Chaochen. Duration calculi : An overview.
%In D~Bjorner, M~Broy and I~Pottosin, editors,
%\textit{Formal Methods in Programming and their Applications},
%LNCS 735, Springer-Verlag 1993, 256--266.
%
M~R~Hansen and Z~Chaochen.
Duration calculus, logical foundations.
Formal Aspects of Computing, 9 (1997), 283--303.
\end{thebibliography}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: