\documentclass[leqno,runningheads]{llncs}

\usepackage{amssymb,amsmath}
\usepackage{algorithm,algpseudocode}
\usepackage{subfigure}
\usepackage{url}
\usepackage{times}
\usepackage{xspace}
\usepackage{graphicx}

\title{Correcting a Space-Efficient Simulation Algorithm%
\thanks{This is an extended abstract; all proofs are omitted. They
can be found in the full version \cite{GP08}.}
}
\titlerunning{Correcting a Space-Efficient Simulation Algorithm}
\authorrunning{R.J.\ van Glabbeek \& B.\ Ploeger}

\author{Rob van Glabbeek\inst{1,2} \and 
Bas Ploeger\inst{3}\thanks{This author is partially supported by the
Netherlands Organisation for Scientific Research (NWO) under VoLTS grant
number 612.065.410.}}

\institute{National ICT Australia, Locked Bag 6016, Sydney, NSW1466, Australia
\and
School of Computer Science and Engineering, The University of New South Wales,\\
Sydney, NSW 2052, Australia 
\and 
Eindhoven University of Technology, Design and Analysis of Systems Group,\\
P.O.~Box~513, 5600~MB Eindhoven, The Netherlands}

\def\andname{\&}           % between authors

% theorem-like environments
\spnewtheorem{counterexample}[example]{Counterexample}{\itshape}{\rmfamily}

% itemize using less space
\renewenvironment{itemize}{\begin{list}{$\bullet$}{\leftmargin 18pt
                        \labelwidth\leftmargini\advance\labelwidth-\labelsep
                        \topsep 4pt \itemsep 2pt \parsep 2pt}}{\end{list}}

