\section{Verifying Safety Properties of Clocked Transition Systems}
\label{safety}
In this section, we present methods for verifying safety properties of
clocked transitions systems.

\subsection{The Invariance Rule}
A temporal formula $\varphi$ that is valid over a program $P$ specifies
a property of $P$, i.e., states a condition that is satisfied by all
computations of $P$. As is explained in \cite{MPB}, the properties
expressible by temporal logic can be arranged in a hierarchy that
identifies different classes of properties according to the form of
formulas expressing them.

Here we will consider only \emm{invariance} properties, namely,
properties that can be expressed by the formula $\G p$,
for some assertion $p$.

\ssb{The Accessibility Rule}
As a preliminary step, we introduce a rule that establishes the
$\Phi$-validity of an assertion $p$. This is rule \acc, presented in
\Figr{acc}.
\begin{figure}
\LLbox{\boxline{\qquad For assertions $\varp$ and $p$,}%\lskip
\Ruleb{A1.\quad $\varp\ \rar\ p$\cr
\noalign{\vskip 5pt}
A2.\quad $\The\ \rar\ \varp$\cr
\noalign{\vskip 5pt}
A3.\quad $\rho_\tau\band\varp\ \ \rar\ \ \varp\pri$\quad for every
$\tau\in\Taut$\cr
\Bar
$\qquad\hskip 1pt\Phi\vmodels p$\cr}\lskip}
\ctrlined{acc}{Rule \acc\ ($\Phi$-state validity of assertion $p$).}

The rule uses an auxiliary assertion $\varp$.  Premise A1 of rule
\acc\ requires that the auxiliary assertion $\varp$ implies assertion
$p$, whose $\Phi$-state validity we wish to prove.  Premise A2 of the
rule requires that $\The$, the initial condition of $P$, implies the
auxiliary assertion $\varp$.  Premise A3 requires that all transitions
in $\Taut^{\Phi}$ (extended transitions of $\Phi$) preserve
$\varp$. Premises A2 and A3 state that $\varp$ holds at the initial
state of every run and that it propagates from any state to its
$\tau$-successor, for every transition $\tau\Taut$ of the
system. Thus, every state in each run of $\Phi$ satisfies $\varp$. Due
to the implication A1, every such state also satisfies $p$. It follows
that $p$ holds on every accessible state of system $\Phi$ and,
therefore, assertion $p$ is $\Phi$-state valid.

\ssb{Rule \inv}
Assume that we have shown that assertion $p$ is $\Phi$-state valid,
i.e., every accessible state of $\Phi$ satisfies $p$. Since all states
appearing in a computation are accessible (every computation is
a run), all states in every computation satisfy $p$. It follows
that every computation of $\Phi$ satisfies $\G p$. Thus, we may use
the premises of rule \acc\ to establish that the temporal formula $\G
p$ is $\Phi$-valid. Consequently, we propose rule \inv, presented in
\Figr{inv}, as the main tool for verifying invariance properties of a
\ctss\ $\Phi$.
\begin{figure}
\LLbox{\boxline{\qquad For assertions $\varp$ and $p$,}%\lskip
\Ruleb{I1.\quad $\varp\ \rar\ p$\cr
\noalign{\vskip 5pt}
I2.\quad $\The\ \rar\ \varp$\cr
\noalign{\vskip 5pt}
I3.\quad $\rho_\tau\band\varp\ \ \rar\ \ \varp\pri$\quad for every
$\tau\in\Taut$\cr
\Bar
$\qquad\hskip 1pt\Phi\models\boc p$\cr}\lskip}
\ctrlined{inv}{Rule \inv\ (invariance) applied to \ctss\ $\Phi$.}

\begin{example}\quad
We use rule \inv\ to establish the invariance of the
assertion
\[p\colon\quad \atl{0,1}\lvee \atm{1}\]
over program \anyy\ (Fig.~\ref{anyy}). This assertion claims that, at
every state in the execution of program \anyy, either control of
process $P_1$ is at $\ell_0$ or $\ell_1$, or control of
$P_2$ is at $m_1$. In particular, it implies that if $P_1$ is at
$\ell_2$ then $P_2$ has already arrived in $m_1$.

We apply rule \inv\ to this choice of $p$, taking
\[\varp\colon\quad (x=0\wedge \atl{0,1})\lvee \atm{1}\]
as the auxiliary assertion.

