\documentclass[runningheads]{llncs}
\bibliographystyle{plain}
\usepackage{epsf,amssymb,graphics,color}

\newcommand{\nc}{\newcommand}
\newcommand{\rnc}{\renewcommand}
\newfont{\fsc}{eusm10}                  % frenchscript letters
\nc {\pset}{\mbox{\fsc P}}  % powerset always in frenchscript
\nc {\Nat}{\mbox{I\hspace{-0.75mm}I\hspace{-1.15mm}N}}  % natural numbers
\nc {\step}[1]{\stackrel{#1}{\longrightarrow}}
\nc {\Step}[1]{\stackrel{#1}{\Longrightarrow}}
\nc {\postscript}[3] {\begin{figure}[b]\epsfxsize=#2
    \vspace{-1em}
    \centerline{\makebox[#2]{\epsfbox{#1.eps}}}\caption{#3}\label{#1}\end{figure}}
\nc {\infr}[2]
    {\rule{0mm}{6mm} \begin{array}{c} #1\\[0.1ex] \hline \rule{0ex}{2.7ex}#2 \end{array}}
\nc {\bis}[1]                           % bisimulation
    {\;\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}\,_{#1}\,}
\nc {\rwbisimd}{\ensuremath{\mathalpha{%
    \setbox0=\hbox{\kern-.1ex{$\leftrightarrow$}\kern-.1ex}
    \setbox1=\vbox{\hbox{\raise .1ex \box0}\hrule}%
    \ensuremath{\mathrel{\hbox{\kern.1ex\box1\kern.1ex}^{\Delta}_{\,rw}}}}}}
\nc {\F}{{\cal F}}                      % global fairness assumption
\nc {\IF}{{\cal I}}                     % possible futures of ...
\nc {\tr}{{\cal T}}                     % trace set of ...
\nc {\eqIF}{\sim_\IF}                   % possible futures equivalence
\nc {\reqIF}{=_{\IF}}                   % possible futures congruence
\nc {\act}{{\cal A}}                    % alphabet of actions
\nc {\plat}[1]{\raisebox{0pt}[0pt][0pt]{#1}}        % no vertical space
\rnc {\epsilon}{\varepsilon}            % empty string
\rnc {\phi}{\varphi}                    % formulas
\nc {\AGAFF}{{\rm AGAF}_{\!\F}}         % fair AGAF property

\title{Liveness, Fairness and Impossible Futures}
\author{Rob van Glabbeek\inst{1,2} and Marc Voorhoeve\inst{3}}
\authorrunning{R.J. van Glabbeek and M. Voorhoeve}
\institute{National ICT Australia, Sydney
  \and School of Computer Science and Engineering, The University of New South Wales
  \and Dept.\ of Mathematics and Computer Science, Eindhoven University of Technology
}
\begin{document}
\maketitle

\begin{abstract}
Impossible futures equivalence is the semantic equivalence on labelled transition systems
that identifies systems iff they have the same ``AGEF'' properties:
temporal logic properties saying that reaching a desired outcome is not doomed to fail.
We show that this equivalence, with an added root condition, is the coarsest
congruence containing weak bisimilarity with explicit divergence that respects
deadlock/livelock traces (or fair testing, or any liveness property under a global
fairness assumption) and assigns unique solutions to recursive equations.
\end{abstract}

\section{Introduction}

\postscript{gsm}{12cm}{Charts of Pete's mobile phone}

This paper deals with a class of system requirements, and related
notions of process equivalence, that we introduce by the following tale.
\\[6pt]
{\small \sf
Pete's mobile phone allows a number to be redialed
as long as connection attempts are unsuccessful.
The phone's manual charts this functionality
(Fig.\,\ref{gsm}, left hand side; {\it ok} and {\it nok} are internal actions
that cannot be observed or interacted with).
After having lost several valuable business opportunities,
Pete finds out that his redial module contains a bug.
During the redial process, data can become corrupted so that all connection attempts fail from then on.
Pete contacts his vendor for damages, who denies responsibility, since all code has been
certified by a company named TEI (Testing Equivalences Inc).
Upon contacting TEI, their spokesman says:
``We indeed have discovered the feature you complain about.
Our technical people have even charted the functionality implemented
(Fig.\,\ref{gsm}, right hand side, dashed arc omitted).
However you have nothing to complain about,
because we have verified that the two systems are
equivalent with respect to ready simulation.
This is our finest equivalence, highly recommended by concurrency specialists \cite{ArBlIsMe95}.''
Our hero is considering his next step.}

\noindent
The specification in his manual led Pete to believe that his phone satisfies the requirement:
{\sf every redial attempt \mbox{\it may} succeed}.
Of course, the attempts may fail, but attempts that are {\em doomed} to fail are not acceptable.
In CTL \cite{IPClEm81}, when taking observable histories of states as atomic propositions,
Pete's requirement may be formulated as, for all $k\!\in\!\Nat$,
{\bf AG}($(tf)^k$ has occurred $\Rightarrow$ {\bf EF} $(tf)^k tc$ has occurred).
We call such requirements \emph{AGEF properties}.
Pete's requirement is not preserved by testing equivalences
such as ready simulation \cite{ArBlIsMe95} or failures equivalence \cite{BHR84}.

\emph{AGAF properties} are (conditional) liveness requirements,
stating that (depending on past activity) some condition will eventually hold.
In Pete's case, such a requirement would be:
{\sf if I keep hitting the redial button, I will eventually be connected}.
The implementation in Fig.\,\ref{gsm} does not satisfy this AGAF property,
but it is open to debate whether the specification satisfies it.
In order to deduce that requirement, a {\em fairness} assumption is needed \cite{BoFra86}, e.g.:
{\sf in a recurring state, a specific option cannot be avoided infinitely often}.
This assumption allows to distinguish the processes in Fig.\,\ref{gsm},
even without testing the AGEF property.
We show that under a sufficiently strong fairness assumption any AGAF property can be
reformulated as a conjunction of AGEF properties.
Since the validity of AGEF properties does not depend on fairness, it
appears preferable to directly verify the AGEF requirements
rather than assume fairness and verify the AGAF requirement.
\emph{Fair testing equivalence}
\cite{IPBrReVo95} preserves the subset of \emph{testable} AGEF properties,
including the reformulated AGAF properties.
Absence of initial deadlock and livelock is an example of a testable AGEF property.
However, many reasonable requirements such as Pete's not-doomed-to-fail requirement are in fact non-testable AGEF properties.
If there is e.g.\ a possibility that the corrupted data in Pete's phone can become
uncorrupted by redialling frantically, as indicated by the dashed arc in Fig.\,\ref{gsm},
the erroneous implementation is fair testing equivalent to the specification.
However, Pete will still be far from satisfied.

In this paper we study the impossible futures (IF) equivalence of \cite{BoVog92,ArVoMa00} that
preserves all AGEF properties.  We prove that any process equivalence that is a congruence w.r.t.\
the operators of calculi like CCS and CSP either preserves all AGEF properties, all testable
properties only, or no proper AGEF property at all. Moreover, any
equivalence that preserves just the testable AGEF properties and is
coarser than weak bisimilarity with explicit divergence ($\rwbisimd$) does not respect the
\emph{recursive specification principle} (RSP), stating that solutions of guarded recursive
equations are unique.  This proof principle is of great importance in equational system verification \cite{Ba90}.
So, among the semantic equivalences coarser than $\rwbisimd$,\footnote{We were
  unable to extend our results to equivalences incomparable with both \mbox{}$\rwbisimd$
  and IF,
  preserving some AGEF property. However, no such equivalences are known.}
IF is the coarsest congruence allowing both the preservation of any chosen proper AGEF
property and equational system verification.

\section{Labelled Transition Systems}

Let $\Sigma^*$ denote the set of finite sequences over a given set $\Sigma$.
Write $\epsilon$ for the empty sequence, $\sigma\rho$ for the concatenation of sequences $\sigma$ and $\rho$, and $a$
for the sequence consisting of the single element $a \in \Sigma$.
Write $\sigma\leq\rho$ if $\sigma$ is a prefix of $\rho$, i.e.\ $\exists \nu\in
\Sigma^*\cdot\sigma\nu=\rho$, and write $\sigma<\rho$ if $\sigma\leq\rho$ and $\sigma\neq\rho$.

We presuppose a countable action alphabet $A$, not containing the
``silent'' action $\tau$ and set $A_\tau = A \cup \{\tau\}$. We assume
that our set $A$ consists of complementary pairs; each $a \in A$ has a
complement $\bar a$ such that $\bar{\bar a} = a$.

\begin{definition}\rm
A \emph{labelled transition system} (LTS) is a pair $(\mathbb{P},\rightarrow)$, where
  $\mathbb{P}$ is a set (of \emph{processes} or \emph{states}) and
  ${\rightarrow} \subseteq \mathbb{P} \times A_\tau \times \mathbb{P}$
    is a set of \emph{transitions}.

\end{definition}
Assuming a fixed transition system $(\mathbb{P},\rightarrow)$, we write $p \step a p'$ for $(p,a,p') \in {\rightarrow}$.
\plat{$p \step{a} p'$} means that process $p$ can evolve into $p'$, while performing the action $a$.

\begin{definition}\rm \label{def:derived}
The ternary relation $\Step\_ \; \subseteq \mathbb{P} \times A^* \times \mathbb{P}$ is
the least relation satisfying
\hfill
  $p \Step \epsilon p$,
\hfill
 $\infr{p \step \tau p'}{p \Step \epsilon p'}$,
\hfill
 $\infr{p \step a p',~ a \not= \tau}{p \Step {a} p'}$,
\hfill and \hfill
 $\infr{p \Step \sigma p' \Step \rho p''}{p \Step {\sigma\rho} p''}$
\enskip.\\
We write $p \Step \sigma$ for $\exists p' \cdot p \Step \sigma p'$
and $p \Step * p'$ for $\exists \sigma \cdot p \Step \sigma p'$.\\
Let $\tr(p) = \{\sigma \in A^* \mid p \Step \sigma\}$ be the set of
\emph{traces} of $p$,\\
and $\act(p) = \{a \in A \mid a$ or $\bar a$ occurs in a trace of $p\}$ the
\emph{alphabet} of $p$.
\end{definition}
%
In this paper we present particular processes that are instrumental in proving
our results (cf.\ Figs.~\ref{context2},~\ref{context}). Therefore our results
apply only to transition systems in which those processes exist. To ensure
this, we assume that $(\mathbb{P},\rightarrow)$\vspace{-6pt}
\begin{enumerate}
\item is closed under \emph{action prefixing}, meaning that for any
  $p\in \mathbb{P}$ and $a\!\in\! A_{\tau}$ there is a process $a p$ such
  that \plat{$\,a p \step{c} q$} iff $a=c$ and $q=p$, and
\item is closed under \emph{countable summation}, meaning that for
  every countable set of processes $P\subseteq \mathbb{P}$ there is a
  process \plat{$\sum P$} such that for all $a\!\in\! A$ we have $\sum P
  \step a q$ iff there exists $p\in   P$ such that $p\step a q$.
\end{enumerate}\vspace{-5pt}
Alternatively we may assume that $(\mathbb{P},\rightarrow)$ contains
finite-state processes only, and is closed under action prefixing and
finite summation (cf.\ Remark~\ref{finite-state} in Sect.~\ref{AGEF}).
We also postulate the Fresh Atom Principle \cite{vG05}, allowing fresh
actions in proofs.

When writing expressions with action prefixing and summation, we let
$0$ stand for $\sum\emptyset$ and $p+q$ for $\sum\{p,q\}$, and
prefixing binds stronger than sum. We write $a$ for $a0$ and, when
$\sigma=a_1\dots a_n$, write $\sigma p$ for $a_1\dots a_n p$
and $\bar\sigma$ for $\bar a_1 \dots \bar a_n$.\vspace{-5pt}

\section{Coarsest Congruence Relations on Processes}

Semantic equivalences on processes are used to assess
whether an implementation has the same functionality as its specification,
viz.\ Fig.\,\ref{gsm}.  The equivalence of two processes should guarantee that
if one has a certain desirable property, then so has the other. In the context
of an LTS $(\mathbb{P},\rightarrow)$, properties can be
modelled as unary predicates $\phi \subseteq \mathbb{P}$.  A semantic
equivalence relation $\sim\;\subseteq \mathbb{P} \times \mathbb{P}$
\emph{respects} or \emph{preserves} % such
a property $\phi$ if $p \sim q \Rightarrow (\phi(p)\Leftrightarrow\phi(q))$.
Thus, a %first requirement of a
semantic equivalence should respect % is that it respects
all relevant properties of the systems
on which it is applied.  Naturally, what is relevant depends to a large extent on
the intended application, and consequently many semantic
equivalences have been proposed in the literature \cite{IPGla93}. This paper focusses on
\pagebreak[1]
system requirements that we call AGEF and AGAF properties; they
will be defined in Section~\ref{AGEF}.

A transition system $(\mathbb{P},\rightarrow)$ is often equipped with process algebraic
operators $f:\mathbb{P}^n\rightarrow\mathbb{P}$.
Throughout this paper, we shall assume that $(\mathbb{P},\rightarrow)$ is equipped with the
\emph{parallel composition} $({\_}\,|\,{\_})$ and \emph{restriction} $\_\,\backslash H$ for
$H\subseteq A$ of CCS \cite{Mi90ccs}.
\begin{definition}\rm \label{def:parres}
  The CCS
\emph{parallel composition operator} is a binary operator $({\_}\,|\,{\_})$ defined on
  $\mathbb{P}$ in such a way that, for all $p,q,r\!\in\!\mathbb{P}$ and for all $a\!\in\! A_{\tau}$,
  $p\,|\,q\step{a}r$ iff
  \begin{enumerate}\rnc{\itemsep}{1pt}
  \item there exists $p'\in\mathbb{P}$ such that \plat{$p\step{a}p'$} and $r=p'\,|\,q$; or
  \item there exists $q'\in\mathbb{P}$ such that \plat{$q\step{a}q'$} and $r=p\,|\,q'$; or
  \item $a=\tau$ and $\exists p',q'\!\in\mathbb{P}$ and $b\in\! A$ such that
          \plat{$p\step{b}p'$, $q\step{\bar b}q'$} and $r=p'\,|\,q'$.
  \end{enumerate}
  A \emph{restriction operator} is a unary operator $\_\,\backslash H$ defined on $\mathbb{P}$ in
  such a way that, for all $p,q\in\mathbb{P}$ and for all $a\in A_{\tau}$, $p\,\backslash H\step a q$
  iff $a,\bar{a}\not\in H$ and there exists $p'\in\mathbb{P}$ such that $p\step{a}p'$ and
  $q=p'\backslash H$.
\end{definition}
Component-based design often results in processes of the form
$(p_0 \,|\, \cdots \,|\, p_n)\backslash H$ when formalised in CCS\@. If % in such a composition a
the component $p_i$ is
replaced by an equivalent component $q_i$, we want to be able to conclude that the resulting composition is equivalent to the original.
Due to the state explosion phenomenon, it is often infeasible to check this explicitly.
Therefore, a second requirement on semantic equivalence relations
is that they are congruences for all relevant composition operators; this
in order to allow compositional verification.
%
\begin{definition}\rm
A semantic equivalence relation $\sim\;\subseteq \mathbb{P} \times \mathbb{P}$ is a \emph{congruence} for an
operator $f:\mathbb{P}^n\rightarrow\mathbb{P}$, or $f$ is \emph{compositional} for $\sim$, if $p_i \sim q_i$ for
$i=1,...,n$ implies that $f(p_1,...,p_n)\sim f(q_1,...,q_n)$.
\end{definition}
%
Often, one requires compositionality of all operators of CCS and CSP; the minimum
requirement typically involves just the operators $|$ and $\backslash H$ of CCS, or
alternatively the \emph{parallel composition} and \emph{concealment} operators of CSP.

Let $\sim,\approx\; \subseteq \mathbb{P} \times \mathbb{P}$ be equivalence relations. Then $\sim$ is called {\em finer}
than $\approx$ and $\approx$ {\em coarser} than $\sim$ if $\sim \;\subseteq\; \approx$. (Note that we use these concepts
in a non-strict sense.)
As explained above, we seek semantic equivalences that
(1) preserve important properties of the processes on which they will be applied,
(2) are congruences for the operators that are used to compose processes, and
(3) possibly satisfy some other requirements, such as RSP (see the introduction).
When the requirements are completely clear and not subject to change,
amongst multiple equivalences that meet all requirements,
the coarsest of them, if it exists, constitutes the
ultimate criterion for system verification,
as it enables more implementations to be shown correct
with respect to a given specification.
The main goal of this paper is to characterise such coarsest equivalences.

\section{AGEF and AGAF Properties}\label{AGEF}

\begin{definition}\rm
The set $\IF(p)$ of \emph{impossible futures} of a process $p$ is the set
of pairs $(\sigma,G) \in A^* \times \pset(A^*)$ satisfying
$$\exists p' \cdot p \Step \sigma p' \land G \cap \tr(p') = \emptyset.$$
Processes $p,q$ are {\em IF-equivalent}, notation \mbox{$p \eqIF q$}, iff $\IF(p)=\IF(q)$.
\pagebreak[2]
\end{definition}
%
Note that $(tf,\{tc\}) \in \IF(q) \setminus \IF(p)$, where $p,q$ are respectively the left- and right-hand
processes of Fig.\,\ref{gsm}. (The transitions {\it ok} and {\it nok} are labelled $\tau$.)
So $p$ and $q$ are not IF-equivalent.
The statement $(\sigma,G) \not\in \IF(p)$ expresses the property
$$\plat{$\forall p' \cdot p \Step \sigma p' \Rightarrow
\exists \rho \in G \cdot p' \Step \rho$}.$$
Pete's redialling requirement consists of the conjunction of these properties for $\sigma=(tf)^k$ and $G = \{tc\}$.
We call them \emph{AGEF properties}.

\begin{definition}\rm
For $\sigma\!\in\! A^*$ and $G\subseteq A^*$, let AGEF$(\sigma,G)$ be the property (subset) of
processes with $p\in {\rm AGEF}(\sigma,G)$ iff \plat{$\forall p' \cdot p \Step \sigma p' \Rightarrow
\exists \rho \in G \cdot p' \Step \rho$}.
\end{definition}
%
Now a process $p$ satisfies AGEF$(\sigma,G)$ iff $(\sigma,G)\not\in \IF(p)$.
Thus, an equivalence on processes respects all AGEF properties if and
only if it is finer than $\eqIF$. Note that AGEF$(\sigma,G \cup G') =
{\rm AGEF}(\sigma,G)$ if every $\rho \in G'$ has a prefix $\rho'\in G$.
We therefore assume w.l.o.g. that the sets $G$ have the \emph{prefix property}:
$\forall \rho,\nu \in G \cdot \rho \not < \nu$.

The name AGEF is derived from a way to express such properties in \emph{Computation Tree Logic} (CTL) \cite{IPClEm81}.
CTL is a formalism to specify temporal properties of systems that are modelled as states in \emph{Kripke structures}.
The latter are transition systems in which states rather than transitions are labelled.
Amongst others, CTL features the formulas, interpreted on a state $s$,\\[3pt]
\begin{tabular}{@{~~}l@{~~~}l@{}}
{\bf AF}$\phi$ & meaning that every path from $s$ eventually passes a state satisfying $\phi$\\
{\bf EF}$\phi$ & meaning that some path from $s$ eventually passes a state satisfying $\phi$\\
{\bf AG}$\phi$ & meaning that on every path from $s$ all states satisfy $\phi$\\
{\bf EG}$\phi$ & meaning that on some path from $s$ all states satisfy $\phi$\\
$\ell$         & meaning that state $s$ has label $\ell$.
\end{tabular}\\[3pt]
Here $\phi$ is again a CTL formula.
CTL formulas can also be combined with propositional connectives.
In order to interpret CTL formulas on a process $p$ in an LTS $\mathbb{L}$, we convert the part of $\mathbb{L}$ that is reachable from $p$
into a Kripke structure by unwinding it into a tree,
and labelling each state with the trace of the unique path leading to it.
This leads to a Kripke structure $\mathbb{L}_p$ whose states are the finite paths $\pi$ in $\mathbb{L}$ starting from $p$,
labelled with the sequence of visible actions labelling $\pi$,
and there is a transition $\pi \rightarrow \pi'$ iff
the path $\pi'$ can be obtained from $\pi$ by adding one transition.
We say that $p$ satisfies a CTL formula $\phi$ iff the root
of the tree-shaped Kripke structure $\mathbb{L}_p$ satisfies $\phi$.%
\footnote{Other translations from LTSs
to Kripke structures have appeared in the literature \cite{DV95},
leading to different interpretations of CTL on LTSs.}
Now the property AGEF$(\sigma,G)$ is expressed in CTL as
${\bf AG} (\sigma \Rightarrow {\bf EF} \bigvee_{\rho\in G} \sigma\rho)$.

We also consider \emph{conditional liveness} requirements or \emph{AGAF properties},
stating that {\em something good} will eventually happen when a specific past has been observed.
The property AGAF$(\sigma,G)$ with $G\neq\emptyset$
states that every run with visible content $\sigma$ \emph{will} be completed to a run with visible content $\sigma\rho$ for $\rho\!\in\!G$, \emph{provided no visible action occurs that disables the potential of achieving $G$}.
In contrast, the property AGEF$(\sigma,G)$ says
that any run with visible content $\sigma$ \emph{can} be completed to such a run.
A liveness property of the form AGAF$(\epsilon,G)$ states that something good will happen unconditionally.
Pete's liveness requirement
``{\sf if I keep hitting the redial button, I will eventually be connected}''
is AGAF$(\epsilon,P)$ with $P=\{(tf)^ktc \mid k \in \Nat\}$.

We now formulate the fairness principle ${\cal F}$:
{\sf during a system run, a specific set of states that remains reachable throughout cannot be avoided forever}.
This amounts to strong fairness \cite{BoFra86} for finite-state processes.
We say that a path satisfies ${\cal F}(\psi)$, with $\psi$ a set of states, if
it is not a infinite path with $\psi$ reachable throughout and avoiding $\psi$ forever.
The requirement AGAF$(\sigma,G)$ under the assumption $\F$ is written $\AGAFF(\sigma,G)$.
The specification of Pete's phone satisfies $\AGAFF(\epsilon,P)$ but not AGAF$(\epsilon,P)$.
The implementation satisfies neither.

In order to conveniently express AGAF properties in temporal logic, we add a modality
${\bf A}\!^\chi{\bf F}$ to CTL. Here $\chi$ is a property on paths, and
${\bf A}\!^\chi{\bf F}\phi$ holds in state $s$, if every (possibly infinite) path from $s$ that is
maximal (cannot be extended) amongst the paths satisfying $\chi$, passes through a state satisfying $\phi$.
AGAF$(\sigma,G)$ with $\sigma \!\in\! A^*$ and $\emptyset\neq G\subseteq A^*$ can be expressed as ${\bf AG}(\sigma \!\Rightarrow\! {\bf A}\!^{[G]}{\bf F} \psi)$,
and $\AGAFF(\sigma,G)$ as ${\bf AG}(\sigma \Rightarrow {\bf A}\!^{{\cal F}(\psi)\land [G]}{\bf F} \psi)$,
where $\psi=\bigvee_{\rho\in G} \sigma\rho$ and $[G]$ is the property of a path that all labels $\sigma\nu$ of its states satisfy
$\exists \rho\!\in\!G\cdot\nu\leq\rho$.

Pete's liveness requirement cannot be expressed as a property of the form
\plat{${\bf AG}(\sigma \!\Rightarrow\! {\bf A}\!^{{\cal F}(\psi)}{\bf F} \psi)$}
with $\psi=\bigvee_{\rho\in G} \sigma\rho$.
When taking $\sigma=\epsilon$ and $G=P$ this property says ``{\sf eventual connection is guaranteed}'',
which is easily refuted by hitting the {\sl stop} button; taking $G=P \cup \{(tf)^ks \mid k \in \Nat\}$
yields a requirement that is satisfied by the buggy implementation.

We will show that any $\AGAFF$ property can be formulated as a conjunction of AGEF properties.
We write AGEF$\:C$ with $C\subseteq A^*\times \pset(A^*)$ for the conjunction
$\bigwedge_{(\sigma,G)\in C}$AGEF$(\sigma,G)$, and similarly for AGAF$\:C$ and $\AGAFF\:C$.

Let $\sigma\!\in\! A^*$ and $\emptyset\neq G\subseteq A^*$. Then
$\mbox{$\uparrow$}(\sigma,G) := \{(\sigma\rho,\rho^{-1}G) \mid \rho \in \,\downarrow\!\!G\}$,
where $\downarrow\!\!G := \{\nu\!\in\!A^* \mid \exists
\rho\cdot\nu\rho\!\in\!G\} \setminus \{\rho\nu \mid \rho\!\in\!G\}$
(the set of proper prefixes of $G$)
and $\sigma^{-1}G := \{\rho \mid \sigma\rho \in\! G\}$.
For instance, $\mbox{$\uparrow$}(a,\{b,cd\}) = \{(a,\{b,cd\}),(ac,\{d\})\}$.

\begin{lemma}\label{trivagef}
Let $\sigma\!\in\! A^*$ and $\emptyset\neq G\subseteq A^*$.
Then\\
${\rm AGAF}(\sigma,G) \subseteq \AGAFF(\sigma,G) \subseteq {\rm AGEF}(\sigma,G)$,\\
${\rm AGAF}(\sigma,G) = {\rm AGAF}\mbox{$\uparrow$}(\sigma,G)$ and $\AGAFF(\sigma,G) = \AGAFF\mbox{$\uparrow$}(\sigma,G)$.
\end{lemma}
\begin{proof}
The inclusions are trivial; something that will happen must surely be possible.
The equalities state e.g.\ that ${\rm AGAF}(\sigma,G)$ implies ${\rm AGAF}(\sigma\rho,\rho^{-1}G)$ for any $\rho\!\in\downarrow\!\!G$:
a promise remains valid as long as it hasn't been delivered.
\qed\end{proof}

\begin{theorem}\label{fair}
The property $\AGAFF(\sigma,G)$ is equal to ${\rm AGEF}\mbox{$\uparrow$}(\sigma,G)$.
\end{theorem}

\begin{proof}
By Lemma~\ref{trivagef}, we find ${\AGAFF}(\sigma,G)
= {\AGAFF}\mbox{$\uparrow$}(\sigma,G) \subseteq {\rm AGEF}\mbox{$\uparrow$}(\sigma,G)$.
Let $\psi=\bigvee_{\rho\in G} \sigma\rho$. If $p \in {\rm AGEF}\mbox{$\uparrow$}(\sigma,G)$
then from every $p'$ with \plat{$p \Step {\sigma\rho} p'$} and
$\rho\in\!\mbox{$\downarrow$}G$, a $\psi$-state is reachable. Any
run from $p$ that starts with $\sigma$, avoids states labelled $\sigma\nu$ with
${\not\!\exists}\rho\!\in\!G\cdot\nu\!\leq\!\rho$,
and satisfies $\F(\psi)$, will eventually reach $\psi$.
\qed\end{proof}
%
By Theorem~\ref{fair}, Pete's liveness requirement
$\AGAFF(\epsilon,P)$ (assuming fairness)
is implied by ${\rm AGEF}\mbox{$\uparrow$}(\epsilon,P) = {\rm AGEF}\{((tf)^n,P),\,((tf)^nt,\{c\}\cup fP) \mid n \in \Nat\}$.

The property ${\rm AGAF}(\sigma,G)$ can be expressed in CTL as
${\rm AGEF}\mbox{$\uparrow$}(\sigma,G)\wedge {\bf AG}(\sigma \!\Rightarrow\! {\bf AF} \bigvee\!_{\rho\not\in\downarrow G}\sigma\rho)$. We therefore do not need the modality ${\bf A}\!^\chi{\bf F}$ for stating AGAF properties with or without $\F$.

In \cite{IPBrReVo95} it is defined when a process $p$ \emph{should pass} a test.
A \emph{test} is given by a test process $t$, whose alphabet may contain an extra action $\checkmark$ that cannot occur in
the alphabet of the process $p$. The test consists of running $p$ and $t$ in parallel using the CSP parallel
composition operator $\|_A$ that forces all actions of $p$ and $t$ to synchronise, except for the action $\checkmark$.
The occurrence of $\checkmark$ denotes a successful outcome of the test.
We give an alternative formulation using the CCS operators:
The process $p$ \emph{should pass} the test, notation $p$ {\bf shd} $t$, if
$(p \,|\, t)\backslash (A\setminus\{\checkmark\})$ satisfies AGEF$(\epsilon,\{\checkmark\})$.
Processes $p,q$ are \emph{fair testing equivalent} \cite{IPBrReVo95}, notation $p =_{\bf shd} q$,
iff $p~{\bf shd}~t \Leftrightarrow q~{\bf shd}~t$ for all tests $t$.

\begin{definition}\rm
A property $\phi$ on transition systems is \emph{(should-) testable} if there
exists a test $t$ such that for all processes $p$ one has $p$ {\bf shd} $t$ iff $p$ satisfies $\phi$.
\end{definition}
%
A property is called \emph{trivial} if it either always holds or always fails.
As $p$ {\bf shd} $\checkmark$ for any $p$ and $p$ {\bf shd} $0$ for no $p$, all trivial properties are testable.
The trivial AGEF properties are AGEF$(\sigma,G)$ with $\epsilon\in G$, and AGEF$(\epsilon,\emptyset)$.

\begin{proposition}\label{should}
A nontrivial AGEF property AGEF$(\sigma,G)$ is testable iff for each sequence $b\rho$ in $G$ also its prefix
$b$ is in $G$.
\end{proposition}

\begin{proof}
``If'':
  We assume $\epsilon \not\in G$ and $G$ has the prefix property ($\forall \rho,\nu \in G \cdot \rho \not < \nu$).
  So $G$ consists of singleton traces only.
  Let $\sigma=a_1\dots a_m$. We define the processes $T_i$ ($0\leq i \leq m$)
  by $T_i = \bar a_{i+1}T_{i+1} + \checkmark$ for $0\leq i < m$ and
  $T_m = \sum \{\bar{b}\checkmark\mid b\in G\}$.
  Fig.~\ref{context2} displays the processes $T_i$ ($0\leq i \leq m$) for finite $G=\{b_1,\dots,b_n\}$.
\begin{figure}[htb]
\vspace{-1em}
\begin{center}
\input{context2.pstex_t}
\end{center}\vspace{-1em}
\caption{The test process $T_0$}
\label{context2}
\vspace{-1em}
\end{figure}

\noindent
Now $p$ satisfies AGEF$(\sigma,G)$ iff $p$ {\bf shd} $T_0$. Namely, if $(\sigma,G) \in \IF(p)$, i.e.\ $p$ does not
satisfy AGEF$(\sigma,G)$, then there exists $p'$ with \plat{$p \Step \sigma p'$} such that
\plat{$\forall \rho \in G \cdot p' \not\Step \rho$}, so \plat{$p\,|\,T_0 \Step \epsilon p'\,|\,T_m \not\Step \checkmark$}.
Conversely, if $(\sigma,G) \not\in \IF(p)$, then for any (strict or not) prefix
$\nu$ of $\sigma$ and any $p'$ with \plat{$p \Step {\nu} p'$} the $\checkmark$ can be done.

``Only if'':
Suppose $G$ contains a sequence $b \rho$ but not $b$.
Set $p := \sigma(b \rho + b)$ and $q := \sigma b \rho + \sigma b$ if $\sigma \not= \epsilon$ and $p := \tau(b \rho +
b)$ and $q := \tau b \rho + \tau b$ otherwise.
Then $p,q$ are fair testing equivalent \cite{IPBrReVo95}, whereas $(\sigma, G) \in \IF(q) \setminus
\IF(p)$. So $AGEF(\sigma,G)$ is not testable.
\qed\end{proof}
\begin{theorem}
All properties of the form ${\rm AGEF}\mbox{$\uparrow$}(\sigma,G)$ are testable.
\end{theorem}
\begin{proof}
Use the same test as above, but with $T_m$ replaced by the
deterministic process $T_G$ with $\tr(T_G)=\{\rho \in A^* \mid
\exists \nu\cdot \rho\nu \in G\} \cup \{\rho\checkmark \mid
\rho\in G\}$.
\qed
\end{proof}

\begin{remark}\label{finite-state}
When working in the context of a finite-state LTS, we only consider AGEF and AGAF properties with finite sets $G$. This way the test processes used
above will be finite. That the correspondence between AGEF properties
and $\eqIF$ is unaffected by this change follows by
\end{remark}
\begin{lemma}\label{finite}
If $(\sigma,G)\in \IF(q)\setminus\IF(q)$ and $q$ is a finite-state process, then
there is a finite $G'$ with $(\sigma,G') \in \IF(q)\setminus\IF(q)$.
\end{lemma}
\begin{proof}
The set $R = \{r \mid q \Step \sigma r\}$ is finite and for
each $r \!\in\! R$ we can choose a $\rho_r \!\in\! G$ such that \plat{$r \Step {\rho_r}$}.
Hence, $(\sigma,\{\rho_r \,|\, r \in R\}) \in \IF(p) \setminus \IF(q)$.
\qed\end{proof}
%
A \emph{safety property} says that \emph{something bad will not happen}.
Formalising ``bad'' as a predicate $B\subseteq A^*$ on the visible content of system runs,
a safety property has the form $B \cap \tr(x)=\emptyset$, and can be written as
$\bigwedge_{\sigma\in B}$AGEF$(\sigma,\emptyset)$.
Considering that the class of testable properties is closed under
conjunction (for $p$\, {\bf shd} $\tau t + \tau t'$ iff $p$ {\bf shd} $t$
and $p$ {\bf shd} $t'$), Prop.~\ref{should} implies that safety properties are testable.
A property AGEF$(\sigma,G)$ or AGEF\mbox{$\uparrow$}$(\sigma,G)$ is
called \emph{proper} if it is neither trivial, nor a safety property,
i.e.\ if $\epsilon\not\in G \neq \emptyset$.

\section{Four Levels of Respect for AGEF Properties}\label{classification}

In this section we show that only four types of congruences exist: those that respect all AGEF
properties, those that respect all testable AGEF properties but no others, those that respect all
safety properties but no other non-trivial AGEF properties, and those that do not respect a single
non-trivial AGEF property.  Examples in each of the four classes are weak bisimilarity
\cite{Mi90ccs}, fair testing equi\-valence \cite{IPBrReVo95}, trace equivalence---defined as $p =_\tr
q$ iff $\tr(q)=\tr(q)$---and failures equivalence \cite{BHR84} (where the absence of traces
occurring past a divergence is not recorded), respectively. In this section
``congruence'' means congruence for the CCS parallel composition and restriction operators; we could
also have used the CSP parallel composition and concealment operators.
The results in this section are not needed further on, although we will reuse the proof of Lemma~\ref{cc}.

We say that a congruence $\sim$ is {\em non-IF} if there exist processes $p,q$ with $p \sim q$ such that $\IF(p) \not= \IF(q)$. For a non-IF congruence there exists an AGEF property that it does not preserve; we shall now prove that in fact it does not preserve any non-testable AGEF property.

\begin{lemma}\label{cc}
If $\sim$ is a non-IF congruence, then for all $c\!\in\! A$ there
exist processes $p_c,q_c$ with $\act(p_c)=\act(q_c)=\{c\}$, such that
$p_c \sim q_c$ and $(\epsilon,\{cc\}) \in \IF(p_c) \setminus \IF(q_c)$.
\end{lemma}

\begin{proof}
The congruence $\sim$ is non-IF, so there exist processes $p,q$ and
$\sigma,G$ such that $p \sim q$ and  $(\sigma,G) \in \IF(p) \setminus
\IF(q)$. Note that $\epsilon \not\in G$: if $\epsilon \in G$ then
$(\sigma,G) \not\in \IF(p)$.

Let $\sigma= a_1 \dots a_m$
and define $H :=\act(p)\cup\act(q)$. We first establish the lemma
for all actions $c \not\in H$, and then consider the case $c \in\! H$.
Let $U_i$ ($0\leq i \leq m$), $V$ and $W$ be defined by
  $U_i= \tau V + \bar{a}_{i+1} U_{i+1}$ for $0\leq i < m$,
  $U_m= \tau V + \tau cW$,
  $V=c(\tau c+ \tau)$ and
  $W=\sum_{\rho \in G}\bar \rho(\tau c + \tau)$
(Fig.~\ref{context} displays the processes $U_i$ ($0\leq i \leq m$),
$V$ and $W$ for the case that $G=\{\rho_1,\dots,\rho_n\}$).
As we assume our alphabet $A$, and hence $G\subseteq A^*$, to be
countable, the sum $W$ is countable too. If $q$ is a finite-state
process, by Lemma~\ref{finite} we may even assume it to be finite.
\begin{figure}[t]
\begin{center}
\input{context1.pstex_t}
\end{center}\vspace{-1em}
\caption{The process $U_0$}\label{context}
\end{figure}
Let $p_c = (U_0\,|\, p)\backslash H$ and $q_c = (U_0\,|\, q)\backslash
H$.  By construction, \plat{$\act(p_c)=\act(q_c)=\{c\}$}.
Since $p \sim q$ and $\sim$ is a congruence for $|$ and $\backslash H$, we have
$(U_0\,|\,p)\backslash H \sim (U_0\,|\,q)\backslash H$.
There exists a $p'$ with \plat{$p \Step \sigma p'$} and \plat{$p' \not\Step \rho$} for all
$\rho\in G$. Therefore, we have $(U_0|\, p)\backslash H
\Step{\epsilon} (cW|\, p')\backslash H$ and $(cW|\, p')\backslash H\hspace{-1pt}
\not\Step{cc}$.  Hence, $(\epsilon,\{cc\}) \in \IF((U_0\,|\, p)\backslash
H)$. However, as \plat{$\forall q' \cdot (q \hspace{-1pt}\Step \sigma\hspace{-1pt} q') \Rightarrow
(\exists \rho \!\in\! G \cdot q'\! \Step \rho)$}, we have $(\epsilon,\{cc\}) \not\in
\IF((U_0\,|\, q)\backslash H)$.  This proves our lemma for all actions
$c\not\in H$.

To obtain the required results for $c\in H$, first choose $d\not\in H$
(appealing to the Fresh Atom Principle \cite{vG05} if $A\setminus H$ is empty).
By the above, there exist $p_{d}$ and
$q_{d}$ with $\act(p_{d})=\act(q_{d})=\{d\}$ such that $p_{d}\sim
q_{d}$ and $(\epsilon,\{dd\})\in\IF(p_{d}) \setminus \IF(q_{d})$.
Now, since $c\in A\setminus\{d\}$, the required $p_c$ and $q_c$
are obtained by running the same arguments again, taking $p:=p_{d}$,
\,$q:=q_{d}$, \,$\sigma:=\epsilon$, \,$G:=\{dd\}$ and $H:=\{d\}$.
\qed\end{proof}
%
From this lemma we deduce that no non-testable AGEF property is preserved by a non-IF congruence.

\begin{theorem}\label{genif}
Let $\sim$ be a non-IF congruence. Then for any non-testable property {\rm AGEF}$(\sigma,G)$ there are
processes $p,q$ such that $p \sim q$ and $(\sigma,G) \in \IF(p) \setminus \IF(q)$.
\end{theorem}
\begin{proof}
Let $(\sigma,G)$ be a non-testable AGEF property.  Pick $b\rho \!\in\! G$ such that $\epsilon, b \not\in G$.
Let $c$ be an action that does not occur in $\sigma b \rho$.  By Lemma~\ref{cc} there are processes $p$
and $q$ with $\act(p)=\act(q)=\{c\}$, $p\sim q$ and $(\epsilon,\{cc\})\in \IF(p)\setminus\IF(q)$.
As $\sim$ is a congruence for $|$ and $\backslash H$, we have $(p\,|\,\sigma b \bar c \bar c \rho)\backslash \{c\}
\sim (q\,|\,\sigma b \bar c \bar c \rho)\backslash \{c\}$.

\noindent\hspace{7pt}%
Whenever $(q\,|\,\sigma b \bar c \bar c \rho)\backslash \{c\} \!\Step\sigma\! r$, the process $r$ must be of the form
$(q'\,|\,b \bar c \bar c \rho)\backslash \{c\}$ with $q\Step\epsilon q'$. Since $(\epsilon,\{cc\})\not\in\IF(q)$, we have
$q'\!\Step {cc}$ and hence \plat{$(q'\,|\,b \bar c \bar c \rho)\backslash \{c\}\Step{b\rho}$}. Thus
$(\sigma, G)\not\in\IF((q\,|\,\sigma b \bar c \bar c \rho)\backslash \{c\})$.

\noindent\hspace{7pt}%
Since $(\epsilon,\{cc\})\in\IF(p)$, we have $p\Step\epsilon p'$ for a process $p'$ with $p'\not\Step {cc}$.
Hence \plat{$(p\,|\,\sigma b \bar c \bar c \rho)\backslash \{c\}\Step\sigma (p'\,|\,b \bar c \bar c \rho)\backslash \{c\}$},
and \plat{$(p'\,|\,b \bar c \bar c \rho)\backslash \{c\}\Step\nu$} only if $\nu=\epsilon$ or $\nu=b$.
It follows that $(\sigma, G)\in \IF((p\,|\,\sigma b \bar c \bar c \rho)\backslash \{c\})$.
\qed\end{proof}
%
Next, we prove that a congruence $\sim$ either preserves all testable properties
(AGEF or otherwise) or does not preserve any proper AGEF property, nor any
proper liveness property under the global fairness assumption ${\cal F}$.

\begin{lemma}\label{c}
If $\sim$ is a congruence that does not respect all testable properties, then for all $c\!\in\! A$ there exist
processes $p_c,q_c$ with $\act(p_c)=\act(q_c)=\{c\}$, such that
$p_c \sim q_c$ and $(\epsilon,\{c\}) \in \IF(p_c) \setminus \IF(q_c)$.
\end{lemma}

\begin{proof}
Let $\phi$ be a testable property that is not preserved by $\sim$.
As $\phi$ is testable, there is a test process $t$ such that $\forall p\!\in\!\mathbb{P}$
one has $p~{\bf shd}~t$ iff $p$ satisfies $\phi$.
As $\phi$ is not preserved by $\sim$, there are processes $p,q$
such that $p\sim q$ and $\phi(q)$ but not $\phi(p)$.
Hence $q~{\bf shd}~t$ but $p~\,\not\!\!\!\!{\bf shd}~t$.
Let $p_{\checkmark} = (p\,|\,t)\backslash (A\setminus\{\checkmark\})$
and $q_{\checkmark} = (q\,|\,t)\backslash (A\setminus\{\checkmark\})$.
Then $q$ satisfies AGEF$(\epsilon,\{\checkmark\})$ but $p$ does not,
so $(\epsilon,\{\checkmark\}) \in \IF(p_{\checkmark}) \setminus \IF(q_{\checkmark})$.
$\act(p_{\checkmark})=\act(q_{\checkmark})=\{\checkmark\}$.
As $\sim$ is a congruence for $|$ and $\backslash H$, we have
$p_{\checkmark} \sim q_{\checkmark}$.
The result for actions $c \neq \checkmark$ is obtained in a manner
similar to the one used in the proof of Lemma~\ref{cc}.
\qed\end{proof}

\begin{theorem}\label{non-testable}
Let $\sim$ be a congruence that does not respect all testable properties.
Then for any proper {\rm AGEF} property {\rm AGEF}$(\sigma,G)$ there are
processes $p$ and $q$ such that $p \sim q$ and
$p \not\in {\rm AGEF}(\sigma,G) \supseteq {\rm AGEF}\mbox{$\uparrow$}(\sigma,G)\ni q$.
\label{gentestif}
\end{theorem}

\begin{proof}
Let $(\sigma,G)$ be given, satisfying $\epsilon\not\in G\not=\emptyset$, and take $\rho \!\in\! G$.
Let $c$ be an action that does not occur in the sequence $\sigma \rho$.  By Lemma~\ref{c} there are processes $p$
and $q$ with $\act(p)=\act(q)=\{c\}$, $p\sim q$ and $(\epsilon,\{c\})\in \IF(p)\setminus\IF(q)$.
Since $\sim$ is a congruence for $|$ and $\backslash H$, we have $(p\,|\,\sigma \bar c \rho)\backslash \{c\}
\sim (q\,|\,\sigma \bar c \rho)\backslash \{c\}$.
As in the proof of Theorem~\ref{genif}, we find that $(\sigma,G) \in \IF((p\,|\,\sigma \bar c \rho)\backslash \{c\})
\setminus \IF((q\,|\,\sigma \bar c \rho)\backslash \{c\})$ and
moreover $p \not\in {\rm AGEF}(\sigma,G) \supseteq {\rm AGEF}\mbox{$\uparrow$}(\sigma, G)\ni q$.
\qed\end{proof}
%
Finally we show that a congruence that fails to respect a safety property does not respect any nontrivial AGEF property.

\begin{lemma}\label{lem-safety}
If $\sim$ is a congruence that does not respect all safety properties,
then for all $c\!\in\! A$ there exist
processes $p_c,q_c$ with $\act(p_c)=\act(q_c)=\{c\}$, such that
$p_c \sim q_c$ and $c \in \tr(p_c) \setminus \tr(q_c)$.
\end{lemma}

\begin{proof}
The congruence $\sim$ violates a safety property $\bigwedge_{\sigma\in G}$AGEF$(\sigma,\emptyset)$,
so there must be an $\sigma\!\in\! G$ and processes $p$ and $q$ with $p\sim q$ and
$(\sigma,\emptyset) \in \IF(p) \setminus \IF(q)$, i.e.\ $\sigma\in\tr(p)\setminus\tr(q)$.
Note that $\sigma\not=\epsilon$: if $\sigma=\epsilon$ then $(\sigma,\emptyset) \in \IF(q)$.
By placing $p$ and $q$ in a context $(\_\!\_\,|\, \bar\sigma c)\backslash H$ with $c\not\in H:= \act(p)\cup\act(q)$
we obtain processes $p_c,q_c$ as required.
The result for $c \!\in\! H$ is obtained just as in the proof of Lemma~\ref{cc}.
\qed\end{proof}

\begin{theorem}\label{safety}
Let $\sim$ be a congruence that does not respect all safety properties.
Then for any nontrivial property {\rm AGEF}$(\sigma,G)$ there are
processes $p$ and $q$ with $p \sim q$ and $(\sigma,G) \in \IF(p) \setminus \IF(q)$, i.e.\
$q \in {\rm AGEF}(\sigma,G)$ and $p \not\in {\rm AGEF}(\sigma,G)$.
\end{theorem}

\begin{proof}
The case $\sigma=\epsilon$ follows from Theorem~\ref{non-testable}, as safety properties are testable
and nontrivial properties AGEF$(\epsilon,G)$ are proper. So assume $\sigma\neq\epsilon$.
Let $c$ be an action that does not occur in $\sigma$. By Lemma~\ref{lem-safety}
there are processes $p,q$ with $p \sim q$, $\act(p)=\act(q)=\{c\}$ and $c \in \tr(p) \setminus \tr(q)$.
Since $\sim$ is a congruence for $|$ and $\backslash H$, we have $(p\,|\,\bar c \sigma)\backslash \{c\}
\sim (q\,|\, \bar c \sigma )\backslash \{c\}$.
Now $(\sigma,G) \in \IF((p\,|\, \bar c \sigma)\backslash \{c\})
\setminus \IF((q\,|\,\bar c \sigma)\backslash \{c\}).\qed$
\end{proof}

\section{The Recursive Specification Principle}

The \emph{Recursive Specification Principle} (RSP) \cite{ArBaBeKl87} says that
systems of guarded recursive equations have unique solutions. Our aim
is to characterise $\eqIF$ as the coarsest congruence that respects
a proper AGEF property and satisfies RSP.
To this end, we only need a simplification of RSP, called RSP$^*$,
saying that equations of the form $X = \sigma X + p$ with $\sigma \in
(A_\tau)^*\setminus\{\tau\}^*$ have unique solutions. We denote the
unique solution of such an equation as $\sigma^*p$.
Alternatively, we could introduce $\sigma^*\_$ as an operator on processes, with
$\sigma^*p \step a p'$ iff $p \step a p'$ or ($\sigma=a\rho$ and $p'=\rho(\sigma^*p)$).

\begin{definition}\rm
An equivalence relation $\sim$ satisfies RSP$^*$ if for all $\sigma \in
(A_\tau)^*\setminus\{\tau\}^*$ and processes $p,q$\vspace{-1ex}
$$p \sim \sigma p + q ~~\Rightarrow~~ p\sim \sigma^*q\;.$$
\end{definition}
%
Fair testing congruence \cite{IPBrReVo95} does not satisfy RSP$^*$, since $t=a^*0+ a^*ab$
is fair testing congruent to $a t+ ab$ but not to $a^*a b$.

\section{Impossible Futures Congruence}

Just like weak bisimulation equivalence \cite{Mi90ccs} and most other weak
equivalences, impossible futures equivalence $\eqIF$ (defined in Sect.~\ref{AGEF})
fails to be a congruence for the CCS choice operator +.
We apply the usual fix to this problem: the addition of a root condition.
Just like for failures or fair testing equivalence, a one-bit root
condition is sufficient: we merely need to distinguish processes that
can do an initial $\tau$-step from those that can not.

\begin{definition}\rm
Processes $p,q$ are {\em IF-congruent}
(notation \mbox{$p \reqIF q$}) iff $p \eqIF q \land (p \step \tau) \Leftrightarrow (q \step \tau)$.
\end{definition}
%
Theorem 12 in \cite{IPBrReVo95} (Theorem 4.8 in the journal preprint) shows that $\reqIF$ is finer than fair testing equivalence, which is itself finer than trace equivalence.
In \cite{ArVoMa00}, it is shown that $\reqIF$ is coarser than weak
bisimulation congruence.
Since $a+\tau b$ and $\tau(a+b)+\tau b$ are IF congruent but not weakly bisimilar, $\reqIF$ is strictly coarser.
We now show that $\reqIF$ is a congruence and satisfies RSP$^*$.

\begin{proposition}
  $\reqIF$ is a congruence satisfying {\rm RSP} $($and hence {\rm RSP}$^*)$.
\end{proposition}
%
\begin{proof}
The argument in \cite{ArVoMa00} can be adapted and extended to yield the required result.
For example, RSP follows from a standard deductive argument \cite{ArBaBeKl87} based on the auxiliary finite projection operator and the induction principle AIP.
\qed\end{proof}
%
% In Section~\ref{sec:ifc},
Below, we show that $\reqIF$ is the coarsest of all
equivalences that (1) respect a proper AGEF property, (2) are
congruences for the CCS parallel composition, restriction, choice and
prefixing, (3) satisfy RSP$^*$, and (4) are coarser than an equivalence
$\bis{\rm max}$.  We show that in (1) it does not matter which AGEF
property we take, so it could for instance be the property
AGEF$(\epsilon,A)$, saying that the system can always do a first
visible action, i.e.\ has no initial livelock or deadlock.\pagebreak[1]\linebreak[1]
Instead of (1) we may also require that the equivalence
respects a proper property $\AGAFF(\sigma,G) =$ AGEF$\mbox{$\uparrow$}(\sigma,G)$,
i.e.\ a conditional liveness property assuming global fairness.
We do not know whether our result is valid without (4), but we use it in our proofs.
% In Section~\ref{sec:ifc}
Below, we establish our result with \emph{rooted weak bisimilarity} in the
r\^ole of $\bis{\rm max}$.
In CCS, weak bisimilarity is the equivalence of choice for e.g.\
comparing specifications and implementations. This equivalence is not a
congruence for all CCS operators, but it becomes so after extending it with a
root condition, yielding {\em rooted weak bisimilarity} ({\em observational
congruence}) \cite{Mi90ccs}.

\begin{definition}\rm
A relation $R \subseteq \mathbb{P} \times \mathbb{P}$ is called a \emph{weak
  bisimulation} if it satisfies for all processes $p,q$ with $p~R~q$
and for all $\sigma\in A^*$:\\
$-$ for all $p'$ with $p \Step
  \sigma p'$ there exists $q'$ such that $q \Step \sigma q'$ and
  $p'~R~q'$,\\
$-$ for all $q'$ with $q \Step \sigma q'$ there
  exists $p'$ such that $p \Step \sigma p'$ and $p'~R~q'$.\\
Processes $p,q$ are called {\em weakly bisimilar} (notation $p \bis{w}
q$) if there exists a weak bisimulation $R$ such that $p~R~q$.
They are called {\em rooted weakly bisimilar} (notation $p \bis{rw} q$) if they satisfy the additional
\emph{root conditions}:\\
$-$ for all $p'$ with $p \step \tau p'$ there exists $q'$ such that $q \Step \epsilon \step \tau q'$ and $p'~R~q'$,\\
$-$ for all $q'$ with $q \step \tau q'$ there exists $p'$ such that $p \Step \epsilon \step \tau p'$ and $p'~R~q'$.
\end{definition}
%
Write $\tau_a(p)$ for $(p\,|\,\bar a^*0)\backslash \{a\}$.
The operator $\tau_a$ renames action $a$ into $\tau$ (and disables $\bar a$).
By construction of rooted weak bisimulations, one can deduce the
following equivalences for $a \in A_\tau$, $\sigma \in
\{a,\tau\}^*\setminus\{\tau\}^*$ and processes $p$:
$$\begin{array}{l@{~}rcl@{~~~~~~~~}l@{~}rcl}
\rm{T1}:~ &a\tau p &\bis{rw} &a p &
\rm{KFAR}:~ &\tau_a(\sigma^*p) &\bis{rw} &\tau \tau_a(p).
\end{array}$$
KFAR \cite{ArBaBeKl87} identifies divergent processes (capable of an infinite
sequence of $\tau$ steps) and non-divergent ones.  We prove a lemma for later use.

\begin{lemma}\rm
Let $p,q,r$ be processes with $p \Step \epsilon \step\tau r \bis{w} q$.
Then $p \bis{rw} p+\tau q$.
\label{QH}
\end{lemma}
\begin{proof}
Let $R$ be $\bis{w}$ augmented with the pair $(p,p+\tau q)$.
This is a weak bisimulation satisfying the root conditions.
\qed \end{proof}
%
% \section{A Coarsest Congruence Result} \label{sec:ifc}
%
A process equivalence $\sim$ is called a {\em w-congruence} iff it is a congruence w.r.t.\ the CCS parallel composition,
restriction, choice and prefixing, and is coarser than $\bis{rw}$.
% In this section we
We proceed to characterise IF congruence as the coarsest w-congruence that
satisfies RSP$^*$ and preserves some arbitrary proper AGEF property.
Recall that a congruence $\sim$ is called {\em non-IF} iff there exist processes $p,q$ with $p \sim q$ such that $\IF(p) \not= \IF(q)$. We start with some lemmas.

\begin{lemma}\label{aa}
If $\sim$ is a non-IF w-congruence, then for any $c\in A$
$$\tau c(\tau c+\tau) \sim \tau c(\tau c+\tau)+\tau c$$
\end{lemma}

\begin{proof}
Start with the proof of Lemma~\ref{cc}, up to $(U_0\,|\,p)\backslash H \sim (U_0\,|\,q)\backslash H$.
Next we define the relation $R$ in Table~\ref{wbisim}.
%
\begin{table}[htb]
\begin{center}
$\begin{array}{llll}
{\rm \,simple~term}          &{\rm ~merge~term}&  &{\rm condition}\\
\hline
\,\tau c(\tau c+\tau)  &(U_0\,|\,q)\backslash H&&\mbox{\sl true}\\
\,c(\tau c+\tau)       &(U_k\,|\,q')\backslash H &~ &0 \leq k \leq m \land q \Step{a_1 \ldots a_k} q'\\
\,c(\tau c+\tau)       &(V\,|\,q')\backslash H   &~ &q \Step * q'\\
\,\tau c+\tau          &(\tau c+\tau \,|\,q')\backslash H  &~ &q \Step * q'\\
\,c                    &(c\,|\,q')\backslash H   &~ &q \Step * q'\\
\,0                    &(0\,|\,q')\backslash H   &~ &q \Step * q'\\
\,c(\tau c+\tau)       &(cW\,|\,q')\backslash H   &~ &q \Step \sigma q'\\
\,\tau c+\tau          &(W\,|\,q')\backslash H   &~ &q \Step \sigma q'\\[-1pt]
\,\tau c+\tau          &(\bar \vartheta(\tau c + \tau) \,|\,q')\backslash H  &~ &\exists \nu\not=\epsilon \cdot \nu\vartheta \in G \land q \Step \sigma \Step{\nu} q' \Step{\vartheta}\\[-1pt]
\,0                    &(\bar \vartheta(\tau c + \tau) \,|\,q')\backslash H &~ &\exists \nu \not=\epsilon \cdot \nu\vartheta \in G \land q \Step \sigma \Step{\nu} q' \not\Step{\vartheta}\\
\hline
\end{array}$
\end{center}
\caption{The relation $R$}
\label{wbisim}
\end{table}
%
This relation is a weak bisimulation, which can be verified by checking all steps.
The crucial argument is that for each $q'$ satisfying $q \Step \sigma q'$ there exists a $\rho\!\in\!G$ such that
\plat{$q'\Step{\rho}$}. The relation satisfies the root conditions, so\vspace{-1em}
$$\tau c(\tau c+\tau) \bis{rw} (U_0\,|\,q)\backslash H.\pagebreak[1]$$
As $(\sigma,G)\in\IF(p)$, there must be a process $p'$ such that $p \Step \sigma p'$ and $\forall \rho\!\in\!G \cdot p' \not\Step{\rho}$.
It is trivial to construct a weak bisimulation showing that $(cW\,|\, p')\backslash H \bis{w} c$
and hence $(U_0\,|\,p)\backslash H \Step{\epsilon} \step\tau (cW\,|\,p')\backslash H \bis{w} c$.
Using Lemma~\ref{QH}, this implies that $(U_0\,|\,p)\backslash H \bis{rw} (U_0\,|\,p)\backslash H + \tau c$.
Therefore, as $\sim$ is a congruence, we have $\tau c(\tau c+\tau) \bis{rw} (U_0\,|\,q)\backslash H \sim
(U_0\,|\,p)\backslash H \bis{rw} (U_0\,|\,p)\backslash H + \tau c \sim (U_0\,|\,q)\backslash H + \tau c$
$\bis{rw} \tau c(\tau c+\tau) + \tau c$. Since $\sim$ is transitive and coarser than
$\bis{rw}$ we obtain the desired result for $c\!\in\! A\!\setminus\! H$.
For $c\!\in\! H$, we proceed as in the proof of Lemma~\ref{cc}.
\qed\end{proof}

\begin{lemma}\label{speceq}
If\, $\sim$ is a non-IF w-congruence, then for all processes $P,Q$ and $a \!\in\! A$,
\begin{equation}\label{1}
\tau a(\tau P + Q) \sim \tau a(\tau P + Q) + \tau a P.
\end{equation}
\end{lemma}

\begin{proof}
Pick $c\not\in\act(P)\cup\act(Q)\cup\{a\}$ and place the processes
equated by Lemma~\ref{aa} in the context
$(\,\_\!\_\,\,|\,\tau a\bar{c}(\tau P+\bar{c}(\tau P+Q))\backslash\{c\})$.
\qed\end{proof}
%
We now use RSP$^*$ to show equivalence of processes with and without deadlock.

\begin{lemma}
Let $\sim$ be a non-IF w-congruence satisfying RSP$^*$.
Then for any process $Q$ we have $\tau(\tau Q + \tau) \sim \tau Q$.
\label{rspwcong}
\end{lemma}

\begin{proof}
Choose $Q$ and $a \not \in \act(Q)$.
Set $P=a^*0$ and $R=(\tau a)^*(\tau Q + \tau.P)$, so\vspace{-.8em}
$$\begin{array}{ll@{~~~~~~~~~~~~~~~~~}ll}
(2) &P \sim a P
&(3) &R \sim \tau P + \tau Q + \tau a R.\vspace{-0.8em}
\end{array}$$
Since $\tau a R = \tau a(\tau P + \tau Q + \tau a R)$, (1) yields $\tau a R \sim \tau a R + \tau a P$. Hence,\vspace{-.5em}
$$\tau a R + \tau Q \sim \tau a R + \tau a P + \tau Q \stackrel{2}\sim \tau a R + \tau P + \tau Q \stackrel{3}\sim R.\vspace{-0.3em}$$
Since $R \sim \tau a R + \tau Q$, RSP$^*$ yields $R \sim (\tau a)^*\tau Q$.
So, since $\sim$ is a congruence,\vspace{-.3em}
$$\tau.(\tau Q + \tau \tau 0) \bis{rw}
\tau_a((\tau a)^*(\tau Q + \tau (a^*0))) \sim
\tau_a((\tau a)^*\tau Q) \bis{rw} \tau \tau Q\vspace{-0.3em}$$
applying KFAR and $\tau_a(Q)=Q$.
Using T1, we obtain $\tau(\tau Q + \tau) \sim \tau Q$.
\qed\end{proof}
%
Fair testing \cite{IPBrReVo95} is a non-IF w-congruence that preserves all testable AGEF properties.
However, non-IF w-congruences satisfying RSP do not preserve {\em any} proper AGEF property,
nor any nontrivial property $\AGAFF(\sigma,G) = {\rm AGEF}\mbox{$\uparrow$}(\sigma,G)$.

\begin{theorem}\label{ifrsp}
Let $\sim$ be a non-IF w-congruence satisfying RSP$^*$. \
Then for any proper {\rm AGEF} property {\rm AGEF}$(\sigma,G)$ there are
processes $p$ and $q$ such that $p \sim q$ and
$p \not\in {\rm AGEF}(\sigma,G) \supseteq {\rm AGEF}\mbox{$\uparrow$}(\sigma,G)\ni q$.
\end{theorem}

\begin{proof}
Let $(\sigma,G)$ be proper, i.e.\ $\epsilon\not\in G\neq \emptyset$, and pick $\rho \!\in\! G$.
Set $Q = \rho$. By Lemma~\ref{rspwcong}, the fact that $\sim$ is a
congruence for the prefix operator, and by identity T1, we have
$p = \sigma(\tau Q + \tau) \sim \sigma Q = q$. Clearly, $(\sigma,G) \in \IF(p) \setminus \IF(q)$ and
$p \not\in {\rm AGEF}(\sigma,G) \supseteq {\rm AGEF}\mbox{$\uparrow$}(\sigma,G)\ni q$.
\qed\end{proof}
%
This theorem also gives a partial answer to van Glabbeek's first problem in \cite{WpAce03}:
{\sf what is the coarsest congruence $\sim$ satisfying RSP and respecting deadlock/livelock traces?}

\begin{definition}\rm
A sequence $\sigma \in A^*$ is a {\em deadlock/livelock trace} of a process $p$ if
\plat{$\exists p'\cdot p \Step \sigma p' \wedge \tr(p')=\{\epsilon\}$}. A process equivalence $\sim$
{\em respects deadlock/livelock traces} iff $p \sim q$ implies that $p$ and $q$ have the same deadlock/livelock traces.
\end{definition}
%
Note that $\sigma$ is a deadlock/livelock trace of $p$ iff
$(\sigma,A) \in \IF(p)$.
This is the negation of a proper AGEF property, so from
Theorem~\ref{ifrsp} we deduce that $\reqIF$ is the coarsest
w-congruence satisfying RSP and respecting deadlock/livelock traces.
The answer is partial, since there exist congruences that respect deadlock/livelock traces but are not coarser than
$\bis{rw}$, such as branching bisimilarity \cite{IPGla93}. So the existence of (non-w) congruences respecting
deadlock/livelock traces and satisfying RSP that are incomparable with $\reqIF$ is conceivable.

The results in this section can be generalised to a divergence sensitive
setting.  Divergence of a process is the possibility to perform an infinite
sequence of $\tau$ steps. By only allowing to relate divergent
processes to divergent processes, one defines
\emph{weak bisimulation congruence with explicit divergence} (notation $\rwbisimd$) \cite{IPGla93}.
We now relax the requirement in Theorem~\ref{ifrsp} that $\sim$ must be a $w$-congruence.
Instead of requiring $\sim$ to be coarser than $\bis{rw}$ we merely require it
to be coarser than $\rwbisimd$, i.e.\ we use $\rwbisimd$ for $\bis{\rm max}$.
The proof, which is omitted due to lack of space, requires a slight extension of RSP$^*$, still implied by RSP.

\begin{theorem}
$\reqIF$ is the coarsest congruence coarser than $\rwbisimd$, satisfying {\rm RSP}
and respecting deadlock/livelock traces.
\end{theorem}
%
This is a useful addition, because many equivalences in the linear time
-- branching time spectrum of \cite{IPGla93}, such as the CSP failures
equivalence \cite{BHR84}, fail to be coarser than $\bis{rw}$, although
virtually all are coarser than $\rwbisimd$. Moreover, the few
equivalences from \cite{IPGla93} that are not coarser than $\rwbisimd$
are certainly finer than $\eqIF$ or do not respect deadlock/livelock
traces; thus no known equivalence is ruled out by the restriction ``coarser than $\rwbisimd$''.

\section{Conclusion}

We have discussed the connection between AGAF properties, expressing
(conditional) lifeness requirements, AGEF properties, expressing
not-doomed-to-fail requirements, and impossible futures congruence,
which we have characterised, under a
mild side-condition, as the coarsest congruence that allows verification of
testable AGEF properties---or AGAF properties under a global fairness
assumption---and assigns unique solutions to guarded recursive equations.
Thus, where such properties are deemed important, equational system verification
\cite{Ba90} requires a semantic equivalence at least as fine as
impossible futures congruence.

The fact that we have used the operators of CCS bears no relevance. We could
have used any process calculus that allows action prefix, choice, communication
merge, restriction and abstraction, such as CSP, ACP, LOTOS and many others.
%
% In the present paper, we concentrated on weak bisimilarity. With slight
% adaptations, the proofs can be adapted to non-IF congruences coarser than
% $\eta$-delay bisimilarity, with satisfies $\tau(\tau.x+y) \sim
% \tau(\tau.x+y)+\tau.x$ in addition to the equations of branching bisimilarity.
\\[1em]
{\bf Acknowledgement}\\
We are grateful for the support and advice of our colleague Bas Luttik.

\begin{thebibliography}{10}

\bibitem{WpAce03}
{\sc L.~Aceto} (moderator) (2003):
\newblock {\em Some open problems in Process Algebra}.\\
{\small \tt http://www.cs.auc.dk/\~{}luca/BICI/open-problems.html}

\bibitem{Ba90}
{\sc J.C.M. Baeten}, editor (1990):
\newblock {\em Applications of Process Algebra}.
\newblock Cambridge Tracts in Theoretical Computer Science 17. Cambridge University Press.

\bibitem{ArBaBeKl87}
{\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(l/2), pp. 129--176.

\bibitem{ArBlIsMe95}
{\sc B. Bloom, S. Istrael \& A. Meyer} (1995):
\newblock {\em Bisimulation Can't Be Traced}.
\newblock {{\sl Journal of the ACM} 42(1), pp. 232--268.}

\bibitem{IPBrReVo95}
{\sc E. Brinksma, A. Rensink \& W. Vogler} (1995):
\newblock {\em Fair Testing}.
\newblock {In {\sl Proceedings CONCUR '95} (I. Lee \& S.A. Smolka, eds.), LNCS 962, Springer, pp. 311--327.}\\
\newblock Journal preprint: {\small \tt http://eprints.eemcs.utwente.nl/1623/01/submitted.pdf}

\bibitem{BHR84}
{\sc S.D. Brookes, C.A.R. Hoare \& A.W. Roscoe} (1984):
\newblock {\em A theory of communicating sequential processes}.
\newblock {\sl Journal of the ACM} 31(3), pp. 560--599.

\bibitem{IPClEm81}
{\sc E.M. Clarke \& E.A. Emerson} (1981):
\newblock {\em Design and synthesis of synchronization skeletons using branching-time temporal logic.}
\newblock In Proceedings workshop on {\sl Logic of Programs} (D.~Kozen, ed.), {\sl \rm LNCS} 131, Springer, pp. 52--71.

\bibitem{DV95}
{\sc R.~De~Nicola \& F.W. Vaandrager} (1995):
\newblock {\em Three logics for branching bisimulation.}
\newblock {\sl Journal of the ACM} 42(2), pp. 458--487.

\bibitem{BoFra86}
{\sc N. Francez} (1986):
\newblock {\em Fairness}.
\newblock {Springer.}

\bibitem{IPGla93}
{\sc R.J.~van Glabbeek} (1993):
\newblock {\em The Linear Time -- Branching Time Spectrum II: The semantics of sequential systems with silent moves (extended abstract)}.
\newblock In {\sl Proceedings CONCUR '93} (E.~Best, ed.), {\sl \rm LNCS} 715, Springer, pp. 66--81.

\bibitem{vG05}
{\sc R.J.~van Glabbeek} (2005):
\newblock {\em A Characterisation of Weak Bisimulation Congruence}.
\newblock In {\sl Processes, Terms and Cycles: Steps on the Road to
Infinity:} Essays Dedicated to J.W. Klop on the Occasion of His
60th Birthday (A. Middeldorp, V. van Oostrom, F. van
Raamsdonk \& R. de Vrijer, eds.), LNCS 3838, Springer, pp. 26-39.

\bibitem{Mi90ccs}
{\sc R.~Milner} (1990):
\newblock {\em Communication and Concurrency}, Prentice-Hall International, Englewood Cliffs, 1989.
\newblock An earlier version appeared as{ \em A Calculus of Communicating Systems}, LNCS 92, Springer-Verlag, 1980.

\bibitem {BoVog92}
{\sc W. Vogler} (1992):
\newblock{\em Modular Construction and Partial Order Semantics of Petri nets.}
\newblock{LNCS 625, Springer.}

\bibitem{ArVoMa00}
{\sc M. Voorhoeve \& S. Mauw} (2001):
\newblock {\em Impossible Futures and Determinism}.
\newblock {{\sl Information Processing Letters} 80(1), Elsevier, pp. 51--58.}

\end{thebibliography}

%\bibliography{../Stanford/lib/abbreviations,../Stanford/lib/dbase,../Stanford/lib/new}
\end{document}