% References
\newcommand{\Sec}[1]{Sect.~\ref{sec:#1}}
\newcommand{\Fig}[1]{Fig.~\ref{fig:#1}}
\newcommand{\Def}[1]{Definition~\ref{def:#1}}
\newcommand{\Prp}[1]{Proposition~\ref{prp:#1}}
\newcommand{\Lem}[1]{Lemma~\ref{lem:#1}}
\newcommand{\Thm}[1]{Theorem~\ref{thm:#1}}
\newcommand{\Cor}[1]{Corollary~\ref{cor:#1}}
\newcommand{\Cex}[1]{Counterexample~\ref{cex:#1}}
\newcommand{\Exm}[1]{Example~\ref{exm:#1}}

% Latin abbreviations
\newcommand{\ie}{\textit{i.e.}\ }
\newcommand{\eg}{\textit{e.g.}\ }
\newcommand{\etal}{\textit{et al.}\ }

% shorthands for fonts in math environments 
\newcommand{\mc}[1]{\ensuremath{\mathcal{#1}}}
\newcommand{\mr}[1]{\ensuremath{\mathrm{#1}}}
\newcommand{\ms}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\mi}[1]{\ensuremath{\mathit{#1}}}

\newfont{\fsc}{eusm10}      % frenchscript letters

% power set
\newcommand{\power}[1]{\mbox{\fsc P}(#1)}

% booleans
\newcommand{\bimp}{\mathbin{\Leftrightarrow}}
\newcommand{\imp}{\mathbin{\Rightarrow}}

% simulation preorder and equivalence
\newcommand{\smin}{\stackrel{\raisebox{-3pt}{$\textstyle\subset\,$}}%
{\raisebox{-3pt}{$\scriptstyle\rightarrow$}}} % simulation inclusion

\newcommand{\smeq}{\stackrel{\rightarrow}{\raisebox{0pt}[1pt][0pt]%
{$\scriptstyle \leftarrow$}}}			% simulation

% no vertical space
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}}

% identity relation over a set
\newcommand{\idty}[1]{\ensuremath{\mc{I}({#1})}}

% partition pair
\newcommand{\pp}[2]{\ensuremath{{\langle #1, #2 \rangle}}}

% Algorithm names
\newcommand{\PAGPP}{\ensuremath{\textsc{PA}_\textsc{GPP}}\xspace}
\newcommand{\RefineGPP}{\ensuremath{\textsc{Refine}_\textsc{GPP}}\xspace}
\newcommand{\UpdateGPP}{\ensuremath{\textsc{Update}_\textsc{GPP}}\xspace}
\newcommand{\PA}{\textsc{PA}\xspace}
\newcommand{\Refine}{\textsc{Refine}\xspace}

\begin{document}
\maketitle
\setcounter{footnote}{0}

\begin{abstract}
\noindent
Although there are many efficient algorithms for calculating the
simulation preorder on finite Kripke structures, only two have been
proposed of which the space complexity is of the same order as the size
of the output of the algorithm. Of these, the one with the best time
complexity exploits the representation of the simulation problem as a
generalised coarsest partition problem. It is based on a fixed-point
operator for obtaining a generalised coarsest partition as the limit of
a sequence of partition pairs.  We show that this fixed-point theory is
flawed, and that the algorithm is incorrect. Although we do not see how
the fixed-point operator can be repaired, we correct the algorithm
without affecting its space and time complexity.

\end{abstract}

\section{Introduction}

The \emph{simulation preorder} \cite{Par:81} is a behavioural
refinement relation on concurrent systems, represented as Kripke
structures or labelled transition systems, that plays a crucial r\^ole
in compositional verification and model checking.  It preserves the
existential and universal fragments of temporal and modal logics. For
CTL$^*$ \cite{EH:86} this is shown in \cite{DGG:93}, and for the modal
$\mu$-calculus \cite{Koz:83} it is shown in \cite{LGS+:95}.
This makes it possible to combat the state explosion problem in model
checking by minimising the state space of a given system modulo
simulation equivalence before checking the validity of relevant
properties within those fragments.  Given that the simulation preorder
is a precongruence for parallel composition \cite{GrV92}, components
in parallel compositions can even be minimised individually.

Simulation equivalence is also used directly in equivalence checking
\cite{KJ06} of finite-state processes.
Often deciding the simulation preorder between processes is the most
appropriate method of showing that two systems are related by another
preorder, that may be appropriate for the task at hand.
In applications where deadlock behaviour plays a crucial r\^ole,
the \emph{ready simulation preorder} \cite{BIM:95} is widely regarded
to be an appropriate behavioural refinement relation for matching an
implementation with a specification. Via a straightforward reduction
(the computation of the initial partition ${\it ER}_1$ in \cite{BP:95}),
finding a ready simulation between two processes is as hard as finding
a plain simulation. 
In applications where deadlock behaviour plays no r\^ole, \emph{trace
inclusion} is often proposed as an appropriate refinement relation.
However, deciding trace inclusion on finite-state processes is
PSPACE-hard \cite{SM:73}, and as the simulation preorder is the
coarsest preorder included in trace inclusion that is known to be
decidable in polynomial time \cite{BP:95,BG:03,GPP:03,HHK:95,RT:07,TC:01},
establishing a simulation between two processes is a favourite way of
showing that they are related by trace inclusion.

In many crucial applications, space rather than time becomes the
bottleneck as the input graph grows \cite{CVW+:90,EP:05,GPP:03,Hol:88}.
Hence, simulation algorithms with minimal space complexity are of
particular interest.  These are the ones by Bustan and Grumberg
\cite{BG:03} and by Gentilini, Piazza and Policriti \cite{GPP:03}.
For an input graph with $N$ states, $T$ transitions and $S$ simulation
equivalence classes, the space complexity of both algorithms is
$\mc{O}(S^2 + N \log S)$.  This can be considered minimal:
$\mc{O}(S^2)$ space is needed for storing the simulation preorder
as a partial order on simulation equivalence classes and
$\mc{O}(N \log S)$ space is needed to store for every state, the
equivalence class to which it belongs.  Of these algorithms, the one
by Gentilini \etal has a better time complexity: $\mc{O}(S^2 T)$.  A
more time-efficient algorithm is the one by Ranzato and Tapparo
\cite{RT:07}, but it is less space efficient.

The approach of Gentilini \etal represents the simulation problem as a
generalised coarsest partition problem (GCPP).  According to the
authors, this problem can be solved by approximating the greatest fixed point
of a decreasing operator on partition pairs that they define in their paper.
They give a partitioning algorithm to compute this fixed point
for any legal input. We recite this definition and a part of the
algorithm in \Sec{GPPsolution}. In \Sec{incorrect-operator} we show
that the operator is flawed because it is not uniquely defined for all
partition pairs.
We give an instance of the GCPP for which repeated application of the
operator does not lead to a unique fixed point. We also show that on this example
the partitioning algorithm irrevocably allocates two
simulation-equivalent states to different simulation-equivalence
classes, and subsequently deadlocks.

In \Sec{rho-operator} we define a simple, yet inefficient fixed-point
operator for which we prove correctness.  This operator is not meant to
be an improvement over the original one, but merely serves as an
expedient for establishing correctness of the algorithm that we present
in \Sec{correct-algorithm}. This algorithm is obtained from that of
Gentilini \etal by means of a few simple corrections; consequently,
it benefits from the key ideas behind the original partitioning
algorithm and has the same time and space complexities.
Yet its correctness proof requires entirely new techniques and is
surprisingly non-trivial.  We also show that no fixed-point operator
can be defined that captures the behaviour of this algorithm.

\section{Preliminaries}
\label{sec:prelim}

\paragraph{Partitions and relations.} For any set $S$, a \emph{partition} over
$S$ is a set $\Sigma \subseteq \power{S}$ such that $\bigcup \Sigma = S$ and
$\forall \alpha \in \Sigma ~.~ \alpha \neq \emptyset \land \forall \beta \in
\Sigma ~.~ \alpha \neq \beta \imp \alpha \cap \beta = \emptyset$.  For any $s\in
S$ we denote by $[s]_\Sigma$ the block $\alpha \in \Sigma$ such that
$s\in\alpha$. Given two partitions $\Sigma$ and $\Pi$ we say $\Pi$ \emph{is
finer than} $\Sigma$ iff for every $\alpha \in \Pi$ there exists an $\alpha' \in
\Sigma$ such that $\alpha \subseteq \alpha'$.
For any set $S$, we denote by $\idty{S}$ the \emph{identity relation}
over $S$, \ie $\idty{S} = \{ (s,s) \mid s \in S \}$. For any relation
$P$, we denote by $P^+$ the \emph{transitive closure} of $P$. 

\paragraph{Graphs.}
A \emph{(directed) graph} is a tuple $(N,\to)$ where $N$ is a finite set of nodes and
${\to} \subseteq N \times N$ is a set of directed transitions between those nodes.  A
\emph{labelled graph} is a tuple $(N,\to,\Sigma)$ where $(N,\to)$ is a graph
and $\Sigma$ is a partition over $N$.
For a graph $(N,\to)$, $a \in N$ and $\beta \subseteq N$, we write $a \to
\beta$ if $\exists b \in \beta ~.~ a \to b$. Moreover, we define the relations
$\to_\exists$ and $\to_\forall$ over $\power{N}$
as follows, for any $\alpha,\beta \subseteq N$:
\begin{align*}
\alpha \to_\exists \beta & \;\bimp\; \exists a\in \alpha ~.~ a \to \beta
&
\alpha \to_\forall \beta & \;\bimp\; \forall a\in \alpha ~.~ a \to \beta.
\end{align*}

\paragraph{Simulations.}
For any labelled graph $(N,\to,\Sigma)$ a relation $R \subseteq N \times N$ is a
\emph{simulation} iff for any $a,b \in N$, $(a,b) \in R$ implies:
\begin{itemize}
  \item $[a]_\Sigma = [b]_\Sigma$ and
  \item $\forall c \in N ~.~ a \to c \;\imp\; \exists d \in N ~.~ b \to d \land
    (c,d) \in R$.
\end{itemize}
We say that $a$ is {\it simulated by} $b$, denoted $a \smin b$, iff there
exists a simulation $R$ such that $(a,b) \in R$. It is well known and
easy to check that $\smin$ is a preorder, \ie a reflexive and
transitive relation, on $N$, and moreover the largest simulation. We
say that $a$ and $b$ are \emph{simulation equivalent}, denoted $a \smeq b$,
iff $a \smin b$ and $b \smin a$.

\paragraph{The simulation problem.}
Given a labelled graph $G = (N,\to,\Sigma)$, the \emph{simulation problem} over
$G$ consists in finding the simulation preorder $\smin$ on $G$.

A variant of the simulation problem asks, given a labelled graph
$(N,\to,\Sigma)$ and two nodes $a,b \in N$, whether $a \smin b$.
In general, no methods to solve this problem are known that are more
efficient than computing the entire relation $\mathord{\smin} \subseteq
N\times N$ and looking up whether $(a,b) \in \mathord{\smin}$.
Another variant of the simulation problem merely asks to find the
simulation equivalence relation $\smeq$ rather than the preorder $\smin$.
Again, no methods to solve that problem are known that do not amount
to finding $\smin$ as well.

Typically, the simulation problem arises in the context of \emph{Kripke
structures} or \emph{labelled transition systems}.  It is trivial to encode a
Kripke structure as a labelled graph in such a way that the simulation preorder
on the Kripke structure agrees with the one on its labelled graph representation.
Likewise, it is not hard to reduce the simulation problem for labelled transition
systems to that for labelled graphs.  Alternatively one can enrich the theory in
a straightforward way to deal with transition labels as well, so that it is
applicable to labelled transition systems directly.

\paragraph{The generalised coarsest partition problem.}
Given a graph $G = (N,\to)$, a \emph{partition pair} over $G$ is a pair
$\pp{\Sigma}{P}$ where $\Sigma$ is a partition over $N$ and $P \subseteq
\Sigma \times \Sigma$ is a reflexive, acyclic relation over $\Sigma$. A
partition pair $\pp{\Sigma}{P}$ is called \emph{transitive} if $P$ is
transitive, and hence a partial order. Given a partition
$\Sigma$, a partition $\Pi$ finer than $\Sigma$, and a relation $P$ over
$\Sigma$, we denote by $P(\Pi)$ the \emph{induced relation} of $P$ on $\Pi$:
\[
P(\Pi) = \{ (\alpha,\beta) \in \Pi \times \Pi \mid \exists (\alpha',\beta') \in
P ~.~ \alpha \subseteq \alpha' \land \beta \subseteq \beta' \}.
\]

\noindent
We define a \emph{partial order $\leq$} on partition pairs by writing,
for any partition pairs $\pp{\Sigma}{P}$ and $\pp{\Pi}{Q}$: $\pp{\Pi}{Q}
\leq \pp{\Sigma}{P}$ iff $\Pi$ is finer than $\Sigma$ and $Q \subseteq
P(\Pi)$.
Given a graph $G = (N,\to)$, we say a partition pair $\pp{\Sigma}{P}$ over $G$
is \emph{stable with respect to $\to$} \cite{GPP:03} iff:
\[
\forall \alpha,\beta,\gamma \in \Sigma ~.~ ((\alpha,\beta) \in P \land \alpha
\to_\exists \gamma) \;\imp\; \exists \delta \in \Sigma ~.~ (\gamma,\delta) \in P
\land \beta \to_\forall \delta.
\]

\noindent
Given a graph $G = (N,\to)$ and a partition pair $\pp{\Sigma}{P}$ over $G$, the
\emph{generalised coarsest partition problem} (GCPP) \cite{GPP:03} consists in
finding a $\leq$-maximal partition pair $\pp{\Xi}{\preceq}$ such that
$\pp{\Xi}{\preceq} \leq \pp{\Sigma}{P^+}$ and $\pp{\Xi}{\preceq}$ is
stable with respect to $\to$.

\paragraph{The simulation problem as a GCPP.}
Let $G=(N,\rightarrow,\Sigma)$ be a labelled graph.
Any preorder $\sqsubseteq$ on $N$ can be represented as a partition
pair $\ms{PP}(\sqsubseteq):=\pp{\Pi}{\preceq}$, as follows: $\Pi$
is the set of equivalence classes of $N$ w.r.t.\ the
equivalence relation $\mathord\equiv := \mathord\sqsubseteq \cap
\mathord{\sqsubseteq^{-1}}$ induced by $\sqsubseteq$, and $\preceq$ is
given by $[a]_\Pi \preceq [b]_\Pi$ iff $a \sqsubseteq b$. Note that
$\preceq$ is a partial order. Moreover, if $\sqsubseteq$ is a simulation then
$\ms{PP}(\sqsubseteq)$ is stable w.r.t.\ $\rightarrow$ and
$\ms{PP}(\sqsubseteq)\leq \pp{\Sigma}{\idty{\Sigma}}$.

Any partition pair $\pp{\Pi}{Q}$ over the graph $(N,\to)$ can be represented as
a relation $R_{\pp{\Pi}{Q}} \subseteq N \times N$ as follows:
$(a,b) \in R_{\pp{\Pi}{Q}}$ iff $\exists (\alpha,\beta) \in Q ~.~
  a\in \alpha \wedge b\in \beta$.
Note that if $\pp{\Pi}{Q}$ is stable w.r.t.\ $\rightarrow$ and $\pp{\Pi}{Q}\leq
\pp{\Sigma}{\idty{\Sigma}}$ then $R_{\pp{\Pi}{Q}}$ is a simulation.
Moreover, $\pp{\Pi}{Q}\leq\pp{\Pi'}{Q'}$ iff $R_{\pp{\Pi}{Q}} \subseteq R_{\pp{\Pi'}{Q'}}$.
Also note that $R_{\ms{PP}(\sqsubseteq)} = \mathord\sqsubseteq$.

Hence $\ms{PP}(\smin)$ is the solution of the GCPP on
$(N,\rightarrow)$ and \pp{\Sigma}{\idty{\Sigma}}. In particular, the
GCPP, when applied to partition pairs of the form
\pp{\Sigma}{\idty{\Sigma}} (plain partitions), always has a unique
solution \pp{\Xi}{\preceq}, in which moreover $\preceq$ is always a
partial order.%
\footnote{The same reasoning extends to the GCPP applied to any
    partition pairs, but this requires considering simulations on
    structures of the form $(N,\rightarrow,\Sigma,\preceq)$ with
    \mbox{$(N,\rightarrow,\Sigma)$} a labelled graph, and $\preceq$ a partial
    order on $\Sigma$; the first clause in the definition of
    simulation then becomes  $[a]_\Sigma \preceq [b]_\Sigma$.}

\section{The GCPP Solution of Gentilini, Piazza and Policriti}
\label{sec:GPPsolution}

To solve the GCPP, Gentilini, Piazza and Policriti \cite{GPP:03}
introduce the following operator:

\begin{trivlist}\item
\textbf{Definition~4.11 in \cite{GPP:03} (Operator $\sigma$).}
Let $G \!=\! (N,\to)$ and $\pp{\Sigma}{P}$ be a partition pair over $G$.
The partition pair $\pp{\Pi}{Q} = \sigma(\pp{\Sigma}{P})$ is defined
as follows:

\begin{minipage}{11cm}
\par\medskip
\begin{itemize}
  \item[$(1\sigma)$] $\Pi$ is the coarsest partition finer than $\Sigma$ such that
    \begin{itemize}
      \item[(a)]
        $\forall \alpha \in \Pi ~ \forall \gamma \in \Sigma (\alpha
        \to_\exists \gamma \;\imp\; \exists \delta \in \Sigma ((\gamma,\delta)\in
        P \land \alpha \to_\forall \delta))$;
    \end{itemize}
  \item[$(2\sigma)$] $Q$ is maximal such that $Q \subseteq P(\Pi)$ and if
    $(\alpha,\beta) \in Q$, then
    \begin{itemize}
      \item[(b)]
        $\forall \gamma \in \Sigma (\alpha \to_\forall \gamma \;\imp\; \exists
        \gamma' \in \Sigma ((\gamma,\gamma')\in P \land \beta \to_\exists
        \gamma'))$ and
      \item[(c)]
        $\forall \gamma \in \Pi (\alpha \to_\forall \gamma \;\imp\; \exists
        \gamma' \in \Pi ((\gamma,\gamma')\in Q \land \beta \to_\exists \gamma'))$.
    \end{itemize}
\end{itemize}
\end{minipage}
\end{trivlist}
They argue that applying $\sigma$ iteratively on an initial partition
pair $\pp{\Sigma_0}{P_0}$ yields a sequence of partition pairs
$\pp{\Sigma_i}{P_i}_{i\geq0}$ with $\pp{\Sigma_{i+1}}{P_{i+1}} =
\sigma(\pp{\Sigma_i}{P_i})$. By construction, this sequence is decreasing, in
the sense that $\pp{\Sigma_{i+1}}{P_{i+1}} \leq \pp{\Sigma_i}{P_i}$. Hence
it will reach a fixed point $\pp{\Sigma_k}{P_k} =
\sigma(\pp{\Sigma_k}{P_k})$. This is the solution to the GCPP.

\begin{algorithm}[ht]
\caption{The partitioning algorithm of \cite{GPP:03}:
$\PAGPP((N,\to),\pp{\Sigma}{P})$}
\label{alg:pa-gpp}
\begin{algorithmic}[1]
\State ${\it change} := \top$; $i := 0$; $\Sigma_0 := \Sigma$; $P_0 := P$;
\While{${\it change}$}
\State ${\it change} := \bot$;
\State $\Sigma_{i+1} := \RefineGPP(\Sigma_i,P_i,{\it change})$;
\label{line:refinecall}
\State $P_{i+1} := \UpdateGPP(\Sigma_i,P_i,\Sigma_{i+1})$;
\State $i := i+1$;
\EndWhile
\end{algorithmic}
\end{algorithm}

\begin{algorithm}
\caption{The refine function of \cite{GPP:03}: \RefineGPP{$(\Sigma_i,P_i,{\it
change})$}}
\label{alg:refine-gpp}
\begin{algorithmic}[1]
  \State $\Sigma_{i+1} := \Sigma_i$;
  \State {\bf for all} $\alpha \in \Sigma_{i+1}$ {\bf do}
    ${\it Stable}(\alpha) := \emptyset$; {\bf end for}
  \State {\bf for all} $\gamma \in \Sigma_{i}$ {\bf do}
    ${\it Row}(\gamma) := \{\gamma' \mid (\gamma,\gamma') \in P_i \}$; {\bf end for}
    \label{line:row}
  \State Let ${\it Sort}$ be a reverse topological sorting of $\Sigma_i$
  w.r.t.\ $P_i$;
  \label{line:revtopsort}
  \While{${\it Sort} \neq \emptyset$}
    \State $\gamma := dequeue({\it Sort})$;
      \State $A := \emptyset$;
      \ForAll{$\alpha \in \Sigma_{i+1}$, $\alpha \to_{\exists} \gamma$,
       ${\it Stable}(\alpha) \cap {\it Row}(\gamma) = \emptyset$}
        \State $\alpha_1 := \alpha \cap {\to^{-1}}(\gamma)$;
        \State $\alpha_2 := \alpha \setminus \alpha_1$;
        \State {\bf if} {$\alpha_2 \neq \emptyset$} {\bf then} ${\it change} := \top$;
        {\bf end if}
        \State $\Sigma_{i+1} := \Sigma_{i+1} \setminus \{\alpha\}$;
        \State $A := A \cup \{\alpha_1,\alpha_2\}$;
        \State ${\it Stable}(\alpha_1) := {\it Stable}(\alpha) \cup \{ \gamma \}$;
        \State ${\it Stable}(\alpha_2) := {\it Stable}(\alpha)$;
      \EndFor
      \State $\Sigma_{i+1} := \Sigma_{i+1} \cup A$;
      \State ${\it Sort} := {\it Sort} \setminus \{ \gamma \}$;
  \EndWhile
  \State \Return $\Sigma_{i+1}$;
\end{algorithmic}
\end{algorithm}

Applying this, they give a partitioning algorithm to solve the GCPP\@. We have
included it here as Algorithm~\ref{alg:pa-gpp} and call it \PAGPP.
It takes as input a graph $(N,\to)$ and a transitive partition pair
$\pp{\Sigma}{P}$ and repeatedly calls the following functions to compute
$\sigma$ until a fixed point is reached: \RefineGPP which computes the
partition $\Pi$ of $(1\sigma)$ and \UpdateGPP which computes the relation $Q$
of $(2\sigma)$.
The boolean variable ${\it change}$ is set to $\top$ by \RefineGPP iff
its output partition differs from its input partition.
We have included the \RefineGPP function as Algorithm~\ref{alg:refine-gpp}.
In line~\ref{line:revtopsort} of this algorithm, a ``reverse topological sorting
of $\Sigma_i$ w.r.t.\ $P_i$'' indicates an ordered listing of the elements of
$\Sigma_i$ such that if $(\gamma,\delta) \in P_i$ then $\delta$ occurs prior to
$\gamma$.

\section{Incorrectness of the Fixed-Point Operator}
\label{sec:incorrect-operator}

\begin{figure}[t]
\centering
\subfigure[]{
\centering
\label{fig:acyclic-counter}
\includegraphics{acyclic-counter}
}
\hspace{1cm}
\subfigure[]{
\centering
\label{fig:function-counter}
\includegraphics{function-counter}
}
\caption{Counterexamples for (a) acyclicity of $Q$ and (b) well-definedness of
$\sigma$.}
\end{figure}

Following the definition of $\sigma$, the authors claim that for any partition
pair $\pp{\Sigma}{P}$, if $\pp{\Pi}{Q} = \sigma(\pp{\Sigma}{P})$ then $Q$
is acyclic. We give an example that counters this claim.

\begin{counterexample}
Consider the graph in \Fig{acyclic-counter} and the partition pair
$\pp{ \Sigma}{ P }$ with $\Sigma = \{\alpha,\beta,\gamma,\delta\}$ as
depicted and
$P = \idty{\Sigma} \cup \{(\beta,\!\delta),(\delta,\!\gamma)\}$.
Let $\pp{\Pi}{Q} = \sigma(\pp{\Sigma}{P})$, then
\begin{align*}
\Pi &= \{ \alpha_1, \alpha_2, \beta, \gamma, \delta \} &
Q &= \idty{\Pi} \cup \{ (\alpha_1,\alpha_2), (\alpha_2,\alpha_1),
(\beta,\delta), (\delta,\gamma) \}
\end{align*}
where $\alpha_1 = \{a_1\}$ and $\alpha_2 = \{a_2\}$. $Q$ is not acyclic, which
counters the claim. \qed\pagebreak[2]
\end{counterexample}

\noindent This counterexample shows that applying $\sigma$ to a given partition
pair does not necessarily yield another partition pair.
After all, for that the resulting relation has to be acyclic.

However, a more fundamental theorem that the authors claim to have
proven, turns out not to hold. Theorem~4.13 states that for every
partition pair $\pp{\Sigma}{P}$ there exists a unique $\leq$-maximal
partition pair $\pp{\Pi}{Q} \leq \pp{\Sigma}{P}$ satisfying conditions (a), (b)
and (c) of Definition~4.11, \ie the $\sigma$ operator is well-defined, and a
function. This theorem is countered by the following example.

\begin{counterexample}
\label{cex:not-unique}
Consider the graph in \Fig{function-counter} and the partition pair
$\pp{\Sigma}{P}$ with $\Sigma = \{\alpha,\beta,\gamma,\delta\}$ as depicted
and $P = \idty{\Sigma} \cup \{(\beta,\gamma), (\gamma,\delta)\}$. Let
$\pp{\Pi}{Q}$ and $\pp{\Pi'}{Q'}$ be partition pairs such that:
\begin{align*}
\Pi &= \{ \alpha_0,\alpha_1, \beta,\gamma,\delta \} &
Q &= \idty{\Pi} \cup \{(\alpha_0,\alpha_1), (\alpha_1,\alpha_0), (\beta,\gamma),
(\gamma,\delta)\}\\
\Pi' &= \{ \alpha_0',\alpha_1', \beta,\gamma,\delta \} &
Q' &= \idty{\Pi'} \cup \{(\alpha_0',\alpha_1'), (\alpha_1',\alpha_0'),
(\beta,\gamma), (\gamma,\delta)\}
\end{align*}
where $\alpha_0 = \{a_0,a_1\}$, $\alpha_1 = \{a_2\}$, $\alpha_0' = \{ a_0\}$
and $\alpha_1' = \{a_1,a_2\}$. Both $\pp{\Pi}{Q}$ and $\pp{\Pi'}{Q'}$ satisfy
conditions {\rm(a)}, {\rm(b)} and {\rm(c)} of Definition~4.11, but neither is
the $\leq$-largest. The only partition pair
greater than both $\pp{\Pi}{Q}$ and $\pp{\Pi'}{Q'}$ and at most as large as
$\pp{\Sigma}{P}$, is $\pp{\Sigma}{P}$ itself, but $\pp{\Sigma}{P}$ does not
satisfy {\rm(a)}. Hence, this example counters Theorem~4.13 of
\cite{GPP:03} and shows that $\sigma$ is not well-defined.
\qed
\end{counterexample}

\noindent
Following Theorem~4.13, the authors present their main fixed-point theorem which
states that the solution of the GCPP over a graph $G$ and partition pair $\pp{
\Sigma}{P }$ can be computed by applying $\sigma$ to $\pp{\Sigma}{P}$ finitely
many times until a fixed point is reached (Theorem~4.14). In this theorem, the
authors demand that $P$ be transitive. One might be inclined to think that
\Cex{not-unique} does not affect this theorem, as we used a
non-transitive $P$. We now show that this is not the case: the main
theorem indeed loses its meaning due to our counterexample for Theorem~4.13. To
do so, we first give an example in which the application of $\sigma$ to a
transitive partition pair produces a non-transitive partition pair.

\begin{figure}
\centering
\subfigure[]{
\label{fig:non-transitive}
\includegraphics{non-transitive}
}
\hspace{0.5cm}
\subfigure[]{
\label{fig:final-counter}
\centering
\includegraphics{final-counter}
}
\caption{(a) Example for which $\sigma$ produces a non-transitive relation $Q$
and (b) counterexample for correctness of $\sigma$.}
\end{figure}

\begin{example}
\label{exm:non-transitive}
Consider the graph in \Fig{non-transitive} and the partition pair
$\pp{\Sigma}{P}$ with $\Sigma = \{\alpha, \beta, \gamma\}$ as depicted and $P
= \idty{\Sigma}$. Let $\pp{\Pi}{Q} = \sigma(\pp{\Sigma}{P})$, then:
\begin{align*}
\Pi & = \{\alpha_1,\alpha_2,\alpha_3,\beta,\gamma\} &
Q & = \idty{\Pi} \cup \{(\alpha_3,\alpha_1),(\alpha_1,\alpha_2)\}
\end{align*}
where $\alpha_1 = \{ a_0,a_1\}$, $\alpha_2 = \{a_2\}$ and $\alpha_3 = \{a_3\}$.
\qed
\end{example}

\noindent
Our final counterexample shows that $\sigma$ is not suitable for computing the
solution of the GCPP, and is constructed by embedding
\Cex{not-unique} in \Exm{non-transitive}, such that
the first application of $\sigma$ produces a non-transitive partition pair on
which $\sigma$ is not well-defined.

\begin{counterexample}
\label{cex:final}

Consider the graph in \Fig{final-counter} and the partition pair
$\pp{\Sigma}{P}$ with $\Sigma = \{\alpha,\beta,\gamma\}$ as depicted and $P =
\idty{\Sigma}$. Let $\pp{\Pi}{Q} = \sigma(\pp{\Sigma}{P})$, then:
\begin{align*}
\Pi & = \{ \alpha_1, \alpha_2, \alpha_3, \beta, \gamma \} &
Q & = \idty{\Pi} \cup \{ (\alpha_3,\alpha_1), (\alpha_1,\alpha_2) \}
\end{align*}
where $\alpha_1 = \{ a_0,a_1 \}$, $\alpha_2 = \{ a_2 \}$ and $\alpha_3 = \{ a_3,
a_4, a_5 \}$. Now, in $\pp{\Pi}{Q}$ the block $\alpha_3$ has to be
split, because $\alpha_3 \to_\exists \alpha_3$ but $\neg \exists
\delta \in \Pi ~.~ ((\alpha_3,\delta)\in Q \land \alpha_3
\to_\forall \delta))$.
There are two candidate
partition pairs for $\sigma(\pp{\Pi}{Q})$: $\alpha_3$ can be split into either
$\alpha_{3,0} = \{ a_4 \}$ and $\alpha_{3,1} = \{ a_3,a_5 \}$ or $\alpha_{3,0}'
= \{ a_4,a_5 \}$ and $\alpha_{3,1}' = \{ a_3 \}$. However, neither of these is
greater than the other, so a unique $\leq$-maximal partition pair does not
exist. \qed
\end{counterexample}

\noindent
When splitting $\alpha_3$ in \Cex{final}, the \RefineGPP
function of algorithm \PAGPP splits the block into $\alpha_{3,0}$ and
$\alpha_{3,1}$.
Observe that this is wrong: $a_4$ and $a_5$ should not end up in different
equivalence classes because $a_4 \smeq a_5$.
This split also results in \UpdateGPP's returning a cyclic relation.
In the subsequent iteration of \PAGPP, the execution of \RefineGPP then fails
because there is no reverse topological sorting of the partition w.r.t. the
cyclic relation (line \ref{line:revtopsort}).

\section{An Auxiliary Fixed-Point Operator}
\label{sec:rho-operator}

In this section we introduce a fixed-point operator $\rho$ to solve the
GCPP and prove its correctness.
The definition of $\rho$ is straightforward: it is based directly on the
stability condition of \Sec{prelim}.

We emphasise that $\rho$ is not intended to be an improvement over the $\sigma$
operator of \Sec{GPPsolution} in any way:
it is a less advanced operator than $\sigma$ aimed to be.
The purpose of $\sigma$ was to compute the solution to the GCPP efficiently,
while $\rho$ gives rise to an algorithm that has an inferior time complexity of
$\mc{O}(S^3 T)$ where $S$ is the number of equivalence classes of the GCPP
solution and $T$ the number of transitions of the input graph.

Namely, the complexity analysis of \cite{GPP:03} uses that, as long
as no fixed point is reached, in each refinement-update step the refinement
of the partition will be non-trivial, \ie the number of blocks
increases.  As a consequence, there will be at most $S$
refinement-update steps before the algorithm terminates. Such an
analysis is not appropriate for $\rho$: applying $\rho$ repeatedly
could involve many steps in which the partition
does not change.  Consequently, the number of
iterations of the algorithm is bounded merely by the size of a
relation on the eventual partition, \ie by $S^2$.

The sole purpose of $\rho$ is to serve as an auxiliary operator for establishing
the correctness of the algorithm that we present in
\Sec{correct-algorithm}.
That algorithm has the same time complexity as \PAGPP and does not correspond to
any fixed-point operator, as we show in the same section.

\begin{definition}[Operator $\rho$] \label{def:rho}
Let $\pp{\Sigma}{P}$ be a transitive partition pair over a graph $(N,{\to})$.
Then $\rho(\pp{\Sigma}{P})$ is the $\leq$-largest partition pair
$\pp{\Pi}{Q}\leq\pp{\Sigma}{P}$ satisfying
\begin{equation}\label{rho}
\forall \alpha,\beta\mathbin\in\Pi ~.~ \forall \gamma \mathbin\in \Sigma ~.~
        ((\alpha,\beta)\mathbin\in Q \land \alpha \to_\exists \gamma \;\imp\; \exists
        \delta \mathbin\in \Sigma ~.~ ((\gamma,\delta)\mathbin\in P \land \beta \to_\forall
        \delta)).
\end{equation}
\end{definition}

\noindent
Alternatively, $\rho$ could be defined just like $\sigma$ of
Definition~4.11, but insisting that its input partition pair is
transitive, and omitting clause (c). It is not hard to check that this
definition is equivalent to the one above.
The correctness of \Def{rho} is ensured by the following.

\begin{proposition} \label{prp:uniqueRho}
Let $\pp{\Sigma}{P}$ be a transitive partition pair over a graph
$(N,\to)$.
Then there exists a $\leq$-largest partition pair 
$\pp{\Pi}{Q}\leq\pp{\Sigma}{P}$ that satisfies \eqref{rho}.
Moreover, $Q$ is transitive.
\end{proposition}

\begin{proposition} \label{prp:monotony}
The operator $\rho$ is monotone with respect to $\leq$:
if $\pp{\Sigma}{P}$ and $\pp{\Sigma'}{P'}$ are transitive partition
pairs with $\pp{\Sigma}{P}\leq\pp{\Sigma'}{P'}$, then
$\rho(\pp{\Sigma}{P})\leq\rho(\pp{\Sigma'}{P'})$.
\end{proposition}

\noindent
Since $\rho(\pp{\Sigma}{P})\leq\pp{\Sigma}{P}$
and $\leq$ is a partial order on a finite set, we obtain:
\begin{proposition} \label{prp:termination}
Let $\pp{\Sigma}{P}$ be a transitive partition pair over a graph.
Then for some $n \mathbin\geq 0$, $\rho^{n+1}(\pp{\Sigma}{P}) \mathbin=
\rho^{n}(\pp{\Sigma}{P})$, \ie repeated application of $\rho$ leads to a fixed
point.
\end{proposition}

\noindent
The solution to the GCPP over an input graph $G$ and an initial
partition pair $\pp{\Sigma}{P}$ over $G$ can be obtained by repeatedly
applying $\rho$ to $\pp{\Sigma}{P^+}$.  The following lemmata say
that as soon as a fixed point is reached, the resulting partition pair
is stable. Moreover, each of the intermediate partition pairs is
larger than or equal to the solution of the GCPP.  It then follows
that the obtained fixed point is in fact the solution to the GCPP.

\begin{lemma} \label{lem:stable-fixpoint}
Let $\pp{\Sigma}{P}$ be a transitive partition pair over a graph $(N,\to)$.
\\
Then $\rho(\pp{\Sigma}{P}) = \pp{\Sigma}{P}$ if and only if
$\pp{\Sigma}{P}$ is stable with respect to $\to$.
\end{lemma}

\begin{lemma} \label{lem:rho-leq}
Let $\pp{\Sigma}{P}$ and $\pp{\Pi}{Q}$ be partition pairs over a graph
$G$, with $Q$ transitive, and let
$\pp{\Xi}{\preceq}$ be the solution of the GCPP over $G$ and $\pp{\Sigma}{P}$.
If $\pp{\Xi}{\preceq} \leq \pp{\Pi}{Q}$ then $\pp{\Xi}{\preceq} \leq
\rho(\pp{\Pi}{Q})$.
\end{lemma}

\begin{theorem} \label{thm:rho-solves-GCPP}
Let $\pp{\Sigma}{P}$ be a partition pair over a graph $G = (N,\to)$
and $\pp{\Xi}{\preceq}$ be the solution of the GCPP over $G$ and $\pp{\Sigma}{P}$.
Let $n \geq 0$ be such that $\rho^{n+1}(\pp{\Sigma}{P^+}) =
\rho^{n}(\pp{\Sigma}{P^+})$. Then $\rho^{n}(\pp{\Sigma}{P^+}) = \pp{\Xi}{\preceq}$.
\end{theorem}


\section{A Correct and Efficient Algorithm}
\label{sec:correct-algorithm}

\begin{algorithm}
\caption{The repaired partitioning algorithm: $\PA((N,\to),\pp{\Sigma}{P})$}
\label{alg:pa}
\begin{algorithmic}[1]
\State $\Sigma_1 := \Refine(\Sigma,P)$; \label{alg:line-init-refine}
\State $P_1 := \UpdateGPP(\Sigma,P,\Sigma_1)$; \label{alg:line-init-update}
\State ${\it change} := \top$; $i := 1$;
\While{${\it change}$}
  \State ${\it change} := \bot$;
  \State $\Sigma_{i+1} := \Refine(\Sigma_i,P_i)$;
  \State $P_{i+1} := \UpdateGPP(\Sigma_i,P_i,\Sigma_{i+1})$;
  \State $i := i+1$;
\EndWhile
\end{algorithmic}
\end{algorithm}

\begin{algorithm}[t]
\caption{The repaired refine function: \Refine{$(\Sigma,P)$}}
\label{alg:refine}
\begin{algorithmic}[1]
  \State $\Pi := \Sigma$;
  \State {\bf for all} $\alpha \in \Pi$ {\bf do}
    ${\it Stable}(\alpha) := \emptyset$; {\bf end for}
          \label{alg:stable-initialisation}
  \State {\bf for all} $\gamma \in \Sigma$ {\bf do}
    ${\it Row}(\gamma) := \{\gamma' \mid (\gamma,\gamma') \in P \}$; {\bf end for}
  \State Let {\it Sort} be a reverse topological sorting of $\Sigma$
  w.r.t. $P$;
          \label{alg:sort}
  \While{${\it Sort} \neq []$}
    \State $\gamma := {\it head}({\it Sort})$;
      \State $A := \emptyset$;
      \ForAll{$\alpha \in \Pi$, $\alpha \to_{\exists} \gamma$}
          \label{alg:prefix1}
        \If {${\it Stable}(\alpha) \cap {\it Row}(\gamma) = \emptyset$}
          \label{alg:prefix2}
          \State $\alpha_1 := \alpha \cap {\to^{-1}}(\gamma)$;
          \State $\alpha_2 := \alpha \setminus \alpha_1$;
          \State $\Pi := \Pi \setminus \{\alpha\}$;
          \State $A := A \cup \{\alpha_1\}$;
          \State ${\it Stable}(\alpha_1) := {\it Stable}(\alpha) \cup \{ \gamma \}$;
          \label{alg:stable1}
          \If {$\alpha_2 \neq \emptyset$} 
            \State ${\it change} := \top$;
            \State $A := A \cup \{\alpha_2\}$;
            \State ${\it Stable}(\alpha_2) := {\it Stable}(\alpha)$;
          \label{alg:stable2}
          \EndIf
        \Else
          \State ${\it Stable}(\alpha) := {\it Stable}(\alpha) \cup \{\gamma\}$;
          \label{alg:stable3}
          \label{alg:line-bugfix}
        \EndIf
      \EndFor
      \State $\Pi := \Pi \cup A$;
      \State ${\it Sort} := {\it tail}({\it Sort})$;
  \EndWhile
  \State \Return $\Pi$;
\end{algorithmic}
\end{algorithm}

\noindent
Our repaired partitioning algorithm is called \PA, see Algorithm~\ref{alg:pa}. 
The variable {\it change} and the input graph $(N,\to)$ have global scope: they
can be accessed from any function. Note however, that \UpdateGPP does not access
{\it change}.

Our corrections of the algorithm are two. Firstly, it is ensured that at
least two refinement-update steps are taken before the algorithm terminates
(lines~\ref{alg:line-init-refine} and~\ref{alg:line-init-update}).
The necessity of this correction is explained in \Sec{another
correction}. Secondly, the most important error --- the one resulting from the incorrect
$\sigma$ operator --- is repaired by the new \Refine function, Algorithm~\ref{alg:refine}.
It contains a few minor improvements over \RefineGPP: using list notations for
variable {\it Sort} and
preventing empty blocks from being added to $\Pi$. However, the actual
correction is in line~\ref{alg:line-bugfix}: if for some $\gamma \in \Sigma$
and $\alpha \in \Pi$ with $\alpha \to_\exists \gamma$ we have ${\it
Stable}(\alpha) \cap {\it Row}(\gamma) \neq \emptyset$ then we add $\gamma$ to
${\it Stable}(\alpha)$.

We use the $\rho$ operator of \Sec{rho-operator} to prove
correctness of \PA in \Sec{PA correctness}.
Its space and time complexities are the same as for \PAGPP:
no additional space is needed and the corrections do not increase the time
complexity.
Finally, in \Sec{no operator} we show that there is no fixed-point
operator that captures the refinement performed by our \Refine function.

\subsection{The Correction of Another Mistake}
\label{sec:another correction}

Apart from the error in \PAGPP that results from the incorrect $\sigma$
operator, we found another mistake in the algorithm. 
We describe it in this section and propose a solution.
The mistake is shown by the following example.

\begin{trivlist}\item
\begin{minipage}{90mm}
\begin{example}
Consider the graph $G = (N,\to)$ on the right and
the partition pair $\pp{\Sigma}{P}$ with $\Sigma = \{ \alpha,\beta \}$ as
depicted and $P = \idty{\Sigma} \cup \{ (\alpha,\beta) \}$.
Observe that the solution to the GCPP over $G$ and
$\pp{\Sigma}{P}$ is $\pp{\Xi}{\preceq}$ with $\Xi = \{ \alpha_0, \alpha_1, \beta
\}$ and ${\preceq} = \idty{\Xi} \cup \{ (\alpha_1,\alpha_0) \}$ where $\alpha_i =
\{ a_i \}$.
After the first iteration of $\PAGPP(G,\pp{\Sigma}{P})$, we have $\Sigma_1
= \Sigma_0 = \Sigma$ and $P_1 = \idty{\Sigma}$.
The algorithm then terminates because ${\it change} = \bot$, and
$\pp{\Sigma_1}{P_1}$ is its answer to the GCPP over $G$ and $\pp{\Sigma}{P}$. 
Obviously $\pp{\Sigma_1}{P_1} \neq \pp{\Xi}{\preceq}$, so this answer is wrong.
\qed
\end{example}
\end{minipage}
\hspace{2mm}
\begin{minipage}{28mm}
\includegraphics{minor-mistake}
\end{minipage}
\end{trivlist}

\noindent
The correctness of \PAGPP hinges on the theory that whenever
$\RefineGPP\hspace{-.3pt}(\Pi,\!Q,\!{\it change}\hspace{-0.62411pt})\hspace{-.8pt}$
returns its input partition $\Pi$,
and thus fails to split any block in $\Pi$, then also the relation $Q$
will be unaffected by \UpdateGPP, \ie $\UpdateGPP(\Pi,Q,\Pi)$ returns
$Q$.
This theory is the upshot of Theorem~4.15 in \cite{GPP:03} and is
essential in the complexity analysis of the algorithm.
However, the above example shows that it does not hold in general.

In the next section we show that this theory does hold under the
condition that $Q$ itself is obtained as output of \UpdateGPP
(\Prp{complexity}).  Therefore, this error in \PAGPP
can be fixed, without violating the complexity analysis, by insisting
that at least two refinement-update steps are performed prior to
termination.

\subsection{Correctness of PA}
\label{sec:PA correctness}

From here on we will use the correctness of the function \UpdateGPP,
as established by Gentilini \etal \cite{GPP:03-TR}. This
correctness can be summarised as follows:

\begin{proposition} \label{prp:uniqueQ2}
Let $\pp{\Sigma}{P}$ be a partition pair over a graph $(N,\rightarrow)$,
and $\Pi$ be a partition over $N$ that is finer than $\Sigma$.
Then there exists a unique relation $Q \subseteq P(\Pi)$ satisfying
condition $(2\sigma)$ of Definition~4.11. Moreover, this relation is
returned by $\UpdateGPP(\Sigma,P,\Pi)$.
\end{proposition}

\noindent
Using this, we obtain the result promised in \Sec{another correction}:
the following proposition implies that if a call to \Refine in the while-loop
of \PA does not split any blocks, then the subsequent call to \UpdateGPP
will return its input relation.
The requirement that this relation has been computed by a previous call to
\UpdateGPP is guaranteed by line~\ref{alg:line-init-update}.

\begin{proposition} \label{prp:complexity}
Let $\pp{\Sigma}{P}$ and $\pp{\Pi}{Q}$ be partition pairs over a graph
such that $\Pi$ is finer than $\Sigma$ and $\UpdateGPP(\Sigma,P,\Pi)$
returns $Q$.
Then $\UpdateGPP(\Pi,Q,\Pi)$ also returns $Q$.
\end{proposition}

\noindent
Let $\pp{\Sigma_i}{P_i}_{1\leq i\leq k}$ be the sequence of partition pairs
produced by \PA.
The following proposition says that every $P_i$ is acyclic and that the
sequence is decreasing.
The former implies that \PA will never deadlock due to the inability to find a
reverse topological sorting (see line~\ref{alg:sort} of \Refine). 
The latter implies that the algorithm terminates.

\begin{proposition} \label{prp:type correct}
Let $\pp{\Sigma}{P}$ be a partition pair over a graph $(N,\to)$,
$\Refine(\Sigma,P)$ return $\Pi$ and
$\UpdateGPP(\Sigma,P,\Pi)$ return $Q$.
Then $\pp{\Pi}{Q}$ is a partition pair with $\pp{\Pi}{Q} \leq \pp{\Sigma}{P}$.
\end{proposition}

\begin{corollary}
For any graph $G$ and any partition pair $\pp{\Sigma}{P}$ over
$G$, the algorithm $\PA(G,\pp{\Sigma}{P})$ terminates.
\qed\end{corollary}

\noindent
The following lemmata state that \Refine and \UpdateGPP converge towards a
fixed point at least as fast as $\rho$ without ever diverging from the
path towards the GCPP solution.
In combination with the monotony of $\rho$ (\Prp{monotony}) this
implies the correctness of our algorithm.

\begin{lemma}
\label{lem:better}
Let $\pp{\Sigma}{P}$ be a partition pair over a graph $(N,\to)$,
$\Refine(\Sigma,P)$ return $\Pi$,
and $\UpdateGPP(\Sigma,P,\Pi)$ return $Q$.
Then $\pp{\Pi}{Q^+} \leq \rho(\pp{\Sigma}{P^+})$.
\end{lemma}

\begin{lemma}
\label{lem:soundness}
Let $\pp{\Sigma}{P}$ and $\pp{\Pi}{Q}$ be partition pairs over a graph $G=(N,\to)$,
\mbox{$\pp{\Xi}{\preceq}$} be the solution of the GCPP over $G$ and
$\pp{\Sigma}{P}$, and $\pp{\Xi}{\preceq} \leq \pp{\Pi}{Q}$.
Let $\Refine(\Pi,\!Q)$ return $\Pi'$ and
$\UpdateGPP(\Pi,\!Q,\!\Pi')$ return $Q'$.
Then $\pp{\Xi}{\!\preceq} \leq \pp{\Pi'\hspace{-2.7pt}}{\!Q'}$.
\end{lemma}

\begin{theorem}
\label{thm:PA computes GCPP}
Let $\pp{\Sigma}{P}$ be a partition pair over a graph $G = (N,\to)$.
Let $k$ be the value of variable $i$ upon termination of
$\PA(G,\pp{\Sigma}{P^+})$.
Then $\pp{\Sigma_k}{P_k}$ is the solution of the GCPP over $G$ and
$\pp{\Sigma}{P}$.
\end{theorem}


\subsection{No Fixed-Point Operator}
\label{sec:no operator}

We now show that there is no (functional) fixed-point operator that
captures the partition refinement performed by \Refine, \ie a function
$\pi$ such that for any partition pairs $\pp{\Sigma}{P}$ and
$\pp{\Pi}{Q}$ with $\pp{\Pi}{Q} = \pi(\pp{\Sigma}{P})$,
$\Refine(\Sigma,P)$ returns $\Pi$.
More specifically, we show that the partition returned by \Refine 
is not uniquely defined, but depends on the particular reverse topological
sorting that is chosen in line~\ref{alg:sort}.

\begin{figure}
\centering
\includegraphics{no-sigma}
\caption{Example on which \Refine does not return a uniquely defined
partition}
\label{fig:no-sigma}
\vspace{-2mm}
\end{figure}

\begin{example}
\label{exm:no-sigma}
Consider the graph $G=(N,\to)$ of \Fig{no-sigma} and the partition
pair $\pp{\Sigma}{P}$ with $\Sigma = \{ \alpha,\beta,\gamma,\delta,\varepsilon
\}$ as depicted and $P = \idty{\Sigma} \cup \{ (\beta,\delta), (\delta,\gamma)
\}$. Then $S = [\varepsilon,\gamma,\delta,\beta,\alpha]$ and $S' =
[\gamma,\delta,\beta,\varepsilon,\alpha]$ are reverse topological sortings of
$\Sigma$ with respect to $P$. Let $\Pi$ and $\Pi'$ be the partitions returned by
$\Refine(\Sigma,P)$ on sortings $S$ and $S'$
respectively. Then $\Pi = \{ \{a_0\}, \{a_1\}, \{a_2\} \}$ and $\Pi' = \{
\{a_0,a_1\}, \{a_2\} \}$. \qed
\end{example}

\noindent
Similar to the construction of \Cex{final}, this example can
be embedded in \Exm{non-transitive} to obtain an example with a
transitive relation for which the partition after the second refinement depends
on the chosen reverse topological sorting.

\section{Conclusions}
\label{sec:concl}

The correspondence between the simulation problem for finite, labelled graphs
and the generalised coarsest partition problem (GCPP) for unlabelled graphs can
be easily established.
We have shown that the $\sigma$ operator defined by Gentilini
\etal \cite{GPP:03} to solve the GCPP is flawed. In
particular, when applied to a partition pair, the result is not
necessarily another partition pair or even well-defined. Moreover, when
applied repeatedly to a transitive partition pair, convergence towards a
unique fixed point is not guaranteed.
Thereby we have shown that $\sigma$ is not suitable for solving the GCPP.
On the counterexample for the latter property, the algorithm of
\cite{GPP:03} that computes $\sigma$, produces a wrong result in which
two simulation-equivalent states are put in different equivalence
classes.

We have repaired this algorithm such that it correctly computes the
solution of the GCPP.
Apart from correcting the error that results from the flaws in the
$\sigma$ operator,
we also corrected a mistake that caused premature termination of
the algorithm on certain input.
Our algorithm benefits from the key ideas behind the original
partitioning algorithm and has the same space and time complexities.
We have proven its correctness using an auxiliary operator $\rho$ of
which we have shown that it solves the GCPP, though inefficiently.
Finally, we have shown that no operator can be defined that captures the
partition refinement performed in every iteration of our algorithm.

Another way to repair the algorithm of \cite{GPP:03} may be to
use the relation $P^+$ instead of $P$ in \RefineGPP.
The so obtained algorithm would converge to a fixed point slightly
slower than ours. More importantly, due to the cost of computing the
transitive closure in each iteration, the time complexity would
not match that of the original algorithm.

\paragraph{Acknowledgements.} We would like to thank Raffaella Gentilini and
Carla Piazza for answering some of our questions about their paper and providing
us with their implementation of the algorithm.
\newpage

\bibliographystyle{plain}
\begin{thebibliography}{10}

\bibitem{BIM:95}
{ B.~Bloom, S.~Istrail \& A.R. Meyer} (1995):
\newblock {\em Bisimulation can't be traced.}
\newblock {\sl Journal of the ACM} 42(1), pp. 232--268.

\bibitem{BP:95}
{ B.~Bloom \& R.~Paige} (1995):
\newblock {\em Transformational design and implementation of a new efficient solution to the ready simulation problem.}
\newblock {\sl Science of Computer Programming} 24(3), pp. 189--220.

\bibitem{BG:03}
{ D.~Bustan \& O.~Grumberg} (2003):
\newblock {\em Simulation-based minimization.}
\newblock {\sl ACM Transactions on Computational Logic} 4(2), pp. 181--206.

\bibitem{CVW+:90}
{ C.~Courcoubetis, M.Y. Vardi, P.~Wolper \& M.~Yannakakis} (1990):
\newblock {\em Memory efficient algorithms for the verification of temporal properties.}
\newblock In {\sl {\rm Proc. 2nd Workshop on} Computer-Aided Verification {\rm (CAV'90)}}, LNCS 531, Springer, pp. 233--242.

\bibitem{DGG:93}
{ D.~Dams, O.~Grumberg \& R.~Gerth} (1993):
\newblock {\em Generation of reduced models for checking fragments of {CTL}.}
\newblock In {\sl {\rm Proc. 5th Conference on} Computer Aided Verification {\rm ({CAV} '93)}}, LNCS 697, Springer, pp. 479--490.

\bibitem{EH:86}
{ E.A. Emerson \& J.Y. Halpern} (1986):
\newblock {\em ``{S}ometimes'' and ``{N}ot {N}ever'' revisited: On branching versus linear time temporal logic.}
\newblock {\sl Journal of the ACM} 33(1), pp. 151--178.

\bibitem{EP:05}
{ S.~Evangelista \& J.-F. Pradat-Peyre} (2005):
\newblock {\em Memory efficient state space storage in explicit software model checking.}
\newblock In {\sl {\rm Proc.~12th International {SPIN} Workshop on} Model Checking Software}, LNCS~3639, Springer, pp. 43--57.

\bibitem{GPP:03}
{ R.~Gentilini, C.~Piazza \& A.~Policriti} (2003):
\newblock {\em From bisimulation to simulation: Coarsest partition problems.}
\newblock {\sl Journal of Automated Reasoning} 31(1), pp. 73--103.

\bibitem{GPP:03-TR}
{ R.~Gentilini, C.~Piazza \& A.~Policriti} (2003):
\newblock {\em From bisimulation to simulation: Coarsest partition problems.}
\newblock RR 12-2003, Dep. of Computer Science, University of Udine, Italy.

\bibitem{GP08}
{ R.J.~van Glabbeek \& B.~Ploeger} (2008):
\newblock {\em Correcting a space-efficient simulation algorithm.}
\newblock CS-Report 08-06, Eindhoven University of Technology.

\bibitem{GrV92}
{ J.F. Groote \& F.W. Vaandrager} (1992):
\newblock {\em Structured operational semantics and bisimulation as a congruence.}
\newblock {\sl Information and Computation} 100(2), pp. 202--260.

\bibitem{HHK:95}
{ M.R. Henzinger, T.A. Henzinger \& P.W. Kopke} (1995):
\newblock {\em Computing simulations on finite and infinite graphs.}
\newblock In {\sl {\rm 36th Annual Symposium on} Foundations of Computer Science {\rm ({FOCS}'95)}}, IEEE Computer Society Press, pp. 453--462.

\bibitem{Hol:88}
{ G.J. Holzmann} (1988):
\newblock {\em An improved protocol reachability analysis technique.}
\newblock {\sl Software Practice and Experience} 18(2), pp. 137--161.

\bibitem{Koz:83}
{ D.~Kozen} (1983):
\newblock {\em Results on the propositional $\mu$-calculus.}
\newblock {\sl Theoretical Computer Science} 27, pp. 333--354.

\bibitem{KJ06}
{ A.~Kucera \& P.~Jancar} (2006):
\newblock {\em Equivalence-checking on infinite-state systems: Techniques and results.}
\newblock {\sl Theory and Practice of Logic Programming} 6(3), pp. 227--264.

\bibitem{LGS+:95}
{ C.~Loiseaux, S.~Graf, J.~Sifakis, A.~Bouajjani \& S.~Bensalem} (1995):
\newblock {\em Property preserving abstractions for the verification of concurrent systems.}
\newblock {\sl Formal Methods in System Design} 6(1), pp. 11--44.

\bibitem{Par:81}
{ D.M.R. Park} (1981):
\newblock {\em Concurrency and automata on infinite sequences.}
\newblock In {\sl {\rm Proc. 5th {GI}-Conference on} Theoretical Computer Science}, LNCS 104, Springer, pp. 167--183.

\bibitem{RT:07}
{ F.~Ranzato \& F.~Tapparo} (2007):
\newblock {\em A new efficient simulation equivalence algorithm.}
\newblock In {\sl {\rm Proc.~22nd Annual IEEE Symposium on} Logic in Computer Science {\rm (LICS'07)}}, IEEE Computer Society Press, pp. 171--180.

\bibitem{SM:73}
{ L.J. Stockmeyer \& A.R. Meyer} (1973):
\newblock {\em Word problems requiring exponential time.}
\newblock In {\sl {\rm Proc.~5th Annual ACM Symposium on} Theory of Computing {\rm (STOC'73)}}, ACM, pp. 1--9.

\bibitem{TC:01}
{ L.~Tan \& R.~Cleaveland} (2001):
\newblock {\em Simulation revisited.}
\newblock In {\sl {\rm Proc.~7th International Conference on} Tools and Algorithms for the Construction and Analysis of Systems {\rm ({TACAS}'01)}}, LNCS 2031, Springer, pp. 480--495.

\end{thebibliography}

\end{document}