Premise I1 assumes the form
\[\underbrace{(x=0 \wedge \atl{0,1}) \vee \atm{1}}_{\varp}
\quad\implies\quad \underbrace{\atl{0,1}\lvee \atm{1}}_p,\]
which is obviously valid.

Premise I2 assumes the form
\[\underbrace{\pi= \{\ell_0, m_0\} \lwedge x=0\lwedge
\cdots}_{\Theta}\quad\to\quad
\underbrace{(x=0 \wedge \atl{0,1}) \vee \cdots}_{\varp} \]
which is obviously valid.

Premise I3 has to be checked for each $\tau\in\{\ell_0, \ell_1,
m_0, \tick\}$. For example, premise I3 for $\ell_0$ assumes the form
$$\begin{array}{l}
\left(\begin{array}{l}
\underbrace{\cdots \wedge
\left(\begin{array}{c}
	x=0\ \wedge\ \pi\pri=\pi-\{\ell_0\}\cup\{\ell_1\} \\
		\vee\\
	x\neq 0\ \wedge\ \pi\pri=\pi-\{\ell_0\}\cup\{\ell_2\}
\end{array}\right)
\lwedge x\pri=x \lwedge \cdots}_{\rho_{\ell_{0}}}\\
\quad\\[-7pt]
\wedge\ \ \underbrace{\bigl(x=0\wedge \elabinp\bigr)\lvee
m_1\in\pi}_{\varp}
\end{array}\right)
\quad\to\quad \hspace*{1.7cm}\\
\quad\\[-7pt]
\multicolumn{1}{r}{
\underbrace{\bigl(x\pri=0\wedge \elabinpp\bigr)\lvee
m_1\in\pi\pri}_{\varp\pri}.}
\end{array}$$
It is not difficult to see that this implication is valid.

This establishes the $P$-validity of the invariant $\G p$, i.e.,
\[ P\models \G(\atl{0,1}\lvee \atm{1}).\corn\]
\end{example}

\nin
For assertions $p$ and $q$ and transition $\tau$, we introduce the
abbreviation
\[\quad\{p\}\tau\{q\}\qquad \mbox{standing for} \qquad \rot \land p\ \to\
q\pri.\]

\ssb{Invariance Verification Diagrams}
An effective way of presenting the verification of an invariance
property by rule \inv\ is provided by the graphical formalism of
\emm{verification diagrams} \cite{tacs94}. An (invariance)
verification diagram is a directed labeled graph, constructed as
follows:
\begin{itemize}
\item \emm{Nodes} in the graph are labeled by assertions $\varphi_1,
\ldots, \varphi_m$. We will often refer to a node by the assertion
labeling it.
\item \emm{Edges} in the graph represent transitions between
assertions. Each edge departs from one node, connects to another, and
is labeled by the name of a transition in the program. We refer to an edge
labeled by $\tau$ as a \emm{$\tau$-edge}.
\item Some of the nodes are 
designated as \emm{initial nodes}. They are annotated by an entry arrow
\mbox{%\input diag8.pic
\setlength{\unitlength}{0.007in}
\begin{picture}(25,%40
25)(0,%5
5)
\put(5,20){\circle*{10}}
\spline(10,20)
(25,20)(25,0)
\path(23,8)(25,0)(27,8)
\end{picture}
}.
\end{itemize}

\noindent For example, in Fig.~\ref{fig:d1} we present a
verification diagram for program \anyy.
\begin{figure}[hbt]
\vspace{-0.5cm}
\begin{center}
%\leavevmode 
\mbox{\input {d1.pstex_t}}
\caption{\label{fig:d1} Verification Diagram $D_1$}
\end{center} 
\vspace{-1cm}
\end{figure} 

\ssb{Verification Conditions for Diagrams}

With each verification diagram, we associate the following \emm{verification
conditions}:

\begin{itemize}
\item Let $\varphi_1$ be the (single) initial node in the diagram. The
verification condition corresponding to premise I2 of rule \inv\ is
given by
\[\Theta\ \to\ \varphi_1.\]
\item Let $\varphi$ be a node in the graph, $\tau$ be a
transition in the program, and let $\varphi_1,\ldots,\varphi_k$ be the
nodes reached by $\tau$-edges departing from $\varphi$.  The case that
no $\tau$-edges depart from $\varphi$, i.e., $k=0$, is also included.
The verification condition associated with $\varphi$ and $\tau$
(corresponding to premise I3) is given by
\[\triple(\varphi,\tau,\varphi \vee \varphi_1 \vee \ldots \vee \varphi_k)\]
\end{itemize}

