\documentclass[a4paper,12pt]{article}
\bibliographystyle{plain}
\addtolength{\topmargin}{-1cm}
\addtolength{\oddsidemargin}{-1cm}
\addtolength{\evensidemargin}{-1cm}
\addtolength{\textheight}{2cm}
\addtolength{\textwidth}{2cm}
\renewenvironment{abstract}{\begin{list}{}
			{\rightmargin\leftmargin
			\listparindent 1.5em
			\parsep 0pt plus 1pt}
			\small\item {\bf Abstract:}}{\end{list}}

\title{\bf On Specifying Timeouts\thanks{Partly based on joint work with
    Frits Vaandrager.}}

\author{Rob van Glabbeek\\
\footnotesize National ICT Australia\\[-5pt]
\footnotesize and School of Computer Science and Engineering\\[-5pt]
\footnotesize The University of New South Wales\\[-5pt]
\footnotesize {\tt rvg@cs.stanford.edu}}
\date{}
\begin{document}
\maketitle
\pagestyle{empty}
\thispagestyle{empty}
\begin{abstract}
This paper raises the question on how to specify timeouts in process
algebra, and finds that the basic formalisms fall short in this task.
\end{abstract}
Consider the following protocol for a mail server:
\begin{quote}
Set a timer for an unspecified but finite amount of time, and try to
send a message again and again until it either succeeds or the timer
goes off. In the latter case return an error message.
Optionally, someone may deactivate the timer before it goes off, in
which case the system may run forever.
\end{quote}
My question is how to model this simple protocol by means of process
algebra. Even though languages like CCS, CSP and ACP and their many
variants have been around for twenty five years, it is still
particularly tricky to do so.  As this problem didn't specify any
real-time constraints it appears less natural to use a real-time
process algebra. The specification should keep it completely open how
long each activity lasts. In particular, there is no upper bound on
the number of trials that are made before the timer goes off. Still we
know that within a finite amount of time either the message is send
successfully, or an error message is returned, unless the timer is
deactivated.

When abstracting, in part, from the timer, the process can be
specified as 
$${\tt set}\cdot\mu X.({\tt fail}\cdot X + {\tt succeed} + {\tt
timeout}\cdot {\tt error})$$
and a specification of the entire protocol (freely mixing ACCSP) could be
$${\tt set}\cdot\left(\mu X.({\tt fail}\cdot X + {\tt succeed} + {\tt
timeout}\cdot{\tt error}) \mbox{\Large$\|$}_{\tt timeout}
\tau\cdot{\tt timeout} + {\tt deactivate}\right).$$
However, this specification leaves open the option that the process keeps
failing forever: the standard operational semantics of ACCSP generates
a transition system that features a path with infinitely many {\tt
fail}-actions and no {\tt deactivate} (see Figure~\ref{graph}).

\begin{figure}[htp]
\mbox{}\vspace{-1em}

