\input zmdefs

%hybrid chapter-from Amir

\font\amsy=msbm10 
\newcommand\cont{\emm{cont}}
\newcommand\contc{}
\def\contc(#1,#2){\triple(#1,\emm{cont},#2)}
\newcommand\stgf{}
\def\stgf(#1,#2,#3,#4,#5,#6){\lan \pi:\{\ell_{#1},m_{#2,1}\}\spcomma
x:#3\spcomma y:#4\spcomma z:#5\spcomma T:#6\ran}
\newcommand\pri{^{\prime}}
\newcommand\hybt{{\sc hyb-t}}
\newcommand\lscr{\ell}
\newcommand\tabb{\\ }
\newcommand\sthf{}
\def\sthf(#1,#2,#3,#4,#5,#6){\lan \pi:\{\ell_{#1},m_{#2}\}\ \; \spcomma
x:#3\spcomma y:#4\spcomma z:#5\spcomma T:#6\ran}

%  Definitions for cat-and-mouse
\newcommand\iniset{$x_c:=X_0,\; x_m:=X_0$}
\newcommand\mous{{\em Mouse}}
\newcommand\mouse{{\em Mouse}}
\newcommand\cat{{\em Cat}}
\newcommand\dldl{$[\Delta,\Delta]$}
\newcommand\eqm{\mbox{$\dot{x}_m=-v_m$}}
\newcommand\eqc{\mbox{$\dot{x}_c=-v_c$}}
\newcommand\xmw{$x_m=0$}
\newcommand\xcw{$x_c=0$}
\newcommand\fmeet{$X_0 > x_c=x_m>0$}
\newcommand\mwin{\mbox{\em Mouse-Wins}}
\newcommand\cwin{\mbox{\em Cat-Wins}}
\newcommand\cex{$w={\bf cat}$}
\newcommand\mex{$x_c=0$}
\newcommand\start{{\em Start}}
\newcommand\rest{{\em rest}}
\newcommand\run{{\em run}}
\newcommand\safe{{\em safe}}
\newcommand\bV{\widehat{V}}
\newcommand\bE{\widehat{\cE}}
\newcommand\bigand[1]{{\displaystyle \bigwedge_{#1}}}
\newcommand\vovj{V_{\overline{J}}}
\newcommand\xhat{\widehat{x}}
\newcommand\pref[1]{(\ref{#1})}
\newcommand\idle{{\bf idle}}
\newcommand\oftb{\oft{$\bullet$}}
\newcommand\delay{{\bf delay}}
\newcommand\ORop{\bigsqcup}
\newcommand\untilc{\hskip 1.5pt\hbox{\sf U}\hskip 0.5pt}
\newcommand\whilec{{\bf while}}
\newcommand\doc{{\bf do}}
\newcommand\awaitcn{{\bf await}}
\newcommand\cwinv{\emm{c\_wins}}
\newcommand\mwinv{\emm{m\_wins}}
\def\catt{\mbox{\em C}}
\newcommand\emmM{\emm{M}}
\newcommand\emmC{\emm{C}}
\newcommand\eqnar[1]{\begin{eqnarray*}#1\end{eqnarray*}}
\newcommand\atlp[1]{{\em at}\pri_-\ell_{#1}}
\newcommand\atmp[1]{{\em at}\pri_-m_{#1}}
\newcommand\band{\ \wedge\ }
\newcommand\sand{\;\wedge\;}
\newcommand\Mrestorun{\emm{M}.\mbox{\emm{rest-run}}}
\newcommand\Crestorun{\emm{C}.\mbox{\emm{rest-run}}}
\newcommand\Mruntosafe{\emm{M}.\mbox{\emm{run-safe}}}
\newcommand\Mwin{\emm{M}.\emm{win}}
\newcommand\Cwin{\emm{C}.\emm{win}}
\newcommand\Msafe{\emm{M}.\emm{safe}}
\newcommand\Mrun{\emm{M}.\emm{run}}
\newcommand\Crun{\emm{C}.\emm{run}}
\newcommand\Mrest{\emm{M}.\emm{rest}}
\newcommand\Crest{\emm{C}.\emm{rest}}
\newcommand\Active{\emm{Active}}
%-----------
\newcommand\supon{^{\emm{on}}}
\newcommand\supoff{^{\emm{off}}}
\newcommand\eqn[1]{\begin{eqnarray*} #1 \end{eqnarray*}}

%-----------
\newcommand\GF{\hbox{\raise 1.6pt \hbox{$\varphi$}}}
\newcommand\GP{\hbox{\raise 1.6pt \hbox{$\psi$}}}
\newcommand\GH{\hbox{\raise 1.6pt \hbox{$\chi$}}}
\newcommand\beqn{\begin{equation}}
\newcommand\eeqn{\end{equation}}
%\newcommand\mtxr{{\sc mutex$_r$}}
\newcommand\mtx{{\sc mutex}}
\newcommand\mtxlu{{\sc mutex$_{[L,U]}$}}
\newcommand\anyy{\mbox{\sc any-y}}
\newcommand\anyr{{\sc any-y$_{\mbox{\tiny T}}$}}
\newcommand\anyh{{\sc any-y$_{h}$}}
\newcommand\ttss{{\sc tts}}
\newcommand\ctss{{\sc cts}}
\newcommand\fts{{\sc fts}}
\newcommand\pts{{\sc pts}}
\newcommand\spl{{\sc spl}}
%\newcommand\Phia{\mbox{$\Phi_{\mbox{\tiny ANY-Y}}$}}
\newcommand\Fsysa{\mbox{$\Fsys_{\mbox{\tiny ANY-Y}}$}}
%\newcommand\Phiar{\mbox{$\Phi_{\mbox{\tiny ANY-Y}_{_T}}$}}
\newcommand\Phiah{\mbox{$\Phi_{\mbox{\tiny ANY-Y}_h}$}}
\newcommand\triple{}
\def\triple(#1,#2,#3){\{#1\}\,#2\,\{#3\}}
\newcommand\binv{{\sc b-inv}}
\newcommand\inv{{\sc inv}}
\newcommand\cinv{{\sc c-inv}}
\newcommand\hinv{{\sc h-inv}}
\newcommand\monG{{\sc mon}-$\G$}
\newcommand\atl[1]{\mbox{${\it at}_-\ell_{#1}$}}
\newcommand\atm[1]{\mbox{${\it at}_-m_{#1}$}}
\newcommand\ltl{\sc ltl}
\def\lan{\langle}
\def\ran{\rangle}
\newcommand\pair[2]{\mbox{$\lan #1,#2\ran$}}
\newcommand\xdot{\dot{x}}
\newcommand\tdom{{\sf R}^{+}}
\newcommand\tdominf{{\sf R}^{\infty}}
\newcommand\Tau{{\cal T}}
\newcommand\cD{{\cal D}}
\newcommand\cV{{\cal V}}
\newcommand\cS{{\cal S}}
\newcommand\cA{{\cal A}}
\newcommand\cI{\mbox{$\cal I$}}
\newcommand\Taut{\Tau_{T}}
\newcommand\Taup{\Tau_{\Phi}}
\newcommand\Tauh{\Tau_{H}}
\newcommand\reals{{\sf R}}
\newcommand\nats{{\sf N}}
\newcommand\realsinf{{\sf R\sp{\infty}_{\geq 0}}}
\newcommand\emm[1]{{\em#1\/}}
\newcommand\cT{\mbox{$\cal T$}}
%\newcommand\Vd{V_d}
\newcommand\Vd{D}
\newcommand\Vc{V_c}
\newcommand\Vi{I}
\newcommand\rot{\rho_\tau}
\newcommand\rotick{\rho_{\scriptstyle \stick}}
\newcommand\varphit{\varphi_{\scriptstyle \stick}}
%\newcommand\rotickm{\rho_{\scriptstyle \stickm}}
\newcommand\rotickp{\rho_{\scriptstyle \stickp}}
\newcommand\rophase{\rho_{\scriptstyle \sphase}}
\newcommand\varphip{\varphi_{\scriptstyle \sphase}}
\newcommand\rophasem{\rho_{\scriptstyle \sphasem}}

\newcommand\Enc[1]{En_{I}(#1)}
\newcommand\true{\mbox{\sc t}}
\newcommand\scT{\mbox{\sc t}}
\newcommand\scF{\mbox{\sc f}}
\newcommand\ssb{\subsubsection*}
\newcommand\sig{\sigma}
\newcommand\Sig{\Sigma}
\newcommand\The{\Theta}
\newcommand\tick{\mbox{\em tick}}
%\newcommand\tickm{\mbox{\em tick-max}}
\newcommand\tickp{\mbox{\em tick-prog}}
\newcommand\ssphase{{\scriptstyle phase}}
\newcommand\ssphasem{{\scriptstyle phase-max}}
\newcommand\sstick{{\scriptstyle tick}}
\newcommand\phase{\mbox{\em phase}}
\newcommand\phasem{\mbox{\em phase-max}}
\newcommand\stick{\em tick}
%\newcommand\stickm{\em tick-max}
\newcommand\stickp{\em tick-prog}
\newcommand\sphase{\em phase}
\newcommand\sphasem{\em phase-max}
\newcommand\lwedge{\,\wedge\,}
\newcommand\lvee{\,\vee\,}
\newcommand\bor{\ \vee\ }
\newcommand\sV{\widetilde{V}}
\newcommand\sTheta{\widetilde{\Theta}}
\newcommand\sTau{\widetilde{\Tau}}
\newcommand\sPhi{\widetilde{\Phi}}
\newcommand\cJ{{\cal J}}
\newcommand\cC{{\cal C}}
\newcommand\scJ{\widetilde{\cJ}}
\newcommand\scC{\widetilde{\cC}}
%\newtheorem{proposition}{Proposition}
\newtheorem{claim}{Claim}
%\newtheorem{example}{Example}
\newtheorem{corollary}[claim]{Corollary}
\newcommand\cPhi{\mbox{\it Comp\/}(\Phi)}
\newcommand\csPhi{\mbox{\it Comp\/}(\sPhi)}
\newcommand\rPhi{\mbox{\it Run\/}(\Phi)}
\newcommand\rsPhi{\mbox{\it Run\/}(\sPhi)}
\newcommand\bold[1]{\mbox{\bf #1}}
\newcommand\PLL{\mathop{\hbox{\vrule height 12pt depth 6pt width .5pt\kern 3pt
  \vrule height 12pt depth 6pt width .5pt}}\limits}
\newcommand\spcomma{,\,}
\def\lrar{\longrightarrow}
\newcommand\olr[1]{\buildrel #1\over\lrar}

\newcommand\strc{}
\def\strc(#1,#2,#3,#4){\lan \pi:\{\ell_#1\spcomma
m_#2\}\spcomma x:#3\spcomma y:#4\ran}

% Verification Diagrams
\newcommand\vrphia{$\varphi_1:$}
\newcommand\vrphib{$\varphi_2:$}
\newcommand\vrphik{$\varphi_k:$}
\newcommand\vrphi{$\varphi$}
\newcommand\ta{$\tau$}
\newcommand\atla{$\varphi_1:\ x = 0 \wedge \atl{0,1}$}
\newcommand\atma{$\varphi_2:\ \atm{1}$}
\newcommand\ma{$m_0$}
\newcommand\maa{$m_0:$}
\newcommand\mc{$m_2$}
\newcommand\xz{$x = 0$}
\newcommand\la{$\ell_0$}
\newcommand\lb{$\ell_1$}
\newcommand\lc{$\ell_1$}

% TTS figures

\newcommand\tts{\sc{tts:}}
\newcommand\cts{\sc{cts:}}
\newcommand\zz{$[0,0]$}
\newcommand\cond{$c$}
\newcommand\ncond{$n_1\colon\neg c$}
\newcommand\condtz{$c/t:=0$}
\newcommand\tlu{$t \leq u$}
\newcommand\tlua{\shortstack{$n_1:$\\$t \leq U$}}
\newcommand\condl{$c \wedge t \geq l$}
\newcommand\lu{$[L,U]$}
\newcommand\tgl{$t \geq L/ t:= 0$}
\newcommand\tz{$/t:=0$}
\newcommand\tglb{$b\wedge c\wedge t \geq L\,/\, t:= 0$}
\newcommand\tlub{$n_1\colon b=c \wedge (\neg c \vee t\le U)$}

% Real time verification diagrams
\newcommand\exra{$\varphi_3: \atl{0,1} \wedge \atm{0} \wedge x=0
\wedge t_1\le 5 \wedge t_2 = T \leq 5$}
\newcommand\exrb{$\varphi_2: \atl{1} \wedge T \leq 5+t_1 \leq 10$}
\newcommand\exrc{$\varphi_1: \atl{0} \wedge T \leq 10 + t_1 \leq 15$}
\newcommand\exrd{$\varphi_0: \atl{2} \wedge \atm{1}$}
\newcommand\exrcoma{$\atm{1}, x = 1$}
\newcommand\exrcomb{$t_1, t_2, T \ge 0$}
%% diagram respanyy
\newcommand\nexra{$\begin{array}{c}
\phi_3: \atl{0,1} \wedge \atm{0} \wedge x=0
\wedge t_1\le 5 \wedge t_2 \leq 5\\
\bet\colon\ t_2\le 5\end{array}$}
\newcommand\nexrb{$\phi_2: \atl{1}$}
\newcommand\nexrc{$\phi_1: \atl{0}$}
\newcommand\nexrd{$\varphi_0=\phi_0: \atl{2}\lwedge\atm{1}$}
\newcommand\nexrcoma{$\atm{1}, x = 1, t_1\le 5,\ \bet\colon\ t_1\le 5$}
%%
\newcommand\awaita{$\neg c \vee t \leq U$}
\newcommand\awaitb{$c \wedge t \geq L$}

% Hybrid Systems example

\newcommand\exha{$x = -1 / x:= 1$}
\newcommand\exhb{$x \geq -1$}
\newcommand\exhc{$\dot{x} = -1$}
\newcommand\exhd{$x = 1$}
\newcommand\tha{$0$}
\newcommand\thb{$1$}
\newcommand\thc{$2$}
\newcommand\thd{$3$}
\newcommand\thde{$4$}
\newcommand\thx{x}
\newcommand\thT{T}

% Hybrid any-h
\newcommand\hsa{$x<1 \wedge 1 \leq z \leq 5 $}
\newcommand\hsb{$/z:=0 $}
\newcommand\hsc{$1\leq z \leq 5 $}
\newcommand\hsd{$/ y:= y+1, z:= 0 $}
\newcommand\hse{$x\geq 1 \wedge 1 \leq z \leq 5 $}
\newcommand\hsf{$\dot{T}=\dot{z}=1$}
\newcommand\mab{$\dot{x} = 0.2$}
\newcommand\xyzt{Initially +$x=y=z=T=0$}
\newcommand\xone{$x = 1$}

% proof diagram for cat and mouse
\newcommand\pdcma{$\varphi_0: \quad\Mrest \lwedge \Crest \lwedge x_c=x_m=X_0
	\lwedge T=0 $}
\newcommand\pdcmb{$\varphi_1: \left(\begin{array}{c}
		\Mrun\lwedge\Crest\lwedge 0 \leq T\leq\Delta\\
		\wedge\\
		x_c=X_0\lwedge x_m=X_0-v_m\cdot T
		\end{array}\right ) $}
\newcommand\pdcmc{$\varphi_2:\left ( \begin{array}{c}
		\Mrun\lwedge \Crun\lwedge \Delta \leq T \leq t_m\\
		\wedge \\
		x_c=X_0-v_c\cdot(T-\Delta)>x_m=X_0-v_m\cdot T
		\end{array}\right )$}
\newcommand\pdcmd{$\varphi_3:\quad (\Msafe \lvee \Mwin)\lwedge x_m=0$}
\newcommand\pdcme{\Mrestorun}
\newcommand\pdcmf{\Crestorun}
\newcommand\pdcmg{\Mruntosafe}
\newcommand\pdcmh{\Mruntosafe}
\newcommand\Del{\Delta}
\newcommand\comment[1]{}
%\newcommand\splr{{\sc spl-r}}
\newcommand\splr{{\sc spl$_{\mbox{\tiny T}}$}}
\newcommand\varp{\varphi}

%\newcommand\makeatletter{\catcode`\@=11\relax}
%\newcommand\makeatother{\catcode`\@=12\relax}

\makeatletter

\def\@fnsymbol#1{\ifcase#1\or\star\or{\dagger}\or{\ddagger}%
   \or \dagger\or \ddagger\or
   \mathchar "278\or \mathchar "27B\or \dagger\or **\or \dagger\dagger
   \or \ddagger\ddagger\else\@ctrerr\fi\relax}

\makeatother
\newcommand\nin{\noindent}
\newcommand\mtl{{\sc mtl}}
\newcommand\tlg{\mbox{{TL$_{\Gamma}$}}}
\newcommand\opH{\boxM}
\newcommand\boxa[1]{\makebox[2.0cm][l]{#1}}
\newcommand\tauI{\tau_{_I}}
\newcommand\corn{\ \lower %5pt
2pt\hbox{\hskip 4pt\vrule width 3pt height 1pt depth
  1pt\hbox{\vrule width 2pt height 4.5pt depth 1pt}}}        % end of
							     % def
\newcommand\Pt{P_T}
\newcommand\anyyt{{\sc \pname}$_T$}
\newcommand\splt{{\sc spl}$_T$}
\newcommand\pname{any-y}
\newcommand\parno{\par\noindent}
\newcommand\pres{\emm{pres}}
\newcommand\sense{\emm{sense}}
\newcommand\wtV{\widetilde{V}}
\newcommand\wtU{\widetilde{U}}
\newcommand\wtTheta{\widetilde{\Theta}}
\newcommand\wtTau{\widetilde{\Tau}}
\newcommand\wtPi{\widetilde{\Pi}}
\newcommand\dclx{{\bf $x\colon$ integer where $x=0$}}
\newcommand\sit{}
\def\sit(#1,#2,#3){\lan \pi\colon\{\ell_0,m_{#1}\},\, x\colon #2;\
T\colon #3 \ran}
\newcommand\labelA{\shortstack{$\ell_0\colon$\\$b=x \lwedge(x\ne 0
\vee t_1 \leq 2)$}}
\newcommand\dclxbt{{\bf $x, b\colon$ integer where $x= b = 0$}}
\newcommand\mst{}
\def\mst(#1,#2,#3,#4,#5,#6,#7){\lan \pi\colon\{\ell_{#1},m_{#2}\},\, x\colon
#3,\, b\colon #4,\, t_1\colon #5, t_2\colon #6%,\, T\colon #7
\ran}
\def\nmodels{\mathop{\models\hskip -8pt /}\,}
\newcommand\ovlr[2]{\buildrel #1\over{\vlrar{#2}}}
\newcommand\vlrar[1]{\setlength{\unitlength}{0.012500in}
\begin{picture}(#1,4)(0,0)
\put(0,2){\vector(1,0){#1}}
\end{picture}}
\newcommand\anyce{\anyy$_{[3,5]}$}
\newcommand\medn{\par\medskip\nin}
\newcommand\Gmon{{\sc $\G$-mon}}
%\newcommand\elabinp{\{\ell_0,\ell_1\}\cap\pi\ne\phi}
%\newcommand\elabinpp{\{\ell_0,\ell_1\}\cap\pi\pri\ne\phi}
\newcommand\elabinp{(\ell_0\in\pi\vee\ell_1\in\pi)}
\newcommand\elabinpp{(\ell_0\in\pi\pri\vee\ell_1\in\pi\pri)}
\newcommand\atn{\mbox{${\it at}_-$}}
%% Added for Ctsl
\newcommand\Om{\Omega}
\newcommand\Tautp{\Tau_{T}^+}
\newcommand\wtDelta{\widetilde{\Delta}}
\newcommand\floor[1]{\lfloor #1\rfloor}
\newcommand\bfloor[1]{\left\lfloor #1\right\rfloor}
\newcommand\ceiling[1]{\lceil #1\rceil}
\newcommand\St{.}
\newcommand\D{\Delta}
\newcommand\wtD{\widetilde{\D}}
\newcommand\maximal{{\it maximal}}
\newcommand\dcla{\begin{tabular}{rl}
$y\colon$ & {\bf integer where $y=0$}\\
$t, T\colon$ & {\bf real where $t=T=0$}
\end{tabular}}
\newcommand\sta{}
\def\sta(#1,#2){\lan \pi\colon 0\,,\, y\colon #1\,,\, t\colon #2\,,\,
T\colon #2\ran}
\newcommand\stb{}
\def\stb(#1,#2){\lan \pi\colon #1\,,\, t\colon #2\,,\, T\colon #2\ran}
\newcommand\stc{}
\def\stc(#1,#2,#3){\lan \pi\colon #1\,,\, y\colon #2\,,\, t\colon #3\,,\,
T\colon #3\ran}
\newcommand\size[1]{|#1|}
\newcommand\om{\omega}
\newcommand\entails{\mathrel{\Rightarrow}}
\newcommand\implies{\mathrel{\to}}
\newcommand\wts{\widetilde{s}}
\newcommand\wtsig{\widetilde{\sig}}
\newcommand\Claimr[1]{Claim~\ref{#1}}
\newcommand\Fsys{F}
\newcommand\Fsysp{\Fsys_{_P}}
\newcommand\Ascr{{\cal A}}
\newcommand\Jscr{{\cal J}}
\newcommand\Escr{{\cal E}}
\newcommand\Tscr{{\cal T}}
\newdimen\offdimen
\def\offset#1#2{\offdimen #1
   \noindent \hangindent \offdimen
   \hbox to \offdimen{#2\hfil}\ignorespaces}
\newcommand\oft{\offset{20pt}}
\newcommand\ofi{\offset{50pt}}
\newcommand\IN{\hbox{\amsy\char'116}}
\newcommand\medno{\medskip\noindent}
\newcommand\ctrline[1]{\begin{center} #1 \end{center}}
\newcommand\subsec{\subsection}
\newcommand\Figr[1]{Fig.~\ref{#1}}
\newcommand\sbseq{\subseteq}
\newcommand\rar{\rightarrow}
\newcommand\del{\delta}
\long\def\Lbox#1{\Xbox{12}{#1}}
\long\def\LLbox#1{\Xbox{50}{#1}}
\long\def\Sbox#1{\Xbox{0}{#1}}
\long\def\Xbox#1#2{\par
  {%\lskip
\setbox 0=\vbox{\advance \hsize -#1truept\HSIZE\hsize%\vskip 5pt
  \vbox{\hrule height 0pt width \hsize \relax #2\par}%\vskip 5pt
}
  \centerline{\vbox{\hrule\hbox{\vrule\hskip 5pt\box 0\hskip 5pt\vrule}
  \hrule}}}}
%\def\lskip{\vskip %4truept
%0pt}
\def\HSIZE{\afterassignment\SetFsizeFskip\hsize}
\hsize \textwidth
\newdimen\fskipindent                         % indentation of equations
\newdimen\fsizex                              % \hsize -\rightskip
\newdimen\fskip                               % \leftskip +\fskipindent
\newdimen\fsize                               % \fsizex -\fskipindent
\fskipindent=50pt
\def\SetFsizeFskip{\fsizex=\hsize\advance\fsizex -\rightskip\fskip=
  \leftskip\advance\fskip\fskipindent\fsize=\fsizex\advance\fsize
  -\fskipindent}
\SetFsizeFskip
\def\boxpar#1{\noindent #1\par}
\def\boxline#1{\vskip 1pt %\line{#1\hfil}
\begin{flushleft} #1 \end{flushleft}
}
\def\lskip{\vskip 8pt}
\def\lft#1{{#1}\hfill}
\def\ctr#1{\hfill{#1}\hfill}
\def\rt#1{\hfill{#1}}
\def\({[}
\def\){]}
\newcommand\Rar{\Rightarrow}
\newcommand\ctrlined[2]{\caption{\label{#1}#2}\end{figure}}
\newcommand\reactw{{\sc react-w}}
\newcommand\pos{{\ \;}}
\newcommand\Sgp{\Sigma^+}
\newcommand\GHp{\GH_p}
\newcommand\ifff{\;\Longleftrightarrow\;}
\newcommand\cF{{\cal F}}
\newcommand\sg{\sigma}
\newcommand\cL{{\cal L}}
\newcommand\dz{\D_\sqsupset}
\newcommand\ml{\{1,...,m\}}
\newcommand\Bar{\noalign{\vskip 5pt\hrule\vskip 7pt}}
\newcommand\Ruleb[1]{\centerline{\vbox{\halign{\lft{##}\cr #1\crcr}}}}
\newcommand\accp{\emm{acc}_{_P}}
\newcommand\accpp{\emm{acc}_{p,_P}}
\newcommand\wh[1]{\widehat{#1}}
\newcommand\ls{l_{_S}}
\newcommand\us{u_{_S}}
\newcommand\pll{\Vert}
\newcommand\wttau{\wt{\tau}}
\newcommand\wt[1]{\widetilde{#1}}
\newcommand\cbchain{{\sc cb-chain}}
\newcommand\cbwell{{\sc cb-well}}
\newcommand\clk{c}
\newcommand\bnd{b}
\newcommand\Bnd{B}
\newcommand\bigmaca{$\atm{7,8}$}
\newcommand\bigmacb{$\atm{9}\lwedge t_1\ge t_2$}
\newcommand\bigmacc{$\atm{10}\lwedge t_1\ge t_2+L$}
\newcommand\bigmacd{$\atm{7}\lwedge t_1\ge t_2$}
\newcommand\bigmace{$\atm{8}\lwedge t_1\ge t_2+L$}
\newcommand\bet{\beta}
%% Macro's for bigmac2
\newcommand\bigmacf{$\atm{0}\lwedge t_1\ge t_2$}
\newcommand\bigmacg{$\atm{1}\lwedge t_1\ge t_2+L$}
\newcommand\bigmach{$\atm{0,1}$}
\newcommand\bigmaci{$\atm{2}\lwedge t_1\ge t_2$}
\newcommand\bigmacj{$\atm{3}\lwedge t_1\ge t_2+L$}
\newcommand\bigmack{$\atm{0..3}$}
\newcommand\bigmacl{$\atm{4}\lwedge t_1\ge t_2$}
\newcommand\bigmacm{$\atm{5}\lwedge t_1\ge t_2+L$}
%%
\newcommand\scor{{\sc or}}
\newcommand\scand{{\sc and}}
\newcommand\race{{\sc race}}
\newcommand\Ta{T_a}
\newcommand\chaintwom{$\phi_0\colon\ \atl{8}\bor (\atl{4,6,7} \lwedge
\atm{6} \lwedge x=2\lwedge t_2=0)$}
\newcommand\cyclic{{\sc cyclic}}
\newcommand\W{\unless\,}
\newcommand\wait{{\sc wait}}
\newcommand\Sys{P}
\newcommand\vmodels{\,\mathop{\raise -2.5pt% 13.10.95 A.P.
\hbox{\vrule height 10pt width 0.5pt}\hskip
  -3pt\models}\hskip 0.5pt}
\newcommand\acc{{\sc acc}}
\newcommand\Um{U_m}
\newcommand\Phida{$\ell_0\colon\ t_1< \frac{1}{\sqrt{y}}$}
\newcommand\Phidb{$(y,t_1) := (y+1,0)$}
\newcommand\nonz{{\sc nonz}}
\newcommand\tl{{\sc tl}}
\newcommand\ctl{{\sc ctl}}
\newcommand\poss{{\sc poss}}
\newcommand\gposs{{\sc g-poss}}
\newcommand\Nextf{\emm{Next}}
\newcommand\Phiea{$\ell_0\colon\ T<1$}
\newcommand\Phieb{$\ell_1\colon$}
\newcommand\nexta{}
\def\nexta(#1,#2){(\pi\pri:\, #1,\;T\pri:\, #2)}
\newcommand\tdctss{{\sc td-ctss}}
\newcommand\ftick{\emm{tick}}
%% labels for poss1.fig
\newcommand\possaa{$\atl{0},\ 1\le b\le y\le 2b+1,\ t_1\ge 0,\ 0\le \Ta<1$}
\newcommand\possab{$\varp_3\colon\ 0<t_1<\frac{1}{\sqrt{y}} \qquad
\del\colon\ 2b+2$}
\newcommand\possac{$\varp_2\colon\ t_1=\frac{1}{\sqrt{y}} \band \Ta\ge
\frac{y-b}{\sqrt{2b+1}} \qquad \del\colon\ (|2b+1-y|,1)$}
\newcommand\possad{$\varp_1\colon\ t_1=0\band \Ta\ge
\frac{y-b-1}{\sqrt{2b+1}} \qquad \del\colon\ (|2b+1-y|,2)$}
\newcommand\possae{$\varp_0\colon\ \Ta\ge 1 \qquad \del\colon\ 0$}
\newcommand\possaf{$\ftick(\frac{1}{\sqrt{y}}-t_1)$}
\newcommand\possag{$\tau_{00}$}
\newcommand\possah{$\ftick(\frac{1}{\sqrt{y}})$}
\newcommand\possai{$\ftick(\frac{1}{\sqrt{y}})$}
%%
\newcommand\updn{{\sc up-down}}
\newcommand\tables{\ \quad}
\newcommand\move{\emm{move}}
%% labels for ranked1.fig
\newcommand\rankedaa{$t_2, T\ge 0,\ 0\le t_1\le U$}
\newcommand\rankedab{$\phi_5\colon\ \atl{0,1}\lwedge \atm{0} \lwedge
x=0 \lwedge y \ge 0,\quad \bet\colon\ t_2\le 5,\quad \del\colon\ 4$}
\newcommand\rankedac{$\atm{1},\ x=1,\ y\ge 0,\qquad \bet\colon\ t_1\le
U$}
\newcommand\rankedad{$\phi_4\colon\ \atl{1},\qquad \del\colon\ 3$}
\newcommand\rankedae{$\phi_3\colon\ \atl{0},\qquad \del\colon\ 2$}
\newcommand\rankedaf{$\atm{1},\ x=1,\ y\ge 0,\qquad \bet\colon\ t_1\le
U$}
\newcommand\rankedag{$\phi_2\colon\ \atl{2},\qquad \del\colon\
(1,2y+1)$}
\newcommand\rankedah{$\phi_1\colon\ \atl{3}\lwedge y>0,\qquad \del\colon\
(1,2y)$}
\newcommand\rankedai{$\phi_0\colon\ \atl{4}\lwedge\atm{1},\qquad
\del\colon\ 0$}
%%
\newcommand\WtoR{W$\to$R}
\newcommand\updnae{\updn$_{[1,5]}$}
%% labels for wait2.fig
\newcommand\waitba{$y\ge 0,\ \Ta\ge 0,\ 0\le t_1\le 5,\ 0\le t_2\le 5$}
\newcommand\waitbc{$\atm{1},\ x=1$}
\newcommand\waitbd{$\atl{1}\lwedge y\le 2\lwedge \Ta\le 5+t_1\le 10$}
\newcommand\waitbe{$\atl{0}\lwedge y\le 3\lwedge \Ta\le 10+t_1\le 15$}
\newcommand\waitbf{$\atm{1},\ x=1,\ y\le 3$}
\newcommand\waitbg{$\atl{2}\lwedge \Ta\le 45-10y+t_1\le 50-10y$}
\newcommand\waitbh{$\atl{3}\lwedge y>0 \lwedge \Ta\le 50-10y+t_1\le 55-10y$}
\newcommand\waitbi{$\atl{4}\lwedge \Ta\le 50$}
\newcommand\waitbj{$\atm{0},\ x=0,\ \Ta\le t_2\le 5$}
\newcommand\waitbk{$\atl{0}\lwedge (y=0 \lvee 2y+t_1\le \Ta+1)$}
\newcommand\waitbl{$\atl{1}\lwedge 2y+t_1\le \Ta$}
%%
