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

\subsection{The Clock-Bounded Chain Rule}
The basic rule for proving response properties of clocked transition
systems is the \emm{clock-bounded chain rule} (rule \cbchain)
presented in \Figr{cbchain}. The rule uses auxiliary assertions
$\varp_1,\ldots,\varp_m$ and refers to assertion $q$ also as
$\varp_0$. With each assertion $\varp_i$ we associate one of the
clocks $\clk_i\in C$, to which we refer as the \emm{helpful clock},
and an upper bound $\bnd_i$. The intention is that while remaining in
states satisfying $\varp_i$, the clock $\clk_i$ is bounded by
$\bnd_i$. Since time in a computation grows beyond any bound, this
will imply that we cannot continually stay at $\varp_i$-state for too
long.
\begin{figure}
\Xbox{80}{\hspace*{1cm}
\vbox{\lskip\boxpar{$\vcenter{\halign{\qquad\lft{#}\ &\lft{#}\cr
For&assertions $p$, $q$, and $\varp_0=q,\varp_1,\ldots,\varp_m$,\cr
&clocks $\clk_1,\ldots,\clk_m\in C$, and\cr
&real constants $\bnd_1,\ldots,\bnd_m\in \reals$,
\cr}}$}\lskip
\boxpar{$\vcenter{\halign{\lft{#}\cr
\ C1.\quad $p\ \ \rar\ \ \displaystyle{\bigvee^m_{j=0}}\
\varp_j$\cr}}$}\medskip
\boxpar{\ The following two premises hold for $i=1,\ldots,m$}\medskip
\boxpar{\quad $\left.\vcenter{\halign{\lft{#}\cr
\ C2.\quad $\rho_{\tau}\band \varp_i\ \ \rar\ \ 
(\varpi\pri \lwedge \clk_i\pri\ge \clk_i)\ \vee\
\displaystyle{\bigvee_{j<i}}\ \varp\pri_j$\cr
\noalign{\vskip 5pt}
\omit\hfill $\hbox{for\ every}\ \tau\in\Taut$\cr
\noalign{\vskip 5pt}
\ C3.\quad $\varp_i\ \ \rar\ \ \clk_i\le \bnd_i$\cr
}}\ \right.$}\vskip 5pt
\boxline{$\vcenter{\halign{\lft{#}\cr
\ \hbox to %9.2
7truecm{\hrulefill}\cr}}$}
$\vcenter{\halign{\lft{#}\cr
\qquad\qquad $p\ \ \Rar\ \ \dia q$\cr}}$\lskip}
}
\ctrlined{cbchain}{Rule \cbchain\ (clock-bounded chain rule for response).}
\par
Premise C1 requires that every $p$-position satisfies one of
$\varp_0=q,\varp_1,\ldots,\varp_m$.
\par
Premise C2 requires that every $\tau$-successor (for any
$\tau\in\Taut$) of a $\varp_i$-state $s$ is a $\varp_j$-state for some
$j\le i$. In the case that the successor state satisfies $\varp_i$, it
is required that the transition does not decrease the value of
$\clk_i$.

Premise C3 requires that assertion $\varp_i$ implies that $\clk_i$ is
bounded by the constant $\bnd_i$.

The following claim states the soundness of the rule:
\begin{claim}
\label{reactwsound}
Rule \cbchain\ is sound for proving that a response formula is
$\Phi$-valid.
\end{claim}

\nin{\bf Justification}: \quad
Assume that the premises of the rule are $\Phi$-valid, and let $\sig$ be
a computation of $\Phi$. We will show that $\sig$ satisfies the
rule's consequence
\[p\ \entails\ \F q,\]
i.e., every $p$ position in $\sig$ is followed by a $q$-position.

Assume that $p$ holds at position $k$ and no later position $i\ge k$
satisfies $q$.  By C1 some $\varp_j$ must hold at position $k$. Let
$j_k$ denote the minimal index such that $\varp_{j_k}$ holds at
$k$. Obviously $j_k>0$ by our assumption that $q$ never occurs beyond
position $k$.

By C2, state $s_{k+1}$ must satisfy $\varp_{j}$ for some $j$, $0<j\le
j_k$. Let $j_{k+1}$ denote the minimal such index. Continuing in this
manner we obtain that every position $i$ beyond $k$ satisfies some
$\varp_{j_i}$, where $j_i>0$ and
\[j_k \ge j_{k+1} \ge j_{k+2} \ge \cdots\ .\]

Since we cannot have an infinite non-increasing sequence of natural
numbers which decreases infinitely many times, there must exist a
position $r\ge k$ such that
\[j_r = j_{r+1} = j_{r+2} = \cdots\ .\]
Denote the value of this eventually-stable assertion index by $u=
j_r$.

Consider the value of the clock $\clk_u$ at states $s_i$, $i\ge r$. By
C2, the value of $\clk_u$ never decreases. Also, whenever a \tick\
transition with increment $\D$ is taken, $\clk_u$ increases (as do all
clocks) by $\D$. It follows that the master clock $T$ cannot increase
by more than $\bnd_u-s_r[\clk_u]$ from its value at state $s_r$. This
contradicts the fact that $\sig$ is a computation in which the master
clock increases beyond all bounds.

We conclude that our assumption of the existence of a $p$-position not
followed by any $q$-position is false. Consequently, if the premises
of the rule hold then every $p$-position must be followed by a
$q$-position, establishing the consequence of the rule.
\corn\medskip

\begin{example}\quad
We illustrate the use of rule \cbchain\ to prove the termination of
program \anyce, which can be stated by the response formula
\[\atl{0}\lwedge \atm{0} \lwedge x=t_1=t_2=0
\quad \entails\quad \F(\atl{2}\lwedge\atm{2}).\]

To apply rule \cbchain, we identify $p$ as $\atl{0}\lwedge \atm{0}
\lwedge x=t_1=t_2=0$ and $q$ as $\atl{2}\lwedge\atm{2}$. The auxiliary
assertions, helpful clocks, and bounds are presented in the following
table:
\[\begin{array}{lll}
\varp_0\colon\ \atl{2}\lwedge\atm{2} & \quad - &
\quad -\\
\varp_1\colon\ \atl{0}\lwedge \atm{1}\lwedge x=1 \lwedge t_1 \le 5 &
\clk_1\colon\ t_1 & \bnd_1\colon\ 5\\
\varp_2\colon\ \atl{1}\lwedge \atm{1}\lwedge x=1 \lwedge t_1\le 5 &
\clk_2\colon\ t_1 & \bnd_1\colon\ 5\\
\varp_3\colon\ \atl{0,1}\lwedge \atm{0}\lwedge x=0 \lwedge t_1\le 5
\lwedge t_2\le 5\qquad & \clk_3\colon\ t_2 \qquad & \bnd_1\colon\ 5
\end{array}\]

\nin We check the premises of rule \cbchain\ for this selection of
auxiliary assertions, helpful clocks, and bounds.
\begin{itemize}
\item Premise C1 assumes the form
\[\begin{array}{ll}
\underbrace{\atl{0}\lwedge \atm{0}\lwedge x=y=t_1=t_2=T=0}_p \ \
\rar\\
\hspace*{2.8cm}\underbrace{\cdots\ \vee\ \atl{0,1}\lwedge \atm{0}\lwedge
x=0 \lwedge t_1\le 5 \lwedge t_2\le 5}_{\cdots\ \vee\ \varp_3},
\end{array}\]
which is obviously state valid.

\item Premise C2 has to be checked for each $i=1,\ldots,m$ and each
$\tau\in\Taut$. We present only few representative cases.

Premise C2 for $\varp_3$ and transition $m_0$ assumes the form
$$\begin{array}{ll}
\underbrace{\pi\pri = \pi-\{m_0\}\cup \{m_1\} \lwedge x\pri =1 \lwedge
t_1\pri = t_1 \lwedge \cdots}_{\rho_{m_0}} \band \underbrace{\atl{0,1}
\lwedge t_1\le 5 \lwedge \cdots}_{\varp_3}\\
\hspace*{4cm}\rar\ \ \left(\begin{array}{lc}
 & \cdots \\[4pt]
\vee \quad & \underbrace{\atlp{0}\lwedge \atmp{1}\lwedge x\pri=1 \lwedge
t_1\pri \le 5}_{\varp_1\pri} \\
\vee \quad & \underbrace{\atlp{1}\lwedge \atmp{1}\lwedge x\pri=1 \lwedge
t_1\pri \le 5}_{\varp_2\pri}
\end{array}\right)_,
\end{array}$$
which is obviously state valid.

Premise C2 for $\varp_2$ and the \tick\ transition assume the form
$$\begin{array}{l}
\underbrace{\D>0 \lwedge \pi\pri = \pi \lwedge x\pri = x \lwedge
t_1\pri = t_1+\D \lwedge (\atl{0,1} \implies t_1+\D \le 5) \lwedge
\cdots}_{\rotick}\\
\wedge\ \underbrace{\atl{1}\lwedge \atm{1}\lwedge x=1 \lwedge t_1\le
5}_{\varp_2} \ \ \rar\\
\multicolumn{1}{r}{
\underbrace{\atlp{1}\lwedge \atmp{1}\lwedge x\pri=1 \lwedge t_1\pri\le
5}_{\varp_2\pri}\ ,}
\end{array}$$
which is obviously state valid.

\item Premise C3 is trivially valid, since each $\varp_i$,
$i=1,\ldots,3$ includes $\clk_i\le\bnd_i$ as a conjunct.
\end{itemize}

\nin This analysis indicates that all premises of rule \cbchain\ are
state valid. It follows that the reponse formula
\[\atl{0}\lwedge \atm{0} \lwedge x=t_1=t_2=0
\quad \entails\quad \F(\atl{2}\lwedge\atm{2})\]
is valid over program \anyce.
\corn
\end{example}

\subsection{Clock-Bounded Chain Diagrams}
\label{chaindiag}
The main ingredients of a proof by rule \cbchain\ can be conveniently
and effectively presented by a special type of verification diagrams
that summarizes the auxiliary assertions with their helpful clocks and
bounds, and display the possible transitions between the assertions.

We define a \emm{clock bounded chain diagram} (\emm{chain diagram} for
short) to be a directed labeled graph constructed as follows:
\begin{itemize}
\item \emm{Nodes} in the graph are labeled by assertions. Each node is
labeled by a pair of assertions: $\phi_i$ and $\bet_i$, for $i
=0,\ldots,m$. The assertion $\bet_i$ has the form $\clk_i\le \bnd_i$,
where $\clk_i\in C$ is a clock and $\bnd_i$ is a real constant. We
refer to the conjunction $\phi_i\lwedge\bet_i$ as $\varp_i$, and say
that the node is labeled by the (combined) assertion $\varp_i$. We
often refer to nodes by the assertion $\varp_i$ labeling them.

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 connects one assertion to another and is labeled
by one or more transitions. An edge can connect node $\varp_i$ to node
$\varp_j$ only if $i\ge j$. This imposes the restriction that the
graph of a chain diagram is weakly acyclic, i.e., the only cycles in
the graph consist of a node connected to itself.
\end{itemize}

\ssb{Verification Conditions Implied by a Chain Diagram}
Consider a nonterminal node labeled by assertion
$\varp\colon\;\phi\lwedge\bet$ where the clock-bound assertion is
$\bet\colon\;\clk\le \bnd$. 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 \lwedge \clk\pri\ge \clk)
\bor \varp\pri_1\ \vee\ \cdots\ \vee\ \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 \lwedge \clk\pri\ge \clk.\]

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

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

\begin{claim}
\label{validreactd}
If $D$ is a $\Phi$-valid chain diagram with nodes
$\varp_0,\ldots,\varp_m$, then
\[\Phi\models {\bigvee_{j=0}^m}\ \varp_j\ \ \Rar\ \ \dia\varp_0\]
If, in addition, $\varp_0= q$ and
\[\mbox{{\rm C1:}}\quad p\ \ \rar\ \ \displaystyle{\bigvee^m_{j=0}}\
\varp_j,\]
then we can conclude:
\[\Phi\models p\ \ \Rar\ \ \dia q.\]
\end{claim}

The claim follows from the observation that the verification
conditions associated with a chain diagram precisely correspond to
premise C2 of rule \cbchain. Premise C1 is trivially satisfied for the
first part of the claim, where we take $p$ to be $\bigvee_{j=0}^m
\varp_j$. It is explicitly provided in the second part of the claim.
Premise C3 is trivially satisfied by having $\bet_i\colon\;
\clk_i\le\bnd_i$ as an explicit conjunct of $varp_i = \phi_i\lwedge
\bet_i$.

\begin{example}\quad
In \Figr{respanyy}, we present a chain diagram for proving that
\[\atl{0}\lwedge \atm{0} \lwedge x=t_1=t_2=0 \quad \entails\quad
\F(\atl{2}\lwedge\atm{2})\]
is valid over program \anyce.
\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input respanyy.pstex_t
\caption{\label{respanyy} Verifying termination of program \anyce.}
\end{center} 
\end{figure}

Note the use of encapsulation in labeling the compound node by the
common clock bound $B\colon\ t_1\le 5$, which is factored out of nodes
$\varp_1$ and $\varp_2$. We also remove the index from the $\bet$
assertion labeling a node and write $\bet$ instead of $\bet_i$.
\corn
\end{example}

%\input{winning}
\subsection{Winning a Race}
We introduce an additional graph-structuring convention which leads to
a more economic and comprehensible verification diagrams. Similar to
the previously introduced encapsulation conventions, this one is also
inspired by the Statechart language \cite{H}.

A \emm{conjunctive compound node} is a compound node which contains
two sets of encapsulated nodes: $\{\phi_1,\ldots,\phi_m\}$ and
$\{\psi_1,\ldots,\psi_n\}$. The two sets are separated by a dashed
line. Edges may connect nodes within each of the sets, and external
nodes to nodes in each of the sets. No edge may connect a $\phi$-node
to a $\psi$-node. We also allow a multi-source edge such as the edge
connecting nodes $\phi_2$ and $\psi_2$ to the external node $\chi$.

In \Figr{andnode}, we present a graph with a conjunctive compound node.
\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input andnode.pstex_t
\caption{\label{andnode} A conjunctive compound node.}
\end{center} 
\end{figure}

Any diagram containing conjunctive nodes can be expanded into an
equivalent flat diagram, to which we refer as the \emm{expanded
diagram}, as follows:
\begin{itemize}
\item For each $i\in\{1,\ldots,m\}$ and $j\in\{\psi_1,\ldots,n\}$,
the expanded diagram contains a node, labeled by the conjunction
$\phi_i\wedge \psi_j$.
\item For each $\tau$-labeled edge connecting $\phi_a$ to $\phi_b$,
there are $\tau$-labeled edges connecting expanded node $\phi_a\wedge
\psi_j$ to $\phi_b\wedge \psi_j$ for all $j\in\{1,\ldots,n\}$.
\item For each $\tau$-labeled edge connecting $\psi_c$ to $\psi_d$,
there are $\tau$-labeled edges connecting expanded node $\phi_i\wedge
\psi_c$ to $\phi_i\wedge \psi_d$ for all $i\in\{1,\ldots,m\}$.
\item For each $\tau$-labeled edge connecting $\phi_a$ to external
node $\chi$, there are $\tau$-labeled edges connecting expanded node
$\phi_a\wedge \psi_j$ to $\chi$ for all $j\in\{1,\ldots,n\}$.
\item For each $\tau$-labeled edge connecting $\psi_c$ to external
node $\chi$, there are $\tau$-labeled edges connecting expanded node
$\phi_i\wedge \psi_c$ to $\chi$ for all $i\in\{1,\ldots,m\}$.
\item For each $\tau$-labeled multi-source edge connecting nodes
$\phi_a$ and $\psi_c$ to external node $\chi$, there exists a
$\tau$-labeled edge connecting expanded node $\phi_a\wedge\psi_c$ to
node $\chi$.
\end{itemize}

\nin In \Figr{expanded}, we present the flat diagram equivalent to the
diagram of \Figr{andnode}.
\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input expanded.pstex_t
\caption{\label{expanded} An expanded equivalent to the conjunctive
diagram.}
\end{center} 
\end{figure}

\ssb{Analyzing Races between Processes}
Conjunctive nodes are particularly helpful for proving that one
process always wins in a race against a competing process. Consider
the trivial program \race\ presented in \Figr{race}.
\begin{figure}[hbtp]
\begin{center}
\fbox{
$
\begin{array}{ccc}
\left[\begin{array}{ll}
\ell_0: & \bold{skip}\\
\ell_1: & \bold{skip}\\
\ell_2:
\end{array}\right]
& \quad\PLL\quad &
\left[\begin{array}{ll}
m_0: & \bold{skip}\\
m_1: & \bold{skip}\\
m_2: & \bold{skip}\\
m_3: & \bold{skip}\\
m_4:
\end{array}\right]\\
\quad \\
-\quad P_1 \quad - & & -\quad P_2 \quad -
\end{array}
$}
\caption{\label{race} Program \race.}
\end{center}
\end{figure}

As in the case of program \mtxlu, we assign to all statements of
program \race\ time bounds $[L,U]$, stipulating that $2L > U$. It is
clear that when this program is run, process $P_1$ will terminate
before $P_2$ does. This is because $P_1$ mst terminate within $2U$
time units, while $P_2$ must take at least $4L> 2U$ time units to
terminate. How do we formally prove this property which can be stated
by the response formula
\[\atl{0}\lwedge \atm{0} \lwedge t_1=t_2=T =0 \quad\entails\quad
\F(\atl{2}\lwedge \atm{0..3})\ ?\]

In \Figr{race1}, we present a chain diagram which proves this
property.
\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input race1.pstex_t
\caption{\label{race1} Chain diagram proving that $P_1$ wins the race.}
\end{center} 
\end{figure}

A central argument in the validation of this diagram is that
transition $m_2$ is disabled on all nodes within the conjunctive
compound node.  Transition $m_2$ can be enabled only on an
$\atm{2}$-state and only when $t_2\ge L$. Combining the assertion
attached to the $m_2$ node with $t_2\ge L$, we obtain $T\ge 2L >
4U$. However, all assertions on the left-hand side of the conjunctive
node imply $T\le 4U$. This shows that $m_2$ is disabled on all states
covered by the conjunctive node, and the only exit is via $\ell_1$.

This establishes the property
\[ \atl{0}\lwedge \atm{0} \lwedge t_1=t_2=T =0 \quad\entails\quad
\F(\atl{2}\lwedge \atm{0..3}).\]

%\input{subsection5p3.tex}
\subsection{Proving Accessibility for Program \mtxlu}
As a more ambitious example, we prove for program \mtxlu\ the property
of accessibility which can be stated (for process $P_1$) by the
response formula
\[\atl{2}\quad\entails\quad \F\atl{9}.\]
A similar formula states accessibility for process $P_2$.

{From} the invariance diagram of \Figr{invmtx}, we can infer the
following four invariants, which we will use in the response proof:
\[\begin{array}{ll}
\GH_0\colon      & \G(x\in\{0,1,2\})\\
\GH_1\colon\quad & \G(\atl{0..2,4,5} \quad\implies\quad x\ne 1)\\
\GH_2\colon      & \G(\atm{0..2,4,5} \quad\implies\quad x\ne 2)\\
\GH_3\colon       & \atl{4}\quad\entails\quad x=0
\bor (\atm{6..10} \lwedge x=2)
\end{array}\]

The accessibility formula is proved in several steps, verifying
separately the following response formulas:
\[\begin{array}{ll}
\psi_1\colon\quad & \atl{2} \quad\entails\quad \F\atl{4}\\
\psi_2\colon & \atl{4}\lwedge x=0 \quad\entails\\
\multicolumn{2}{r}{\F\bigl(\atl{8} \bor (\atl{4,6,7} \lwedge \atm{6}
\lwedge x=2 \lwedge t_2=0)\bigr)}\\
\psi_3\colon & \atl{4,6,7} \lwedge \atm{6} \lwedge x=2 \lwedge t_2=0
\quad\entails\\
\multicolumn{2}{r}{\F(\atl{4} \lwedge \atm{0} \lwedge x=0 \lwedge
t_2=0)}\\
\psi_4\colon & \atl{4}\lwedge \atm{6..10} \lwedge x=2
\quad\entails\\
\multicolumn{2}{r}{\F(\atl{4} \lwedge \atm{0} \lwedge x=0 \lwedge
t_2=0)}\\
\psi_5\colon & \atl{4} \lwedge \atm{0} \lwedge x=0 \lwedge t_2=0
\quad\entails\\
\multicolumn{2}{r}{\F(\atl{6} \lwedge \atm{0..4} \lwedge x=1)}\\
\psi_6\colon & \atl{6} \lwedge \atm{0..4} \lwedge x=1
\quad\entails\quad \F\atl{8}
\end{array}\]

\nin It is not difficult to see that response formulas
$\psi_1$--$\psi_6$ lead to the accessibility property.

We proceed to prove each of the response formulas.

\ssb{Proving $\psi_1\colon\quad  \atl{2} \ \ \entails\ \ \ \F\atl{4}$}
Formula $\psi_1$ states that, starting at $\ell_2$, process $P_2$ is
guaranteed to reach $\ell_4$. Statement $\ell_2$ is unconditional and
is guaranteed to terminate within $U$ time units. By $\GH_1$, when we
enter $\ell_3$ from $\ell_2$, $x$ is different from 1, and will remain
so as long as we stay at $\ell_3$ ($\ell_5$ is the only statement that
can set $x$ to $1$). Consequently, within $U$ time units, $P_1$ will
proceed to $\ell_4$.

The formal proof of $\psi_1$ is provided by the chain diagram of
\Figr{chain1}
\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input chain1.pstex_t
\caption{\label{chain1} Chain diagram for $\psi_1\colon\ \atl{2}\
\entails\ \F\atl{4}$.}
\end{center} 
\end{figure}

\ssb{Proving $\psi_2$}
Response formula $\psi_2$ is given by
$$\atl{4}\lwedge x=0 \quad \entails\quad \F\bigl(\atl{8} \bor (\atl{4,6,7}
\lwedge \atm{6} \lwedge x=2 \lwedge t_2=0)\bigr).$$

\nin It states that, starting at location $\ell_4$ with $x=0$, process
$P_1$ will either reach the critical section (at $\ell_8$), or be
overtaken by process $P_2$ just entering location $m_6$ (and hence
$t_2=0$), while setting $x$ to $2$. In the latter case, $P_1$ will be
overtaken at one of the locations $\ell_4$, $\ell_6$, or $\ell_7$.

The formal proof of $\psi_2$ is presented by the chain diagram of
\Figr{chain2}.
\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input {chain2.pstex_t}
\caption{\label{chain2}
Chain diagram for the formula}
$\psi_2\colon\ \atl{4}\lwedge x=0 \ \ \entails\ \
\F\bigl(\atl{8} \bor (\atl{4,6,7} \lwedge \atm{6} \lwedge x=2 \lwedge
t_2=0)\bigr).$
\end{center} 
\end{figure}

The diagram follows the progress of process $P_1$ from $\ell_4$ with
$x=0$. While $P_1$ is at $\ell_4$, $P_2$ may execute statement $m_5$
and set $x$ to 2, which reaches the goal $\phi_0$. If this does not
happen, $P_1$ proceeds to $\ell_5$ and then to $\ell_6$, setting $x$
to 1. From this point on, either $P_2$ will perform $m_5$, leading
again to $\phi_0$, or $P_2$ will perform $\ell_7$ moving to $\ell_8$,
which is also a goal state.

\ssb{Proving $\psi_3$}
Response formula $\psi_3$ is given by
$$\atl{4,6,7} \lwedge \atm{6} \lwedge x=2 \lwedge t_2=0
\quad\entails\quad \F(\atl{4} \lwedge \atm{0} \lwedge x=0 \lwedge
t_2=0).$$

\nin The formula states that, once $P_1$ has been overtaken by $P_2$,
it will return to location $\ell_4$ \emm{before} $P_2$ exits its
critical section and returns to $m_0$, setting $x$ back to $0$. The
fact that, being denied entry to $\ell_8$, process $P_1$ must
eventually return to $\ell_3$ and proceed to $\ell_4$ is obvious. Less
obvious is the fact that when $P_2$ performs $m_{10}$ on its exit from
the critical section, $P_1$ is already at $\ell{4}$. This
result from the number of statements that each process has to execute
until they reach $\ell_4$ and $m_0$, respectively, and from the
assumption $U< 2L$ which guarantees that $P_1$ completes the execution
of a single statement before $P_2$ can complete the execution of two
statements.

The worst case for $P_1$ is if it is overtaken at $\ell_6$. To reach
$\ell_4$ it must execute 3 statements: $\ell_6$, $\ell_7$, and
$\ell_3$. It will take $P_1$ at most $3U$ to do so. To reach location
$m_0$ from its initial location at $m_6$, $P_2$ has to execute at
least 6 statements: $m_6$, $m_7$, $m_8$, $m_3$, $m_9$,
and $m_{10}$. It will take $P_2$ at least $6L$ to reach
$m_0$. Since $3U< 6L$, $P_1$ will get to $\ell_3$ first.

The precise analysis of this race between $P_1$ and $P_2$ is presented
by the chain diagram of \Figr{race2}
\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input {race2.pstex_t}
\caption{\label{race2}
Chain diagram for the formula}
$\begin{array}{l}
\psi_3:\quad
\atl{4,6,7} \lwedge \atm{6} \lwedge x=2 \lwedge t_2=0 \lwedge \Ta=0
\quad\entails\\
\hspace*{5cm}\F(\atl{4} \lwedge \atm{0} \lwedge x=0 \lwedge
t_2=0).
\end{array}$
\end{center} 
\end{figure}

Note that $m_{10}$ is enabled only at states in which $P_1$ is at
$\ell_4$. This is becaus at all other $P_1$-locations, $\Ta\le 3U< 6L$.
For $m_10$ to be enabled, $\Ta$ must be at least $6L$.

\ssb{Proving $\psi_4$}
Response formula $\psi_4$ is given by
$$\atl{4}\lwedge \atm{6..10} \lwedge x=2 \quad\entails\quad
\F(\atl{4} \lwedge \atm{0} \lwedge x=0 \lwedge t_2=0).$$

\nin The formula states that, starting with $P_1$ at $\ell_4$, $x=2$,
and $P_2$ somewhere within $\{m_6,\ldots,m_{10}\}$, we are guaranteed
to reach a state in which $P_1$ is still at $\ell_4$ but $P_2$ has
just moved to $m_0$ (hence $t_2= x=0$). This property relies on the
progress of $P_2$ through $\{m_6,\ldots,m_{10}\}$ to $m_0$ while $x=2$
and $P_1$ cannot change the value of $x$, beeing stuck at $\ell_4$.
For a formal proof of this property, we can use again the diagram of
\Figr{race2}, where the initial nodes are within the compound node
labeled by $\atl{4}$.


\ssb{Proving $\psi_5$}
Response formula $\psi_5$ is given by
$$\atl{4} \lwedge \atm{0} \lwedge x=0 \lwedge t_2=0
\quad\entails\quad \F(\atl{6} \lwedge \atm{0..4} \lwedge x=1).$$

The formula considers another possible race between $P_1$ and $P_2$,
starting with $P_1$ at $\ell_{4}$ and $P_2$ just arriving to $m_0$.
Formula $\psi_5$ states that $P_1$ will reach $\ell_6$ (with $x=1$
before $P_2$ reaches $m_5$. Note that from a state satisfying $\atl{6}
\lwedge \atm{0..4} \lwedge x=1$ the entry of $P_1$ to its critical
section is guaranteed, since $P_2$ cannot pass the test at $m_4$ and
interefere with $P_1$'s progress.

Formula $\psi_5$ is verified by the chain diagram of \Figr{race3}.
\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input {race3.pstex_t}
\caption{\label{race3}
Chain diagram for the formula}
$\psi_5\colon\quad
\atl{4} \lwedge \atm{0} \lwedge x=0 \lwedge t_2=0 \lwedge \Ta=0
\quad\entails\quad \F(\atl{6} \lwedge \atm{0..4} \lwedge x=1).$
\end{center} 
\end{figure}

A simple informal argument explains why $P_1$ is sure to win this
race. To move from $\ell_4$ to $\ell_6$, $P_1$ has to execute 2
statements: $\ell_4$ and $\ell_5$, which takes at most
$2U$. In that time, $P_2$ cannot complete the execution of the 5
statements $m_0$--$m_4$ necessary to reach $m_5$, since $5L > 2U$.

\ssb{Proving $\psi_6$}
Response formula $\psi_6$ is given by
$$\psi_6\colon\quad \atl{6} \lwedge \atm{0..4} \lwedge x=1
\quad\entails\quad \F\atl{8}.$$

\nin This formula states that, once $P_1$ reached $\ell_6$ while $P_2$
is still confined within the range $\{m_0,\ldots,m_4\}$, entry of
$P_1$ to $\ell_8$ is guaranteed. The proof presented in the diagram of
\Figr{nchain6} simply traces the progress of $P_1$ from $\ell_6$ to
$\ell_8$, while $x$ keeps its value of $1$.
\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input {nchain6.pstex_t}
\caption{\label{nchain6}
Chain diagram for the formula}
$\psi_6\colon\quad
\atl{6} \lwedge \atm{0..4} \lwedge x=1 \quad\entails\quad \F\atl{8}.$
\end{center} 
\end{figure}

\medskip

This concludes the proof of accessibility for program \mtxlu.