%\input{graph}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \special{pn 8}%
    \special{ar 1594 722 20 20 0 6.28319}%
    \special{pa 1516 699}%
    \special{pa 1575 722}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1491 662}%
    \special{pa 1575 722}%
    \special{pa 1473 709}%
    \special{pa 1491 662}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.250in
    \rlap{\kern 1.594in\lower\graphtemp\hbox to 0pt{\hss {\tt fail}\hss}}%
    \special{ar 1594 526 197 197 0 6.28319}%
    \special{sh 0.000}%
    \special{ar 1594 722 20 20 0 6.28319}%
    \special{ar 1988 1510 20 20 0 6.28319}%
    \special{pa 1603 740}%
    \special{pa 1979 1492}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1957 1392}%
    \special{pa 1979 1492}%
    \special{pa 1912 1414}%
    \special{pa 1957 1392}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.116in
    \rlap{\kern 1.791in\lower\graphtemp\hbox to 0pt{\hss {\tt ~~~~~~succ.}\hss}}%
    \special{ar 20 1510 20 20 0 6.28319}%
    \special{pa 37 1501}%
    \special{pa 1577 731}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1476 754}%
    \special{pa 1577 731}%
    \special{pa 1499 798}%
    \special{pa 1476 754}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.116in
    \rlap{\kern 0.807in\lower\graphtemp\hbox to 0pt{\hss {\tt set~~}\hss}}%
    \special{ar 2382 722 20 20 0 6.28319}%
    \special{pa 1614 722}%
    \special{pa 2362 722}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2262 697}%
    \special{pa 2362 722}%
    \special{pa 2262 747}%
    \special{pa 2262 697}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.722in
    \rlap{\kern 1.988in\lower\graphtemp\hbox to 0pt{\hss $\tau$\hss}}%
    \special{pa 2303 699}%
    \special{pa 2362 722}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2279 662}%
    \special{pa 2362 722}%
    \special{pa 2260 709}%
    \special{pa 2279 662}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.250in
    \rlap{\kern 2.382in\lower\graphtemp\hbox to 0pt{\hss {\tt fail}\hss}}%
    \special{ar 2382 526 197 197 0 6.28319}%
    \special{sh 0.000}%
    \special{ar 2382 722 20 20 0 6.28319}%
    \special{ar 2776 1510 20 20 0 6.28319}%
    \special{pa 2391 740}%
    \special{pa 2767 1492}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2744 1392}%
    \special{pa 2767 1492}%
    \special{pa 2700 1414}%
    \special{pa 2744 1392}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.116in
    \rlap{\kern 2.579in\lower\graphtemp\hbox to 0pt{\hss {\tt ~~~~~~succ.}\hss}}%
    \special{pa 2008 1510}%
    \special{pa 2756 1510}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2656 1485}%
    \special{pa 2756 1510}%
    \special{pa 2656 1535}%
    \special{pa 2656 1485}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.510in
    \rlap{\kern 2.382in\lower\graphtemp\hbox to 0pt{\hss $\tau$\hss}}%
    \special{ar 3563 722 20 20 0 6.28319}%
    \special{pa 2402 722}%
    \special{pa 3543 722}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3443 697}%
    \special{pa 3543 722}%
    \special{pa 3443 747}%
    \special{pa 3443 697}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.722in
    \rlap{\kern 2.972in\lower\graphtemp\hbox to 0pt{\hss {\tt timeout}\hss}}%
    \special{ar 4744 722 20 20 0 6.28319}%
    \special{pa 3583 722}%
    \special{pa 4724 722}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 4624 697}%
    \special{pa 4724 722}%
    \special{pa 4624 747}%
    \special{pa 4624 697}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.722in
    \rlap{\kern 4.154in\lower\graphtemp\hbox to 0pt{\hss {\tt error}\hss}}%
    \special{ar 1594 1904 20 20 0 6.28319}%
    \special{pa 1594 742}%
    \special{pa 1594 1884}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1619 1784}%
    \special{pa 1594 1884}%
    \special{pa 1569 1784}%
    \special{pa 1619 1784}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.313in
    \rlap{\kern 1.594in\lower\graphtemp\hbox to 0pt{\hss {\tt deact.~~~~~~~}\hss}}%
    \special{pa 1571 1982}%
    \special{pa 1575 1904}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1545 2002}%
    \special{pa 1575 1904}%
    \special{pa 1595 2005}%
    \special{pa 1545 2002}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.904in
    \rlap{\kern 1.004in\lower\graphtemp\hbox to 0pt{\hss {\tt fail}\hss}}%
    \special{ar 1398 1904 197 197 0 6.28319}%
    \special{sh 0.000}%
    \special{ar 1594 1904 20 20 0 6.28319}%
    \special{ar 1988 2691 20 20 0 6.28319}%
    \special{pa 1603 1921}%
    \special{pa 1979 2673}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1957 2573}%
    \special{pa 1979 2673}%
    \special{pa 1912 2595}%
    \special{pa 1957 2573}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 2.297in
    \rlap{\kern 1.791in\lower\graphtemp\hbox to 0pt{\hss {\tt succ.~~~~~}\hss}}%
    \special{pa 1988 1530}%
    \special{pa 1988 2671}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2013 2571}%
    \special{pa 1988 2671}%
    \special{pa 1963 2571}%
    \special{pa 2013 2571}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 2.100in
    \rlap{\kern 1.988in\lower\graphtemp\hbox to 0pt{\hss {\tt ~~~~~~~deact.}\hss}}%
    \hbox{\vrule depth2.711in width0pt height 0pt}%
    \kern 4.764in
  }%
}%
\centerline{\raise 1em\box\graph}
\caption{Process graph of the ACCSP specification}
\label{graph}
\end{figure}