\noindent For example, the verification conditions associated with
diagram $D_1$ (Fig.~\ref{fig:d1}), are:

$$\begin{array}{lcl}
\mbox{I2:} & \quad &\Theta \to\ x=0 \wedge \atl{0,1}\\[4pt]
\mbox{I3 for $\varp_1$ and $\ell_0:$} & &
\triple(x=0 \wedge \atl{0,1},\ell_0,x=0\wedge \atl{0,1})\\
\mbox{I3 for $\varp_1$ and $\ell_1:$} & &
\triple(x=0 \wedge \atl{0,1},\ell_1,x=0\wedge \atl{0,1})\\
\mbox{I3 for $\varp_1$ and $m_0:$} & &
\triple(x=0 \wedge \atl{0,1},m_0,{(x=0\wedge \atl{0,1}) \lvee \atm{1}})\\
\mbox{I3 for $\varp_1$ and $\tick:$} & &
\triple(x=0 \wedge \atl{0,1},\tick,x=0\wedge \atl{0,1})\\[4pt]
\mbox{I3 for $\varp_2$ and $\ell_0:$} & &
\triple(\atm{1},\ell_0,\atm{1})\\
\mbox{I3 for $\varp_2$ and $\ell_1:$} & &
\triple(\atm{1},\ell_1,\atm{1})\\
\mbox{I3 for $\varp_2$ and $m_0:$} & &
\triple(\atm{1},m_0,\atm{1})\\
\mbox{I3 for $\varp_2$ and $\tick:$} & &
\triple(\atm{1},\tick,\atm{1})\\
\end{array}$$

We say that a verification diagram is \emm{valid} if all the
verification conditions associated with the diagram are valid.

Let $D_{_P}$ be a verification diagram associated with a
program $P$. Let
$\varphi_1,\ldots,\varphi_m$ be the assertions labeling the nodes of
$D_{_P}$.

\begin{claim}
If the verification diagram $D_P$ is valid, then
\[P \models \G\bigvee_{i = 1}^{m} \varphi_i \]
If, in addition, $\varphi_i \to\ p$ for every $i = 1,\ldots, m$, then
\[P \models \G p.\]
\end{claim}

For example, all the verification conditions associated with
diagram $D_1$ are valid and the verification diagram $D_1$
establishes
\begin{equation}
\label{anyyeq}
\mbox{\sc any-y} \models (\atl{0,1} \lvee \atm{1})
\end{equation}

\subsubsection*{Encapsulation Conventions}
There are several encapsulation conventions that improve the
presentation and readability of verification diagrams. We extend the
notion of a directed graph into a structured directed graph by
allowing \emm{compound nodes} that may encapsulate other nodes, and
edges that may depart or arrive at compound nodes. A node that does
not encapsulate other nodes is called a \emm{basic node}.


We use the following conventions:
\begin{itemize}
\item \emm{Labels of compound nodes}:\quad A diagram containing a
compound node $n$, labeled by an assertion $\GF$ and encapsulating
nodes $n_1,\ldots,n_k$ with assertions $\GF_1,\ldots,\GF_k$, is
equivalent to a diagram in which $n$ is unlabeled and nodes
$n_1,\ldots,n_k$ are labeled by $\GF_1\wedge \GF$, \ldots, and
$\GF_k\wedge \GF$.
\item \emm{Edges entering and exiting compound nodes}:\quad A diagram
containing an edge $e$ connecting node $A$ to a compound node $n$
encapsulating nodes $n_1,\ldots,n_k$ is equivalent to a diagram in
which there is an edge connecting $A$ to each $n_i$, $i=1,\ldots,k$,
with the same label as $e$. Similarly, an edge $e$ connecting
the compound node $n$ to node $B$ is the same as having a separate
edge connecting each $n_i$, $i=1,\ldots,k$, to $B$ with the same label
as $e$.
\end{itemize}

\noindent  With these conventions we can draw a more detailed verification
diagram 
establishing~(\ref{anyyeq}), as shown in Fig.~\ref{fig:d2}.

\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input d2.pstex_t
\caption{\label{fig:d2} A more detailed diagram, using encapsulation
conventions}
\end{center} 
\end{figure}
In the diagram of Fig.~\ref{fig:d2}, the single assertion $x=0\wedge
\atl{0,1}$, has been broken into the two sub-cases: $x=0\wedge \atl{0}$
and $x=0\wedge \atl{1}$, explicitly displaying the fact that
transitions $\ell_0$ and $\ell_1$ cause the system to move between
these two sub-cases.


%% Old %%
We also use invariance diagrams to provide succinct representations of
proofs by rule \inv.

\begin{example}\quad
We use rule \inv\ to prove that program \anyce\ terminates within $15$
time units, as specified by the following invariance formula:
\[ \G\bigl(T \leq 15 \lvee (\atl{2} \wedge \atm{1})\bigr) \]

\noindent This formula claims that every accessible state in which the
program has not terminated yet (i.e., $\atl{2} \wedge \atm{1}$ does
not hold), can only be observed when the master clock $T$ has not yet
passed $15$. It follows that any state observed later than $T=15$ must
be a termination state.

The proof is presented by the invariance diagram in
Fig.~\ref{fig:exr1}.
\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input exr1.pstex_t
\caption{\label{fig:exr1} Termination of {\sc any-y} within $15$ time units.}
\end{center} 
\end{figure} 

\nin
The assertions are indexed in descending order from $\varp_3$ on top to
$\varp_0$ at bottom in order to keep compatibility with the chain
diagrams introduced in Section~\ref{response}.

Note that no edge in the diagram is labeled by the \tick\ transition.
This implies that all verification conditions involving the \tick\
transition are of the form $\triple(\varp_i,\tick,\varp_i)$ claiming
that the \tick\ transition preserves each of the assertions appearing
in the diagram.

As an example, consider the verification condition claiming that
assertion $\varp_1\colon\ \atl{1}\lwedge T\le 5+ t_1\le 10$ is
preserved by the \tick\ transition.
$$\begin{array}{l}
\underbrace{\atl{1}\lwedge T\le 5+ t_1\le 10}_{\varp_1} \quad \band \\
\multicolumn{1}{r}{\underbrace{\D>0 \lwedge \pi\pri=\pi
\lwedge T\pri = T+\D \lwedge t_1\pri = t_1+\D \lwedge (\atl{1} \to
t_1+\D \le 5) \lwedge \cdots}_{\rotick}} \\
\multicolumn{1}{r}{\implies \quad
\underbrace{
\atlp{1}\lwedge T\pri\le 5+ t_1\pri\le 10}_{\varp_1\pri}}
\end{array}$$
It is not difficult to see that this implication is state-valid.\corn

\end{example}

%\input{example5.tex}
\begin{example}\quad
As a second example, we present a mutual-exclusion
algorithm, due to M. Fischer, which functions properly only due to the
timing constraints associated with the statements. Similar proofs to
the one we will present here are given in \cite{SBM91}, \cite{AL91},
and \cite{MMP}.

