\section{Real-Time Systems}
\label{cts}
We now introduce a computational model for real-time systems.

\subsection{Computational Model: Clocked Transition System}

Real-time systems are modeled as \emm{clocked transition systems} (\ctss).
A clocked transition system
$\Phi=\bigl<V,\Theta,\Tau,\Pi \bigr>$ consists of: 
\begin{itemize}
\item $V  = \{u_1, \ldots, u_n\}$ : A finite set of {\em system
variables}. The set $V=\Vd\cup C$ is partitioned into $\Vd$ the set
of \emm{discrete variables} and $C$ the set of \emm{clocks}.
Clocks always have the type \emm{real}. The
discrete variables can be of any type.
We introduce a special clock $T \in C$, representing the \emm{master
clock}, as one of the system variables.

\item $\Theta$ : The {\em initial condition}. A satisfiable assertion
characterizing the initial states. It is required that
$$ \Theta \quad \to\quad T = 0,$$
i.e., $T=0$ at all initial states.

\item $\cT$ : A finite set of {\em transitions}. Each transition
$\tau \in \cT$ is a function
$$\tau:\Sigma\mapsto 2\sp{\Sigma},$$
mapping each state $s\in\Sigma$ into a (possibly
empty) set of \emm{$\tau$-successor} states $\tau(s)\subseteq\Sigma$.

The function associated with a transition $\tau$ is represented by an
assertion $\rot(V ,V\pri)$, called the {\em transition relation},
which relates a state $s\in\Sigma$ to its $\tau$-successor $s\pri\in\tau(s)$
by referring to both unprimed and primed versions of the system variables.
An unprimed version of a system variable refers to its value in $s$,
while a primed version of the same variable refers to its
value in $s\pri$. For example, the assertion $x\pri=x+1$ states that the
value of $x$ in $s\pri$ is greater by $1$ than its value in $s$.