One solution is to invoke Koomen's Fair Abstraction Rule (KFAR)
[1] to prove, by abstraction from {\tt fail}, that either {\tt
succeed} or {\tt timeout} will happen eventually.  However, this
hinges on a global fairness assumption that is not warranted in this
example. Even if the action {\tt deactivate} occurs, KFAR allows us to
derive, contrary to the specification, that {\tt succeed} will happen
eventually.

What appears to be needed here is some kind of priority mechanism,
saying that when {\tt timeout} can occur, it takes precedence over the
alternative actions {\tt fail} and {\tt succeed}. When
performing abstraction by renaming into silent steps, priority
mechanisms are cumbersome in process algebra, because in weak and
branching bisimulation semantics the processes $a(b+c)$ and
$a.(\tau.(b+c)+b)$ are equivalent, but if $c$ has priority over $b$
one would expect that only the latter can do a $b$-step.

Even when the priority mechanism is in place, the process of
Figure~\ref{graph} still allows an infinite sequence of {\tt
fail}-actions without {\tt deactivate}, due to the interleaving of the
components in the parallel composition.
\begin{figure}[htb]
%\input{net}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \special{pn 8}%
    \special{ar 374 492 98 98 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 0.374in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 472 492}%
    \special{pa 669 492}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 630 467}%
    \special{pa 669 492}%
    \special{pa 630 517}%
    \special{pa 630 467}%
    \special{fp}%
    \special{pa 669 591}%
    \special{pa 1102 591}%
    \special{pa 1102 394}%
    \special{pa 669 394}%
    \special{pa 669 591}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 0.886in\lower\graphtemp\hbox to 0pt{\hss {\tt set}\hss}}%
    \special{pa 1102 492}%
    \special{pa 1299 492}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1260 467}%
    \special{pa 1299 492}%
    \special{pa 1260 517}%
    \special{pa 1260 467}%
    \special{fp}%
    \special{ar 1398 492 98 98 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 1.398in\lower\graphtemp\hbox to 0pt{\hss $p$\hss}}%
    \special{pa 1496 492}%
    \special{pa 1693 492}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1654 467}%
    \special{pa 1693 492}%
    \special{pa 1654 517}%
    \special{pa 1654 467}%
    \special{fp}%
    \special{pa 1693 591}%
    \special{pa 2441 591}%
    \special{pa 2441 394}%
    \special{pa 1693 394}%
    \special{pa 1693 591}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 2.067in\lower\graphtemp\hbox to 0pt{\hss {\tt timeout}\hss}}%
    \special{pa 2441 492}%
    \special{pa 2638 492}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2598 467}%
    \special{pa 2638 492}%
    \special{pa 2598 517}%
    \special{pa 2598 467}%
    \special{fp}%
    \special{ar 2736 492 98 98 0 6.28319}%
    \special{pa 2835 492}%
    \special{pa 3031 492}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2992 467}%
    \special{pa 3031 492}%
    \special{pa 2992 517}%
    \special{pa 2992 467}%
    \special{fp}%
    \special{pa 3031 591}%
    \special{pa 3622 591}%
    \special{pa 3622 394}%
    \special{pa 3031 394}%
    \special{pa 3031 591}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 3.327in\lower\graphtemp\hbox to 0pt{\hss {\tt error}\hss}}%
    \special{pa 1181 197}%
    \special{pa 1614 197}%
    \special{pa 1614 0}%
    \special{pa 1181 0}%
    \special{pa 1181 197}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.098in
    \rlap{\kern 1.398in\lower\graphtemp\hbox to 0pt{\hss {\tt fail}\hss}}%
    \special{ar 1261 281 250 250 -0.345348 0.599451}%
    \special{sh 1.000}%
    \special{pa 1486 242}%
    \special{pa 1496 197}%
    \special{pa 1533 225}%
    \special{pa 1486 242}%
    \special{fp}%
    \special{ar 1534 281 250 250 2.542141 3.486941}%
    \special{sh 1.000}%
    \special{pa 1326 376}%
    \special{pa 1328 423}%
    \special{pa 1285 404}%
    \special{pa 1326 376}%
    \special{fp}%
    \special{pa 1181 984}%
    \special{pa 1614 984}%
    \special{pa 1614 787}%
    \special{pa 1181 787}%
    \special{pa 1181 984}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 1.398in\lower\graphtemp\hbox to 0pt{\hss {\tt succ.}\hss}}%
    \special{pa 1398 591}%
    \special{pa 1398 787}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1423 748}%
    \special{pa 1398 787}%
    \special{pa 1373 748}%
    \special{pa 1423 748}%
    \special{fp}%
    \special{ar 886 1280 98 98 0 6.28319}%
    \special{pa 886 591}%
    \special{pa 886 1181}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 911 1142}%
    \special{pa 886 1181}%
    \special{pa 861 1142}%
    \special{pa 911 1142}%
    \special{fp}%
    \special{pa 1260 1378}%
    \special{pa 1693 1378}%
    \special{pa 1693 1181}%
    \special{pa 1260 1181}%
    \special{pa 1260 1378}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.280in
    \rlap{\kern 1.476in\lower\graphtemp\hbox to 0pt{\hss $\tau$\hss}}%
    \special{pa 984 1280}%
    \special{pa 1260 1280}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1220 1255}%
    \special{pa 1260 1280}%
    \special{pa 1220 1305}%
    \special{pa 1220 1255}%
    \special{fp}%
    \special{ar 2067 1280 98 98 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 1.280in
    \rlap{\kern 2.067in\lower\graphtemp\hbox to 0pt{\hss $q$\hss}}%
    \special{pa 1693 1280}%
    \special{pa 1969 1280}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1929 1255}%
    \special{pa 1969 1280}%
    \special{pa 1929 1305}%
    \special{pa 1929 1255}%
    \special{fp}%
    \special{pa 2067 1181}%
    \special{pa 2067 591}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2042 630}%
    \special{pa 2067 591}%
    \special{pa 2092 630}%
    \special{pa 2042 630}%
    \special{fp}%
    \special{pa 0 1378}%
    \special{pa 591 1378}%
    \special{pa 591 1181}%
    \special{pa 0 1181}%
    \special{pa 0 1378}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.280in
    \rlap{\kern 0.295in\lower\graphtemp\hbox to 0pt{\hss {\tt deact.}\hss}}%
    \special{pa 787 1280}%
    \special{pa 591 1280}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 630 1305}%
    \special{pa 591 1280}%
    \special{pa 630 1255}%
    \special{pa 630 1305}%
    \special{fp}%
    \hbox{\vrule depth1.378in width0pt height 0pt}%
    \kern 3.622in
  }%
}%
\centerline{\raise 1em\box\graph}
\caption{Petri net of the ACCSP specification}
\label{net}
\end{figure}
Maybe an elegant solution can be found by modelling the specification
as Petri net---see Figure~\ref{net}. Under a normal progress
assumption, provided that no {\tt deactivate} occurs, sooner or later
there will be a token in place $q$.  Now {\tt timeout} should have
priority over the actions {\tt fail} and {\tt succeed} that compete
for the token in $p$, but this priority takes effect only when there
is a token in $q$.  How to best formalise such reasoning is suggested
as topic for future research.
%\bibliography{../Stanford/lib/abbreviations,../Stanford/lib/dbase}

\begin{list}{$[1]$}{\leftmargin 18pt
                        \labelwidth\leftmargini\advance\labelwidth-\labelsep
                        \topsep 4pt \itemsep 2pt \parsep 2pt}
\item
{\sc J.C.M. Baeten, J.A. Bergstra \& J.W. Klop} (1987):
\newblock {\em On the consistency of {Koomen's} fair abstraction rule.}
\newblock {\sl Theoretical Computer Science} 51(1/2), pp. 129--176.
\end{list}
\end{document}