The algorithm is presented in Fig.~\ref{fschr} under the name of
program \mtx. By assigning all statements in \mtx\ the uniform time
bounds $[L,U]$, we obtain the timed program \mtxlu.  Assuming that
$2L > U$, we prove that the mutual exclusion property
\[\G\neg(\atl{8} \lwedge \atm{8}) \]
is valid for \mtxlu.
\begin{figure}[hbtp]
\begin{center}
\fbox{
$
\begin{array}{c}
x\colon\ \bold{integer\ where}\ x=0\\
\quad\\
\begin{array}{ccc}
\left[\begin{array}{l}
\ell_0: \ \bold{loop forever do}\\
\quad \left[\begin{array}{ll}
  \ell_1: & \bold{noncritical}\\
  \ell_2: & \bold{skip}\\
  \ell_3: & \bold{while $x\ne 1$ do}\\
  \multicolumn{2}{l}{\quad\left[\begin{array}{ll}
    \ell_4: & \bold{await $x=0$} \\
    \ell_5: & x:= 1	\\
    \ell_6: & \bold{skip}\\
    \ell_7: & \bold{if $x=1$ then} \\
            & \ell_8: \ \bold{critical}
    \end{array}\right]}\\
  \ell_9: & \bold{skip}\\	
  \ell_{10}: & x := 0
  \end{array}\right]
\end{array}\right]
& \quad\PLL\quad &
\left[\begin{array}{l}
m_0: \ \bold{loop forever do}\\
\quad \left[\begin{array}{ll}
  m_1: & \bold{noncritical}\\
  m_2: & \bold{skip}\\
  m_3: & \bold{while $x\ne 2$ do}\\
  \multicolumn{2}{l}{\quad\left[\begin{array}{ll}
    m_4: & \bold{await $x=0$} \\
    m_5: & x:= 2	\\
    m_6: & \bold{skip}\\
    m_7: & \bold{if $x=2$ then} \\
            & m_8: \ \bold{critical}
    \end{array}\right]}\\
  m_9: & \bold{skip}\\	
  m_{10}: & x := 0
  \end{array}\right]
\end{array}\right]\\
\quad \\
-\quad P_1 \quad - & & -\quad P_2 \quad -
\end{array}
\end{array}
$
}
\caption{\label{fschr} Program \mtx, implementing Fischer's protocol.}
\end{center}
\end{figure}

Let us explain informally why mutual exclusion for program \mtx\ is
guaranteed and the role of the \emm{skip} statements at $\ell_6$ and
$m_6$. Assume a violation of mutual exclusion in which process $P_1$
ewntered its critical section (location $\ell_8$) first and, while
$P_1$ is still there, process $P_2$ enters $m_8$. When $P_1$ entered
$\ell_8$, $x$ was $1$. For $P_2$ to enter $m_8$ later, it was
necessary for it to set $x$ to 2 first, which can only be done at
$m_5$. Since after $P_1$ set $x$ to 1 at $\ell_5$, $P_2$ cannot pass
the test for $x=0$ at $m_4$, the only possibility is that $P_2$ kept
waiting at $m_5$ while $P_1$ executed $\ell_6$ and the test at
$\ell_7$. This must have taken $P_1$ at least $2L$, since $L$ is the
lower bound for execution of a statement. However, $P_2$ cannot wait
at $m_5$ for as long as $2L$ because $2L>U$ and no process can delay
the execution of a statement for more than $U$. It follows that the
described scenario in which $P_2$ keep waiting at $m_5$ until $P_1$
enters $\ell_8$ is impossible. The role of the \emm{skip} statement at
$\ell_6$ is therefore to introduce an additional delay of at least $L$
time units.

The \emm{skip} statements at $\ell_9$ and $m_9$ are
necessary to guarantee the response properties of this algorithm, and
we will discuss them in the next section. The \emm{skip} statements at
$\ell_2$ and $m_2$ represent exits out of the noncritical sections (at
$\ell_1$ and $m_1$, respectively) and intention to enter the critical
sections.

The property of mutual exclusion for program \mtx\ can be stated by
the invariance formula
\[\G\neg (\atl{8}\band \atm{8}).\]
A formal proof of this invariant is presented by the invariance
diagram of \Figr{invmtx}.
\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input invmtx.pstex_t
\caption{\label{invmtx} Mutual exclusion for program \mtx.}
\end{center} 
\end{figure}

Note that the edge labeled $\ell_5$ reaches the compound node labeled
$x=1$. By the encapsulation conventions, this is equivalent to having
this edge connect to the basic node labeled $\atl{6..10},\
\atm{0..4,6,7,9,10}$ and the compound node labeled $\atm{5}$. While
reaching this compound node, it should enter some of its contained
basic nodes. The default-entry arrow marks the basic node labeled
$\atl{6},\ t_2\ge t_1$ as the single node entered by the $\ell_5$
edge. Thus, the $\ell_5$ edge connects to the basic node labeled
$\atl{6..10},\ \atm{0..4,6,7,9,10}$ and the one labeled $\atl{6},\
t_2\ge t_1$.
\corn
\end{example}

\subsection*{Completeness of Rule \inv}
Rule \inv\ is complete for verifying invariances of fair transition
systems. This is stated by the following claim.

\begin{claim}
\label{complinv}
If formula $\G p$ is valid over non-zeno \ctss\ $P$, then there exists
an assertion $\varp$ such that premises {\rm I1}-{\rm I3} of rule \inv\
are state-valid.
\end{claim}

\nin{\bf Justification}\quad
The basic idea of the proof is the construction of an assertion
$\accp$ that holds in a state $s$ iff $s$ is $P$-accessible, i.e.,
appears in some run of $P$. We then show that if $\G p$ is $P$-valid,
then the premises of rule \inv\ are state-valid (implying that they
are also $P$-state valid) when taking $\accp$ for $\GF$. Since we are
only proving \emm{relative} completeness, it is enough to show
validity of the premises, assuming an oracle that provides proofs or
otherwise verifies all generally valid assertions.

For the construction of $\accp$, we refer the reader to \cite{Comp91}
or Chapter 2 of \cite{MPB2}. Assume that we have constructed an
assertion $\accp$ such that
\begin{quote}
$s\models \accp$ \qquad iff \qquad $s$ is a $P$-accessible state.
\end{quote}

\nin
We show that $\accp$, when substituted for $\GF$, validates the three
premises of rule \inv.
\begin{itemize}
\item[I1.] $\accp\to p$\\
By our assumption that $\G p$ is $P$-valid, it follows that each state
appearing in some computation satisfies $p$. As $P$ is non-zeno, every
accessible state appears in some computation and, hence, every
accessible state satisfies $p$. Since $\accp$ characterizes precisely
the accessible states, the premise follows.
\item[I2.] $\Theta\to\accp$\\
It is obvious that every state satisfying $\The$ is initial and
is, therefore, $P$-accessible. Consequently, such a state must satisfy
$\accp$, which characterizes all $P$-accessible states.
\item[I3.] $\rot(U,\wtU)\lwedge \accp(U) \quad \to \quad
\accp(\wtU)$,\ for each $\tau\in\cT$ and every values of $U$ and
$\wtU$.\\
Let $U$ and $\wtU$ be two lists of values, which can be viewed as values
of the system variables $V$, such that both $\rot(U,\wtU)$ and $\accp(U)$
are true. We will show that $\accp(\wtU)$ is also true.

Let $s$ and $\wts$ be two arbitrary states such that $s[V]= U$ and
$\wts[V] = \wtU$. Since $\accp(U)=\scT$, we have that $s\models \accp$.
By the meaning of $\accp$, it follows that $s$ is $P$-accessible. From
$\rot(U,\wtU) =\scT$, it follows that $\langle s,\wts \rangle \models
\rot(V ,V\pri)$ and, therefore, that $\wts$ is a $\tau$-successor of
$s$. Since $s$ is accessible, it follows that also $\wts$ is
accessible and, hence $\wts\models \accp$, leading to $\accp(\wtU) = \scT$

\end{itemize}
This concludes the proof of completeness of rule \inv.\corn

\medskip

The following example demonstrates that the assumption that $P$ is
non-zeno is essential to the completeness of the rule.

\begin{example}\quad
Consider the \ctss\ $\Phi_3$ which is presented graphically in
\Figr{phic} and textually in \Figr{phictab}.
\begin{figure}
\begin{center}
\fbox{
\begin{tabular}{ccc}
\quad\\
& \input {phic.pstex_t} & \\
\quad
\end{tabular}
}
\caption{\label{phic} \ctss\ $\Phi_3$.}
\end{center} 
\end{figure}

Clearly, \ctss\ $\Phi_3$ is a possibly-zeno system because, once a run
enters location $\ell_1$, time is bounded and cannot diverge. Thus, a
run entering location $\ell_1$ cannot be extended into a computation
of $\Phi_3$. A result of the fact that no computation of $\Phi_3$ ever
enters location $\ell_1$ is that the invariance formula $\G\atl{0}$ is
$\Phi_3$-valid.
\begin{figure}
$$
\begin{array}{|c|}
\hline
\quad \\[-8pt]
\ \begin{array}{rl}
V\colon & \{\pi\colon \{0,1\}; t,T\colon \mbox{\bf real}\} \\
\Theta\colon & \pi = t = T = 0 \\
\Tau\colon & \{\tau_{01}\}\ \mbox{with transition relations}\\
& \begin{array}{rl}
\tau_{01}\colon & \pi =0 \lwedge \pi\pri = 1 \lwedge t\pri = 0 \lwedge
T\pri = T
\end{array}\\
\Pi\colon & \pi=1 \to t<1
\end{array}\ \\[-8pt]
\quad \\
\hline
\end{array}
$$
\caption{\label{phictab} \ctss\ $\Phi_3$ in textual form.}
\end{figure}
However, examination of the arguments for the soundness of rule \inv\
shows that any assertion $p$, whose invariance is proven by rule \inv,
must hold on all accesible states. The state $\lan \pi\colon 1\ran$ is
accessible for \ctss\ $\Phi_3$ but does not satisfy $\atl{0}$.
Therefore, the $\Phi_3$ validity of $\G\atl{0}$ cannot be proven by
rule \inv.
\corn

\end{example}

%\input{waiting}
\subsection{Verifying Waiting-for Formulas}
The invariance formula $\G q$ states that $q$ holds continuously from
the beginning of the computation to infinity. In comparison, the
waiting-for formula
\[p \quad\entails\quad q\W r\]
also states the continuous holding of $q$ but only for an interval
that is initiated by an occurrence of $p$ and may be terminated by an
occurrence of $r$. Such formulas are useful for expressing timing
properties, where time is measured since an occurrence of an event,
rather than from the beginning of a computation.

\begin{example}\quad
Consider program \cyclic, presented in \Figr{cyclicp}.
\begin{figure}[hbtp]
\begin{center}
\fbox{
$
\begin{array}{c}
x, y\colon\ \bold{integer\ where}\ x=y=0\\
\quad\\
\begin{array}{ccc}
%P_1::\ \ 
\left[\begin{array}{l}
\ell_0: \ \bold{loop forever do}\\
\quad\left[\begin{array}{ll}
\ell_1: & \bold{while}\ x=0\ \bold{do}\\
\multicolumn{2}{l}{
\quad\ell_2:\ y:=y+1}\\
\ell_3: & x := 1
\end{array}\right] 
\end{array}\right]
& \quad\PLL\quad &
%P_2::\ \ 
\left[\begin{array}{l}
m_0: \ \bold{loop forever do}\\
\quad\left[\begin{array}{ll}
m_1: & x:= 1\\
m_2: & \bold{await $x=0$}
\end{array} \right]
\end{array} \right]\\
\quad\\
-\quad P_1 \quad - & & -\quad P_2 \quad -
\end{array}
\end{array}
$
}
\caption{\label{cyclicp} Program \cyclic.}
%
\end{center}
\end{figure}
This program can be viewed as a generalization of program \anyy, in
which the basic interaction between processes $P_1$ and $P_2$ is
embedded within an endless loop.

Since program \cyclic\ never terminates, a relevant time-related
property is that from any state in which we observe $P_1$ at $\ell_1$
and $P_2$ at $m_1$, $P_1$ will reach location $\ell_3$ within at most
$15$ time units.

This property can be stated by the following waiting-for formula:
\[\atl{1}\lwedge \atm{1}\lwedge x=0 \lwedge T=a
\quad\entails\quad (T\le a+15)\W\atl{3}.\]
This formulas uses a rigid variable $a$ to record the time at the
initial observation state. It claims that from the time we observe a
state satisfying $\atl{1}\lwedge \atm{1}\lwedge x=0$, time will not
progress by more than 15 units before we observe $P_1$ at $\ell_3$.

To facilitate the expression of such properties, we introduce the
abbreviation
\[\Ta\colon\quad T-a.\]
With this abbreviation we can write the property of ``reaching
$\ell_3$ within $15$ time units'' as
\[\atl{1}\lwedge \atm{1}\lwedge x=0 \lwedge \Ta=0
\quad\entails\quad (\Ta\le 15)\W\atl{3}.\]
The $\Ta$ abbreviation allows us to view $\Ta$ as a special timer,
reset at the initial point of observation.
\corn
\end{example}

\ssb{A Waiting-for Rule}
To establish the $P$-validity of a waiting-for formula, we may use
rule \wait, presented in \Figr{wait}.
\begin{figure}
\LLbox{\boxline{\qquad For assertions $p$, $q$, $\varp$, and $r$,}
\Ruleb{U1.\quad $\varp\ \rar\ q$\cr
\noalign{\vskip 5pt}
U2.\quad $p\ \rar\ r\lvee \varp$\cr
\noalign{\vskip 5pt}
U3.\quad $\rho_\tau\band\varp\ \ \rar\ \ r\pri \lvee \varp\pri$\quad
for every $\tau\in\Taut$\cr
\Bar
$\qquad\hskip 1pt\Sys\models p\quad\entails\quad q\W r$\cr}\lskip}
\ctrlined{wait}{Rule \wait\ (waiting-for) applied to \ctss\ $\Sys$.}

\ssb{Waiting Diagrams}
Proofs by rule \wait\ can be succinctly represented by special
verification diagrams to which we refer as \emm{waiting diagrams}.

A waiting diagram is a directed labeled graph constructed as follows:
\begin{itemize}
\item \emm{Nodes} in the graph are labeled by assertions $\varphi_0,
\ldots, \varphi_m$. We will often refer to a node by the assertion
labeling it.

The node labeled by $\varp_0$ is called the \emm{terminal node} and is
graphically identified by being drawn with bold-face boundaries.

\item \emm{Edges} in the graph represent transitions between
assertions. Each edge is labeled by the name of a transition in the
program. We refer to an edge labeled by $\tau$ as a \emm{$\tau$-edge}.
No edges depart form the terminal node.

\item Some of the nodes are designated as \emm{initial nodes}. They
are annotated by an entry arrow.
\end{itemize}

\ssb{Verification Conditions Implied by a Chain Diagram}
Consider a nonterminal node labeled by assertion
$\varp$. Let $\tau\in \Taut$ be a transition and let
$\varp_1,\ldots,\varp_k$, $k\ge 0$, be the successors of $\varp$ by
edges labeled with $\tau$ (possibly including $\varp$ itself).
With each such node and transition, we associate the
following verification condition:
\[\rho_\tau\band\varp\ \ \rar\ \ \varp\pri
\bor \varp\pri_1\ \bor\ \cdots\ \bor\ \varp\pri_k.\]
In particular, if $k=0$ (i.e., $\varp$ has no $\tau$-successors), the
associated verification condition is
\[\rho_\tau\band\varp\ \ \rar\ \ \varp\pri.\]

\ssb{Valid Waiting Diagrams}
A waiting diagram is said to be \emm{valid over \ctss\ $P$}
($P$-\emm{valid} for short) if all the verification conditions
associated with the diagram are $P$-state valid.

The consequences of having a valid chain diagram are stated in the
following claim:

\begin{claim}
\label{validwaitd}
If $D$ is a $P$-valid waiting diagram with nodes
$\varp_0,\ldots,\varp_m$, then
\[P\models {\bigvee_{j=0}^m}\ \varp_j\ \ \Rar\ \ (\bigvee_{j=0}^m\W\varp_0\]
If, in addition, $\varp_0= r$,
\[\mbox{{\rm U1:}}
\quad \displaystyle{\bigvee^m_{j=0}}\ \varp_j\ \ \rar\ \ q,
\qquad\mbox{and}\qquad
\mbox{{\rm U2:}}
\quad p\ \ \rar\ \ \displaystyle{\bigvee^m_{j=0}}\ \varp_j,
\]
then we can conclude:
\[P\models p\ \ \Rar\ \ q\W r.\]
\end{claim}

\nin{\bf Justification}\quad
We observe first that the verification conditions associated with a
waiting diagram imply premise U3 of rule \wait, when we take $\varp$
to be $\varp_1\lvee\cdots\lvee\varp_m$ and $r$ to be $\varp_0$.

If we further take $p= \varp_0\lvee\cdots\lvee\varp_m$ and
$q= \varp_1\lvee\cdots\lvee\varp_m$, we find that
premises U1 and U2 hold trivially. This yields the first part of the
claim.

The second part of the claim considers different $p$ and $q$ but
explicitly requires that premises U1 and U2 are $P$-valid. The
conclusion follows by rule \wait.\corn

\begin{example}\quad
In \Figr{wait1}, we present a waiting diagram that establishes the
property
\[\atl{1}\lwedge \atm{1}\lwedge x=0 \lwedge \Ta=0
\quad\entails\quad (\Ta\le 15)\W\atl{3}\]
for program \cyclic.
\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input wait1.pstex_t
\caption{\label{wait1} A waiting diagram, establishing the formula}
$\atl{1}\lwedge \atm{1}\lwedge x=0 \lwedge \Ta=0 \quad\entails\quad
(\Ta\le 15)\W\atl{3}$
\end{center} 
\end{figure}
\corn
\end{example}
