%% %% \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: