\title{Verifying Clocked Transition Systems\thanks{
This research was supported in part by the National Science Foundation
under grant CCR-92-23226, by the Advanced Research Projects
Agency under NASA grant NAG2-892, by the United States Air Force
Office of Scientific Research under grant F49620-93-1-0139, and by
Department of the Army under grant DAAH04-95-1-0317,
by a basic research grant from the Israeli Academy
of Sciences, and by the European Community ESPRIT Basic Research
Action Project 6021 (REACT).
}\\
%{\large A tribute to Prof. C.S. Tang on his 70th birthday}
}

%\addtocounter{footnote}{3}

\newcommand\titlesp{\quad }

\author{
Yonit Kesten\thanks{%
Department of Computer Science, Weizmann
Institute, Rehovot, Israel, e-mail: {\tt yonit@wisdom.weizmann.ac.il}}
\titlesp
Zohar Manna\thanks{%
Department of Computer Science, Stanford University,
Stanford, CA 94305,
e-mail: {\tt manna@cs.stanford.edu}}
\titlesp
Amir Pnueli\footnotemark[2]
}
%\date{Draft\\ \today}

%\addtocounter{footnote}{-2}

\institute{}

%\institute{
%Department of Computer Science, Stanford University\\
%Stanford, CA 94305\\
%e-mail: {\tt manna@cs.stanford.edu}
%\and
%Department of Applied Mathematics and Computer Science\\
%Weizmann Institute, Rehovot, Israel\\
%e-mail: {\tt amir@wisdom.weizmann.ac.il}
%}

\maketitle

\comment{
\begin{dedication}
This paper is dedicated to Prof. C.S. Tang who took the ideas of
temporal logic much beyond anyone's imagination, and applied them in
ways nobody before ever thought possible. We wish him many more
productive years of research and scientific contribution.
\end{dedication}
}

\begin{abstract}

This paper presents a new computational model for real-time systems,
called the \emm{clocked transition system} model.  The model is a
development of our previous \emm{timed transition} model, where some
of the changes are inspired by the model of \emm{timed automata}. The
new model leads to a simpler style of temporal specification and
verification, requiring no extension of the temporal language. For
verifying safety properties, we present a run-preserving reduction
from the new real-time model to the untimed model of fair transition
systems. This reduction allows the (re)use of safety verification methods
and tools, developed for untimed reactive systems, for proving safety
properties of real-time systems.

\end{abstract}


