\section{Proving that a \ctss\ is Non-Zeno}
\label{nonzenos}%
It is by now a widely accepted notion that the only interesting
real-time systems are those which obey the non-zeno restriction. One
of the reasons is that, since we only consider time-divergent runs as
computations, a possibly-zeno system may contain components that will
never be accessed in a computation. In some sense, these components
are redundant to the description of the system and their inclusion is
superfluous and often confusing and misleading. Non-zeno systems, on
the other hand, contain no such redundancy, since every accessible
state also appears in some computation.

In view of the significance of the non-zeno restriction, it is
important to be able to verify that an arbitrary given \ctss\ is
non-zeno.

In many cases, there are simple sufficient conditions which guarantee
that the system is non-zeno. One of the most important case is the
following:
\begin{claim}
\label{programsnonz}%
Let $P$ be an \splt\ program in which the upper bound assigned to each
executable statement is positive. Then $\Fsysp$, the \ctss\
corresponding to $P$, is a non-zeno system.
\end{claim}

\nin{\bf Justification}\quad
Let $\Um>0$ be the minimal upper bound. Consider a finite run
$r\colon\ s_0,\ldots,s_k$. We wish to show that $r$ can be extended
into a computation.

The recipe for extending $r$ considers the last reached state $s$ (starts
at $s=s_k$ and decides to apply the next transition as follows:
\begin{itemize}
\item If the \tick\ transition is enabled on $s$, take the \tick\
transition with increment $\D>0$, which is the maximal $\D\le 1$
satisfying $s\vmodels \Om(\D)$.
\item If the \tick\ transition is disabled on $s$, it must be blocked
by one of the processes, say $P_i$, whose clock $t_i$ has reached the
upper bound of some transition $\tau$ of $P_i$ which is currently enabled.
In this case, take this ripe transition $\tau$.
\end{itemize}
It is not difficult to check that an accessible state in a clocked
transition systems derived from a program with positive upper bounds
always has at least one extended transition enabled on it. Thus, the
described recipe produces an infinite run. This observation hinges on
the revised transition relation we associated with the \emm{wait}
statement.

It only remains to check that the infinite run produced by this
recipe is time-divergent and, hence, is a computation. By considering
the different possibilities, we observe that two cases are possible.

In one case, we eventually reach a state $s$ such that $s\vmodels
\Om(\D)$, for every $\D>0$. In this case, once we reach this $s$, we
continue to take \tick\ steps with $\D=1$.

In the remaining case, for every reached state $s_i$, there exists a
limit $\D_i$ such that $s_i\vmodels \Om(\D)$ for no $\D>\D_i$. In this
case, our construction must take infinitely many untimed transitions,
i.e., transitions $\tau\ne\tick$. Note that each such transition
resets one of the clocks to 0. It follows that the construction of the
infinite run causes at least one of the clocks, say $t_i$, to be reset
to 0 infinitely many times. It is not difficult to see that between
two consecutive resets of clock $t_i$, time must progress by at least
$\Um$. It follows that time has progressed infinitely many time by the
amount $\Um>$ and, therefore, the run is time-divergent.
\corn

\subsection{A Rule for Establishing Non-Zenoness}
While Claim~\ref{programsnonz} settles the question of non-zenoness
for many useful cases, there are additional cases which require
different methods. The claim was established for the simpler case that
the upper bounds assigned to transitions were positive constants. It
can easily be generalized to state-dependent upper bounds which are
bounded from below by a positive constant. However, this still does
not cover all possible cases. For example, \ctss\ $\Phi_4$ presented
in \Figr{Phi4}, is a non-zeno system, even though, the upper bounds of
the transition connecting $\ell_0$ to itself have no lower bound.
\begin{figure}
\begin{center}
\fbox{
\begin{tabular}{ccc}
&\quad\\
& \begin{tabular}{rl}
$y\colon$ & \bold{integer where $y=1$} \\
$t_1, T\colon$ & \bold{real where $t_1=T=0$}
\end{tabular}\\
&\quad\\
& \mbox{\input {Phi4.pstex_t}} & \\
\quad
\end{tabular}
}
\caption{\label{Phi4} A nonzeno \ctss\ $\Phi_4$ with upper bounds
tending to 0.}
\end{center} 
\end{figure}

The general strategy we propose for proving that a given \ctss\ $\Phi$
is non-zeno is summarized in rule \nonz, presented in \Figr{nonz}.
\begin{figure}
\LLbox{\boxline{\qquad For assertion $\varp$,}
\Ruleb{N1.\quad $\Phi\vmodels \varp$\cr
\noalign{\vskip 5pt}
N2.\quad $\Phi\models AG(\varp\lwedge V=V_0\lwedge \Ta=0
\quad\rar\quad EF(\Ta>0))$\cr
\Bar
\qquad\hskip 1pt$\Phi$ is non-zeno\cr}\lskip}
\ctrlined{nonz}{Rule \nonz\ ($\Phi$ is a non-zeno \ctss).}

The rule uses an auxiliary assertion $\varp$. Premise N1 requires that
$\varp$ is $\Phi$-state valid, and can be proven using rule \acc.

Premise N2 belongs to the realm of branching-time temporal logic, which
is different from the linear-time temporal framework we have been
consistently using in this paper. It has long been observed that the
property of being non-zeno cannot be formulated in linear-time \tl\
and needs branching-time \tl\ for its precise formulation. In a recent
paper (\cite{possibility}), Lamport makes this observation but suggests a
method by which properties such as non-zenoness can still be verified
in a linear framework. We prefer to use the branching-time logic \ctl
(\cite{EC}) for formulating the required property, as in premise N2,
and present a single proof rule which is adequate to establish \ctl\
formulas such as the one presented in N2. A deductive
system for verifying the main \ctl\ properties appeared in \cite{BMP}.
A more comprehensive deductive system for \ctl\ was recently proposed
in \cite{FG95}.

\subsection{Verifying Possibility Formulas}
A \emm{possibility formula} is a \ctl formula of the form
\[ AG(p\ \rar\ EF q),\]
for assertions $p$ and $q$. Without entering into the individual
meaning of the \ctl\ temporal operators $AG$ and $EF$, we say that the
possibility formula $AG(p \rar EF q)$ is \emm{valid over} \ctss\
$\Phi$ (\emm{$\Phi$-valid}) if
\begin{quote}
For every accessible $p$-state $s$, there exists a run segment
$s{=}s_1, \ldots, s_k$ leading from $s$ to a $q$-state $s_k$.
\end{quote}
We write
\[\Phi\models AG(p\ \rar\ EF q)\]
to indicate that the possibility formula $AG(p \rar EF q)$ is
$\Phi$-valid.

In \Figr{gposs}, we present rule \poss\ which is sound and complete for
proving the $\Phi$-validity of a possibility formula.
\begin{figure}
\LLbox{
\hspace*{1.6cm}
\vbox{\lskip\boxpar{$\vcenter{\halign{\qquad\lft{#}\ &\lft{#}\cr
For&assertions $p$, $q$, and $\varp_0=q,\varp_1,\ldots,\varp_m$,\cr
&transitions $\tau_1,\ldots,\tau_m\in\Taut$,\cr
&functions $\Nextf_1,\ldots,\Nextf_m\colon\ \Sig\mapsto\Sig$,\cr
&a well-founded domain $(\Ascr,\succ)$, and\cr
&ranking functions $\del_0,\ldots,\del_m\colon\ \Sig\mapsto\Ascr$,
\cr}}$}\lskip
\boxpar{$\vcenter{\halign{\lft{#}\cr
\ G1.\quad $p\ \ \rar\ \ \displaystyle{\bigvee^m_{j=0}}\
\varp_j$\cr}}$}\medskip
\boxpar{\ The following premise holds for $i=1,\ldots,m$}\medskip
\boxpar{\quad $\left.\vcenter{\halign{\lft{#}\cr
\ G2.\quad $ \varp_i\band V\pri=\Nextf_i\ \ \rar\ \ \rho_{\tau_i}\band
\displaystyle{\bigvee^m_{j=0}} (\varp\pri_j \lwedge \del_i \succ
\del_j\pri)$\cr
}}\ \right.$}\vskip 5pt
\boxline{$\vcenter{\halign{\lft{#}\cr
\ \hbox to %9.2
7truecm{\hrulefill}\cr}}$}
$\vcenter{\halign{\lft{#}\cr
\qquad\qquad $\Phi\models AG(p\ \ \Rar\ \ EF q)$\cr}}$\lskip}
}
\ctrlined{gposs}{Rule \gposs\ ($\Phi$ validity of a possibility formula).}

The rule requires finding auxiliary assertions $\varp_i$, functions
$\Nextf_i\colon\ \Sig\mapsto\Sig$, and transitions $\tau_i$,
$i=1,\ldots,m$, a well-founded domain $(\Ascr,\succ)$, and ranking
functions $\del_i\colon\ \Sscr\mapsto\Ascr$. Each assertion $\varp_i$
is associated with the transition $\tau_i$ that is helpful at
positions satisfying $\varp_i$, with a function $\Nextf_i$ that
selects a successor state, and with its own ranking function
$\del_i$. We have presented the successor-selection functions
$\Nextf_i$ as mapping states to states but, in fact, they map $s[V]$,
i.e., the values of the system variables in state $s$, to $s\pri[V]$,
the values of the system variables in a successor state $s\pri$.

Premise G1 requires that every $p$-position satisfies one of
$\varp_0,\ldots,\varp_m$.

Premise G2 considers a $\varp_i$-state $s$ and a state $\wts$ such
that $\wts[V]=s[V\pri] = \Nextf_i$, for some $i=1,\ldots,m$.
The premise requires that $\wts$ is a $\tau_i$-successor of $s$ which
satisfies $\varp_j$, for some $j=0,\ldots,m$ and has a rank
lower than that of $s$.

\nin{\bf Justification}\quad
Let $s$ be a $p$-state. We will show that there exists a run segment
$s{=}s_1,\ldots, s_k$ which leads from $s$ to a $q$-state. By premise
G1, $s=s_1$ must satisfy $\varp_j$, for some $j=0,\ldots,m$. Let $j_1$
be the minimal $j$ such that $s\vmodels\varp_j$. If $j=0$, we are
done, since $s_1$ satisfies $\varp_0=q$.

Otherwise, $j_1>0$ and let $u_1=\del_{j_1}(s_1)$. Let $s_2$ be any
state such that $s_2[V]=\Nextf_{j_1}(s_1[V])$. By premise G2, $s_2$ is
a $\tau_{j_1}$-successor of $s_1$, satisfies $\varp_{j_2}$ for some
$j_2\in\{0,\ldots,m\}$, and a rank $u_2=\del_{j_2}(s_2)\prec u_1$.
If $j_2=0$, we are done. Otherwise, we take $s_3$ to be some
$\Nextf_{j_2}$-selected successor of $s_2$, and so on.

This construction can terminate when we reach some $k$ such that
$j_k=0$. If it does no terminate, we generate an infinite descending
sequence
\[u_1\succ u_2 \succ \cdots.\]
This is impossible due to the well-foundedness of $\cA$. We conclude
that the construction must terminate in a state $s_k$ satisfying
$\varp_0=q$.
\corn

\begin{example}\quad
We illustrate the application of rule \gposs\ for proving that the
possibility formula
\[AG\bigl(\underbrace{\atl{0,1}\lwedge \Ta=0}_p \quad\rar\quad
EF(\underbrace{\Ta\ge 1}_q)\bigr)\]
is valid over \ctss\ $\Phi_5$, presented in \Figr{Phi5}.
\begin{figure}
\begin{center}
\fbox{
\begin{tabular}{ccc}
&\quad\\
& \begin{tabular}{rl}
$T\colon$\ & \bold{real where $t_1=T=0$}
\end{tabular}\\
&\quad\\
& \mbox{\input {Phi5.pstex_t}} & \\
\quad
\end{tabular}
}
\caption{\label{Phi5} A nonzeno \ctss\ $\Phi_5$.}
\end{center} 
\end{figure}

Observe that transition $\tau$, the only transition in $\Phi_5$, has
two successors. One satisfying $\atl{0}$ and the other satisfying
$\atl{1}$.

To apply rule \gposs, we take $(\IN,>)$ (the domain of the natural
numbers) as the well-founded domain. The auxiliary assertions, helpful
transitions, successor-selection functions, and ranking functions are
given by the following table:
\[\begin{array}{llll}
\varp_0\colon\ \Ta\ge 1 & \tau_0\colon\ \tick & \Nextf_0\colon\
\nexta(1,T+1) & \del_0\colon\ 0\\
\varp_1\colon\ \atl{1}\lwedge \Ta\ge 0 & \tau_1\colon\ \tick\quad &
\Nextf_1\colon\ \nexta(1,T+1)\quad & \del_1\colon\ 1\\
\varp_2\colon\ \atl{0}\lwedge \Ta\ge 0\quad & \tau_2\colon\ \tau &
\Nextf_2\colon\ \nexta(1,T) & \del_2\colon\ 2
\end{array}\]
This choice of constructs, corresponds to a strategy of constructing a
run segment in which time will progress by at least 1. According to
this strategy, if we are at $\ell_0$, we choose to take transition
$\tau$ and choose a $\tau$-successor state satisfying $\atl{1}$. If we
are at $\ell_1$, we choose to take the \tick\ transition with time
increment 1.

It is not difficult to check that all premises of rule \gposs\ are
satisfied by this choice of constructs.

It follows that the
possibility formula
\[AG\bigl(\atl{0,1}\lwedge \Ta=0 \quad\rar\quad
EF(\Ta\ge 1)\bigr)\]
is $\Phi_5$-valid.
\corn
\end{example}

\subsection*{Systems with Deterministic Transitions}
Rule \gposs\ is very general and can be shown to be complete for
proving possibilities properties of all clocked transition systems.
However, there is a big family of systems which can be handled by a
rule which call for identification of simpler constructs.

A transition $\tau$ of a \ctss\ is called \emm{deterministic} if all
the $\tau$-successors of an accessible state assign the same values to
the system variables. That is, if we restrict our attention to the
values of the system variables, each accessible state has at most one
$\tau$-successor. We say that a \ctss\ $\Phi$ is
\emm{transition-deterministic} ($\Phi$ is a \tdctss\ for short) if all
of its (untimed) transitions are deterministic. All the systems we
have presented in this paper, excluding $\Phi_5$, are
transition-deterministic.

Consider a \tdctss\ $\Phi$.  Assume that we wish to construct the
successor-selection function $\Nextf_i$ corresponding to assertion
$\varp_i$, where $\tau_i\ne\tick$. Since $\tau_i$ is deterministic,
$\Nextf_i$ is uniquely determined, and its explicit specification is
redundant. The situation is different with the \tick\ transition,
which may have (uncountably) many successors, each corresponding to a
different value of the time increment $\D$. However, once we specify
the value of $\D$, the successor of a \tick\ transition is also
uniquely determined up to differences in non-system variables.

Thus, instead of specifying a complete successor function, specifying
the values of all system variables in the successor state, it is
sufficient to specify the time increment $\D_i$ associated with the
successor. For uniformity, we specify values of $\D_i$ also for
untimed transitions, but then we ensure that $\D_i=0$.

This leads to rule \poss\ (\Figr{poss}) which is adequate for proving
possibility properties of every \tdctss. Rule \poss\ has more
premises than rule \gposs\ but it requires the identification of
simpler constructs, and the premises are easier to verify.
\begin{figure}
\LLbox{
\hspace*{1.0cm}
\vbox{\lskip\boxpar{$\vcenter{\halign{\qquad\lft{#}\ &\lft{#}\cr
For&assertions $p$, $q$, and $\varp_0=q,\varp_1,\ldots,\varp_m$,\cr
&transitions $\tau_1,\ldots,\tau_m\in\Taut$,\cr
&time increments $\D_1,\ldots,\D_m\ge 0$,\cr
&a well-founded domain $(\Ascr,\succ)$, and\cr
&ranking functions $\del_0,\ldots,\del_m\colon\ \Sig\mapsto\Ascr$,
\cr}}$}\lskip
\boxpar{$\vcenter{\halign{\lft{#}\cr
\ P1.\quad $p\ \ \rar\ \ \displaystyle{\bigvee^m_{j=0}}\
\varp_j$\cr}}$}\medskip
\boxpar{\ The following premises hold for $i=1,\ldots,m$}\medskip
\boxpar{\quad $\left.\vcenter{\halign{\lft{#}\cr
\ P2.\quad $\rho_{\tau_i}\band T\pri= T+\D_i\band \varp_i\ \ \rar\ \ 
\displaystyle{\bigvee^m_{j=0}} (\varp\pri_j \lwedge \del_i \succ
\del_j\pri)$\cr
\noalign{\vskip 5pt}
\ P3.\quad If $\tau_i=\tick$ then\cr
\noalign{\vskip 2pt}
\qquad\qquad P3t.\quad $\varp_i\ \ \rar\ \ \Om(\D_i)$\cr
\noalign{\vskip 2pt}
\hspace*{0.8cm} Otherwise\cr
\noalign{\vskip 2pt}
\qquad\qquad P3n.\quad $\varp_i\ \ \rar\ \ \D_i=0 \band \emm{En}(\tau_i)$\cr
}}\ \right.$}\vskip 5pt
\boxline{$\vcenter{\halign{\lft{#}\cr
\ \hbox to %9.2
7truecm{\hrulefill}\cr}}$}
$\vcenter{\halign{\lft{#}\cr
\qquad\qquad $\Phi\models AG(p\ \ \Rar\ \ EF q)$\cr}}$\lskip}
}
\ctrlined{poss}{Rule \poss\ ($\Phi$ validity of a possibility formula).}

Note that rule \poss\ splits premise G2 of rule \gposs\ into two
premises. Premise P2 guarantees that the (unique) successor of a
$\varp_i$-state corresponding to the identification of the helpful
transition $\tau_i$ and the time increment $\D_i$ (if it exists),
satisfies some $\varp_j$ with a lower rank. Premise P3 guarantees that
each $\varp_i$ state does have a successor corresponding to $\tau_i$
and $\D_i$. The premise is split into the case of the \tick\
transition (sub-premise P3t) and the case of all other untimed
transitions (sub-premise P3n). Sub-premise P3t requires that $\varp_i$
imply $\Om$, the enabling condition of of transition \tick, with the
specified $\D_i$. Sub-premise P3n requires that $\D_i=0$ and that
$\varp_i$ implies the enableness of $\tau_i$.

\begin{example}\label{provpos}\quad
We illustrate the use of rule \poss\ for proving that the possibility
formula
\[AG(\underbrace{\atl{0} \lwedge 1\le b=y \lwedge 0\le
t_1\le\frac{1}{\sqrt{y}} \lwedge 0=\Ta}_p \quad\rar\quad
EF(\underbrace{\Ta\ge 1}_q))\]
is valid over \ctss\ $\Phi_4$.

Note that \ctss\ $\Phi_4$ has a single untimed transition, to which we
refer as $\tau_{00}$.

As the well-founded domain, we take $(\IN^2,\succ)$, the domain of
lexicographic pairs. The auxiliary assertions, helpful transitions,
time increments, and ranking functions are given by the following table:
\[\begin{array}{llll}
\varp_0\colon\quad \Ta\ge 1\quad
& \tau_0\colon\quad \tau_{00}
& \D_0\colon\quad 0
& \del_0\colon\quad 0\\[4pt]
\multicolumn{4}{l}{\varp_1\colon\quad \atl{0}\band 1\le b \le y \le
2b+1 \band t_1=0 \band \frac{y-b-1}{\sqrt{2b+1}} \le \Ta< 1}\\[2pt]
& \tau_1\colon\quad \tick
& \D_1\colon\quad \frac{1}{\sqrt{y}}
& \del_1\colon\quad (|2b+1-y|,2)\\[4pt]
\multicolumn{4}{l}{\varp_2\colon\quad \atl{0} \band 1\le b \le y \le
2b+1 \band t_1=\frac{1}{\sqrt{y}} \band \frac{y-b}{\sqrt{2b+1}} \le
\Ta< 1}\\[2pt]
& \tau_2\colon\quad \tau_{00}\quad
& \D_2\colon\quad 0
& \del_2\colon\quad (|2b+1-y|,1)\\[4pt]
\multicolumn{4}{l}{\varp_3\colon\quad \atl{0}\band 1\le b \le y \le
2b+1 \band 0<t_1<\frac{1}{\sqrt{y}} \band 0 \le \Ta< 1}\\[2pt]
& \tau_3\colon\quad \tick\quad
& \D_3\colon\quad \frac{1}{\sqrt{y}}-t_1\quad
& \del_3\colon\quad 2b+2
\end{array}\]

The idea behind this selection is the following. Starting in a state
at which $y=b\ge 1$ and $0<t_1<\frac{1}{\sqrt{y}}$ (described by
assertion $\varp_3$), we first step time with an increment
$\frac{1}{\sqrt{y}}-t_1$, this will get us to a state in which $t_1=
\frac{1}{\sqrt{y}}$ (described by $\varp_2$). From this point on, we
alternate between taking untimed transition $\tau_{00}$ which
increments $y$ by 1 but preserves time, and taking transition
\tick, which increments time by $\frac{1}{\sqrt{y}}$ but preserves the
value of $y$. We repeat this couple of steps at most $b+1$ times,
letting $y$ increase from $b$ to $2b+1$. Since the time step in each
round is decreasing, the total time increase is not less than $b+1$
times the last time increment which is $\frac{1}{\sqrt{2b+1}}$. Thus
the total time increase is not less than
\[\frac{b+1}{\sqrt{2b+1}}\ \ge \ 1,\]
where the inequality holds for every $b\ge 1$.

This informal argument can be formalized by checking that all premises
of rule \poss\ are state valid for the specified selection of the
auxiliary assertions, helpful transitions, time increments, and
well-founded ranking.

This establishes that the possibility formula
\[AG(\atl{0} \lwedge 1\le b=y \lwedge 0\le t_1\le\frac{1}{\sqrt{y}}
\lwedge 0=\Ta \quad\rar\quad EF(\Ta\ge 1))\]
is valid over \ctss\ $\Phi_4$.
\corn
\end{example}

\subsection{Possibility Diagrams}
Proofs according to rule \poss\ can be succinctly represented by
\emm{possibility diagrams}. 

A possibility 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. In addition to the assertion, each node is also labeled
by a ranking function $\del$.

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 an untimed transition
in the program or by a label of the form $\ftick(\D)$. We refer to an
edge labeled by $\tau$ (including the case that $\tau=\ftick$) as a
\emm{$\tau$-edge}.  All edges departing from the same node must have
the same label.  Every non-terminal node must have an edge departing
from it. 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$ and ranking
function $del$. Let $\varp_1,\ldots,\varp_k$, $k> 0$, be the
successors of $\varp$ by edges departing from $\varp$ (possibly including
$\varp$ itself).  With each such node, we associate the
following verification condition:
\begin{itemize}
\item If the label of all edges departing from $\varp$ is
$\ftick(\D)$, then we require the following verification conditions to
hold:
$$\hspace*{-0.5cm}\begin{array}{ll}
\mbox{P2.} & \quad \rho_{\ftick}\band T\pri= T+\D\band \varp\ \ \rar\ \ 
(\varp\pri_1 \lwedge \del \succ \del_1\pri)\band \cdots\band
(\varp\pri_k \lwedge \del \succ \del_k\pri)\\
\mbox{P3t.} & \quad \varp\ \ \rar\ \ \Om(\D)
\end{array}$$

\item If the label of all edges departing from $\varp$ is
$\tau\ne\ftick$, then we require the following verification conditions to
hold:
$$\begin{array}{ll}
\mbox{P2.} & \quad \rho_{\tau}\band T\pri= T\band \varp\ \ \rar\ \ 
(\varp\pri_1 \lwedge \del \succ \del_1\pri)\band \cdots\band
(\varp\pri_k \lwedge \del \succ \del_k\pri)\\
\mbox{P3n.} & \quad \varp\ \ \rar\ \ \emm{En}(\tau)
\end{array}$$

\end{itemize}

\ssb{Valid Possibility Diagrams}
A possibility 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 $P$-state valid.

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

\begin{claim}
\label{validposs}
If $D$ is a $\Phi$-valid possibility diagram with nodes
$\varp_0,\ldots,\varp_m$, then
\[\Phi\models AG\bigl({\bigvee_{j=0}^m}\ \varp_j\ \ \rar\ \ EF \varp_0\bigr)\]
If, in addition, $\varp_0= q$, and
\[p\ \ \rar\ \ \displaystyle{\bigvee^m_{j=0}}\ \varp_j,
\]
then we can conclude:
\[\Phi\models AG(p\ \ \rar\ \ EF q).\]
\end{claim}

\begin{example}\quad
In \Figr{poss1}, we present a waiting diagram that establishes the
possibility property
\[AG(\atl{0} \lwedge 1\le b=y \lwedge 0\le t_1\le\frac{1}{\sqrt{y}}
\lwedge 0=\Ta \quad\rar\quad EF(\Ta\ge 1))\]
for system $\Phi_4$.
\begin{figure}[hbt]
\begin{center}
\leavevmode 
\input poss1.pstex_t
\caption{\label{poss1} A possibility diagram, establishing the formula}
$AG(\atl{0} \lwedge 1\le b=y \lwedge 0\le t_1\le\frac{1}{\sqrt{y}}
\lwedge 0=\Ta \quad\rar\quad EF(\Ta\ge 1))$
\end{center} 
\end{figure}
\corn
\end{example}

\subsection{Proving that $\Phi_4$ is Non-Zeno}
We conclude this discussion by applying rule \nonz\ to show that
\ctss\ $\Phi_4$ is non-zeno.

As the assertion $\varp$ required by rule \nonz, we take
\[\varp\colon\quad \atl{0}\band y\ge 1 \band 0\le
t_1\le\frac{1}{\sqrt{y}}.\]
	
It is not difficult to show by rule \acc\ that $\varp$ is
$\Phi_4$-state valid. This establishes premise N1 of rule \nonz.

For premise N2 of \nonz, we have to verify the possibility formula
\[AG(\atl{0}\lwedge y\ge 1 \lwedge 0\le t_1\le\frac{1}{\sqrt{y}}
\lwedge y=b \lwedge \Ta=0 \quad\rar\quad EF(\Ta\ge 1)).\]
This is essentially done in Example~\ref{provpos}.

We conclude that \ctss\ $\Phi_4$ is non-zeno.