For every $\tau \in \cT$, it is required that
\[ \rot \quad \to\quad T' = T,\]
i.e., the master clock is modified by no transition.

\item $\Pi$ : The {\em time-progress condition}. An
assertion over $V$. The assertion is used to specify a global
restriction over the progress of time.

\end{itemize}

\ssb{Extended Transitions}

Let $\Phi:\bigl<V,\Theta,\Tau,\Pi\bigr>$ be a clocked transition system.
We define the set of {\em extended transitions} $\Taut$ associated with $\Phi$
as follows:
\[ \Taut = \Tau \cup \{\tick\}. \]
Transition $\tick$ is a special transition intended to represent the
passage of time. Its transition relation is given by:
\[\rotick\colon \quad \exists \Delta \St\, \Om(\Delta) \band \Vd' =
\Vd \band C' = C + \Delta,\]
where $\Om(\Delta)$ is given by
\[\Om(\Delta)\colon\quad \D>0 \band
\forall t \in [0,\Delta)\St\, \Pi(\Vd, C+t).\]
Let $\Vd=\{u_1,\ldots,u_m\}$ be the set of discrete variables of
$\Phi$ and $C=\{c_1,\ldots,c_k\}$ be the set of its clocks.
Then, the expression $C' = C+\Del$ is an abbreviation for
\[c'_1 = c_1+\Del\ \lwedge\ \cdots\ \lwedge\ c'_k=c+\Del,\]
and $\Pi(\Vd, C+t)$ is an abbreviation for
$\Pi(u_1,\ldots,u_m,c_1+t,\ldots,c_k+t)$.

\ssb{Runs and Computations}

Let $\Phi:\bigl<V,\Theta,\Tau,\Pi\bigr>$ be a clocked transition system.
A \emm{run} of $\Phi$ is a finite or infinite sequence of states
$\sig  :  s_0, s_1, \ldots$ satisfying:

\begin{itemize}
\item \boxa{{\em Initiation}:} $s_0\models\The$

\item \boxa{{\em Consecution}:} For each $j\in[0,\size{\sig})$\,
$s_{j+1} \in \tau(s_j)$,
for some $\tau \in \Taut$.
\end{itemize}

\noindent A state is called ($\Phi$-)\emm{accessible} if it appears in
a run of $\Phi$.

A \emm{computation} of $\Phi$ is an infinite run satisfying:

\begin{itemize}
\item \emm{Time Divergence:}\quad The sequence $s_0[T], s_1[T], \ldots$
grows beyond any bound. That is, as $i$ increases, the value of $T$ at
$s_i$ increases beyond any bound.
\end{itemize}

\ssb{A Frequently Occurring Case}
In many cases, the time-progress condition $\Pi$ has the following
special form
\[\Pi\colon\quad \bigwedge_{i\in I} (p_i\implies t^i<E_i),\]
where $I$ is some finite index set and, for each $i\in I$, the
assertion $p_i$ and the real-valued expression $E_i$ do not depend on
the clocks, and $t^i\in C$ is some clock. This is, for example, the
form of the time-progress condition for any \ctss\ representing a
real-time program. For such cases, the formula $\Om(\D)$ can be
significantly simplified and assumes the following form:
\[\begin{array}{rl}
\Om(\D)\colon\quad & \D>0 \band \displaystyle 
\bigwedge_{i\in I} (p_i\implies t^i+\D\le E_i)
\end{array}\]
Note, in particular, that this simpler form does not use
quantifications over $t$.

\ssb{Non-Zeno Systems}
A \ctss\ is defined to be \emm{non-zeno} if every finite run can be
extended into a computation (see \cite{AL91}, \cite{IPL}). An
equivalent formulation is that $\Phi$ is non-zeno if it satisfies
\begin{quote}
A finite sequence $\sig$ is a run of $\Phi$ iff $\sig$ is a prefix of
some computation of~$\Phi$.
\end{quote}
A consequence of $\Phi$ being non-zeno is that a state $s$ is
$\Phi$-accessible iff it appears in some computation of $\Phi$.

\begin{example}\quad
\label{exnonznonp}
Consider the \ctss's $\Phi_1$ and $\Phi_2$ presented in
Fig~\ref{2systems}.
\begin{figure}
\begin{center}
\fbox{
\begin{tabular}{ccc}
\quad\\
& \input {2systems.pstex_t} & \\
\quad
\end{tabular}
}
\caption{\label{2systems} Two \ctss's.}
\end{center} 
\end{figure}
In Fig~\ref{2systab}, we present these two \ctss's in textual form.
The predicate $\pres(y,t,T)$ is an abbreviation for the assertion
\[ \pres(y,t,T)\colon\quad y\pri=y \band t\pri=t \band T\pri,\]
stating that $y$, $t$, and $T$, are preserved by the transition.
\begin{figure}
$$
\begin{array}{|c|c|}
 \hline & \\
\ \begin{array}{rl}
V\colon & \underbrace{\{\pi\colon \{0,1\}; y\colon \mbox{\bf
integer}\}}_D \cup \underbrace{\{t,T\colon \mbox{\bf real}\}}_C \\
\Theta\colon & \pi = y = t = T = 0 \\
\Tau\colon & \{\tau_0, \tau_1\} \mbox{with transition relations}\\
& \begin{array}{rl}
\tau_0\colon & \pi = \pi\pri = 0 \lwedge y\pri = y+1\\
\multicolumn{2}{r}{\lwedge \pres(t,T)}\\
\tau_1\colon & \pi =0 \lwedge \pi\pri = 1 \lwedge \pres(y,t,T)
\end{array}\\
\Pi\colon & \pi=0 \to t<2\\
\quad\\
\multicolumn{2}{c}{\mbox{\ctss\ $\Phi_1$}}
\end{array}
\ &\
\begin{array}{rl}
V\colon & \underbrace{\{\pi\colon \{0,1\}; y\colon \mbox{\bf
integer}\}}_D \cup \underbrace{\{t,T\colon \mbox{\bf real}\}}_C \\
\Theta\colon & \pi = y = t = T = 0 \\
\Tau\colon & \{\tau_0, \tau_1\} \mbox{with transition relations}\\
& \begin{array}{rl}
\tau_0\colon & \pi = \pi\pri = t\pri = 0 \lwedge y\pri = y+1\\
\multicolumn{2}{r}{\lwedge \pres(T)}\\
\tau_1\colon & \pi =0 \lwedge \pi\pri = 1 \lwedge \pres(y,t,T)
\end{array}\\
\Pi\colon & \pi=0 \to t<\frac{1}{2^{y+1}}\\
\quad\\
\multicolumn{2}{c}{\mbox{\ctss\ $\Phi_2$}}
\end{array}\ \\
\quad & \\ \hline
\end{array}
$$
\caption{\label{2systab} The two \ctss's in textual form.}
\end{figure}

It is not difficult to establish that both $\Phi_1$ and $\Phi_2$ are
non-zeno \ctss's. This is becaues, from any accessible state, we can
always move to state $\ell_1$ from which we can continue to take
infinitely many time steps with increment 1.

The \tick\ transitions for these two \ctss's are given by
$$\begin{array}{rl}
\rotick^1 \colon & \exists\D>0 \St\, 
%\pi\pri = \pi \lwedge y\pri = y
\pres(\pi,y)
\lwedge
%t\pri = t+\D \lwedge T\pri = T+\D
(t\pri,T\pri) = (t+\D,T+\D)
\lwedge (\pi =0 \implies
t+\D \le 2)\\
\rotick^2 \colon & \exists\D>0 \St\,
%\pi\pri = \pi \lwedge y\pri = y
\pres(\pi,y)
\lwedge
%t\pri = t+\D \lwedge T\pri = T+\D
(t\pri,T\pri) = (t+\D,T+\D)
\lwedge (\pi =0 \implies
t+\D \le \frac{1}{2^{y+1}}).
\end{array}$$

Following is a computation of \ctss\ $\Phi_1$:
$$\begin{array}{lclc}
\stc(0,0,0) & \olr{tick(1)} &
\stc(0,0,1) & \olr{\tau_0} \\
\stc(0,1,1) & \olr{\tau_0} &
\stc(0,2,1) & \olr{tick(1)} \\
\stc(0,2,2) & \olr{\tau_0} &
\stc(0,3,2) & \olr{\tau_0}\\
\stc(0,4,2) & \olr{\tau_1} &
\stc(1,4,2) & \olr{tick(1)} \\
\stc(1,4,3) & \olr{tick(1)} &
\stc(1,4,4) & \olr{tick(1)} \\
\multicolumn{2}{c}{\cdots}
\end{array}$$
Note that to be a computation, time must grow beyond any bounds. Since,
at location $\ell_0$ of \ctss\ time cannot grow beyond $2$, any
computation of $\Phi_1$ must eventually move to location $\ell_1$,
where time can grow beyond any bounds.
\corn
\end{example}
