\documentstyle[twoside,12pt]{article} 
\pagestyle{myheadings}
 
% SIDE MARGINS:                   
\oddsidemargin  -4.4mm            % Left margin on odd-numbered pages.
\evensidemargin  3.6mm            % Left margin on even-numbered pages.
 
% VERTICAL SPACING:        
\topmargin      -4mm              % Nominal distance from top of page to top 
                                  % of box containing running head.
\headheight     13mm              % No running headline, and no
\headsep        24pt              % space between running headline and text.
 
% DIMENSION OF TEXT:
\textheight 230mm                 % Height of text part of page
\textwidth 160mm                  % Width of text part of page, i.e. of line

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%	     On American paper the right margin is 6 mm longer,		  %%%%
%%%%		whereas the bottom margin is 17.6 mm smaller.		  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newlength{\shiftside}			 \newlength{\shifttop}
\setlength{\shiftside}{3mm}		 \setlength{\shifttop}{-8.8mm}
\typeout{On what kind of paper are you going to print this?}
\typein[\paper]{Enter 1 for American paper or 0 for A4.}
\addtolength\oddsidemargin{\paper\shiftside}
\addtolength\evensidemargin{\paper\shiftside}
\addtolength\topmargin{\paper\shifttop}

\renewcommand{\abstract}[1]{\begin{list}{}
			{\rightmargin\leftmargin
			\listparindent 1.5em
			\parsep 0pt plus 1pt}
			\small\item #1\end{list}}
\newtheorem{adefinizione}{Definition}[section] 
\newtheorem{alemma}[adefinizione]{Lemma} 
\newtheorem{ateorema}[adefinizione]{Theorem} 
\newtheorem{acorollario}[adefinizione]{Corollary} 
\newtheorem{aproposizione}[adefinizione]{Proposition}
\newenvironment{definizione}{\begin{adefinizione}\rm}{ \end{adefinizione}} 
\newenvironment{lemma}{\begin{alemma}\rm}{\end{alemma}} 
\newenvironment{teorema}{\begin{ateorema}\rm}{\end{ateorema}} 
\newenvironment{corollario}{\begin{acorollario}\rm}{\end{acorollario}} 
\newenvironment{proposizione}{\begin{aproposizione}\rm}{\end{aproposizione}}
\newcommand{\dimo}{\par\medskip\noindent{\bf Proof. }} 
\newcommand{\deriv}[1]{{\mbox{${\:\stackrel{#1}{\rightarrow}\:}$}}} 
\newcommand{\nderiv}[1]{{\mbox{${\not\stackrel{#1}{\longrightarrow}}$} }}
\newcommand{\spazio}{\mbox{      }}
\newcommand{\bigfrac}[2]{\begin{array}{c}#1\\\hline#2\end{array}} 
\newcommand{\sem}[1]{\mbox{$[\! [#1]\! ]$}} 
\newcommand{\fine}{\hfill{$\rule{2mm}{2mm}$}}
\newcommand{\para}{\mbox{$\,\parallel\!\!_{S}\,$}} 
\newcommand{\sync}{\mbox{$\,\mid\!\!_{S}\,$}} 
\newcommand{\refin}[1]{\mbox{$[a\leadsto#1]$}} 
\newcommand{\rtom}{\mbox{$\gg$}} 
\newcommand{\merge}[1]{\mbox{${\stackrel{#1}{\bowtie}}$}} 
\newcommand{\lmerge}[1]{\mbox{${\stackrel{#1}{\lhd}}$}} 
\newcommand{\rmerge}[1]{\mbox{${\stackrel{#1}{\rhd}}$}} 
\newcommand{\nil}{\varepsilon}
\newcommand{\seq}{\cdot}
\newcommand{\name}[1]{\mbox{name($#1$)}}
\newcommand{\idx}[1]{\mbox{index($#1$)}}
\newcommand{\sg}[1]{\mbox{sg($#1$)}}
\newcommand{\incr}[1]{\mbox{inc($#1$)}}
\newcommand{\trans}[2]{f(#1,#2)}
\newcommand{\sk}{\mbox{skip}}
\newcommand{\M}{\mbox{\it Act}}

% ****************** Right Merge ***************************** 
\newcommand{\rp}
{\,\,     \setlength{\unitlength}{1ex} \begin{picture}(1,1.75)
\put(0.45,0){\line(-1,0){1}}
\put(0,0){\line(0,1){1.75}}
\put(0.45,0){\line(0,1){1.75}}
\end{picture}                             \,} 
%*************************************************************
\newcommand{\lpar}{\,\rp\!\!_{S}\,}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% vG's macro for open terms:
\newcommand{\opent}{\mbox{\sf T\hspace{-5.5pt}T}}  % Open terms
% Alternative for those who have font msbm10:
% \newfont{\open}{msbm10 scaled\magstep1}          % Openface letters
% \newcommand{\opent}{\mbox{\open T}}		   % Open terms as in Fokkink

%vG's macro for bisimulation:
\newcommand{\bisimm}[1]{ \;                        % bisimulation
        \raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}\,}
\newcommand{\bisim}{\bisimm{P'}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%Tex macro package by Vaughan Pratt for drawing character-sized objects%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcount\PLv\newcount\PLw\newcount\PLx\newcount\PLy\newdimen\PLyy\newdimen\PLX
\newbox\PLdot \setbox\PLdot\hbox{\tiny.} \def\scl{.08} % resettable scale
\def\PLot#1{\PLx`#1\advance\PLx-42\PLy\PLx\PLv\PLx\divide\PLy9\PLw\PLy\multiply
\PLw9\advance\PLx-\PLw\advance\PLx-4\PLy-\PLy\advance\PLy4\PLX=\the\PLx pt
\advance\PLyy\the\PLy pt\wd\PLdot=\scl\PLX\raise\scl\PLyy\copy\PLdot}
\def\draw#1{\ifx#1\end\let\next=\relax\else\PLot#1\let\next=\draw\fi\next}
%%%%%%%%%%%%%%%%%%%Polish a by Rob van Glabbeek%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\pa{\mbox{a\hspace{-2pt}\raisebox{-.7pt}%     \pa   Polish a
        {\draw Wabcdefgh_VVM\end}\hspace{1pt}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Axiomatising ST-Bisimulation Equivalence}

\author{
Nadia Busi$^{a}$ \thanks{The first and third authors have been supported by
CNR, MURST and Esprit project 8130 LOMAPS.}
\and Rob van Glabbeek$^{b}$ \thanks{The second author has been
funded by ONR under grant number N00014-92-J-1974.}
\and Roberto Gorrieri$^{c}$ $^{*}$
\date{\small
$^{a}$Dipartimento di Matematica, Universit\`{a}
di Siena \\
Via del Capitano, 15, I-53100 Siena, Italy \\
e-mail: busi@cs.unibo.it \\
\vspace{.2cm}
$^{b}$Computer Science Department, Stanford University\\
Stanford, CA 94305, USA\\ e-mail: rvg@cs.stanford.edu \\
\vspace{.2cm}
$^{c}$Dipartimento di Matematica, Universit\`{a}
di Bologna \\
Piazza di Porta S. Donato 5, I-40127 Bologna, Italy \\
e-mail: gorrieri@cs.unibo.it \\
}}



\begin{document}
\bibliographystyle{plain}
\maketitle
\abstract{
A simple ST operational semantics for a process algebra is provided, by 
defining a set of operational rules in Plotkin's style. 
This algebra comprises TCSP parallel composition, ACP sequential composition 
and a refinement operator, which is used for replacing an action with an 
entire process, thus permitting hierarchical specification of systems.
We prove that ST-bisimulation equivalence is a congruence, resorting 
to standard techniques on rule formats. Moreover, we provide a set of 
axioms that is sound and complete with respect to ST-bisimulation.
The intriguing case of the forgetful refinement (i.e.\ when an action is
refined into the properly terminated process) is dealt with in a new,
improved manner.
}

\section{Introduction}
Among the non-interleaving equivalences, one of the most relevant is
ST-bisimulation equivalence, originally proposed in \cite{GlaVaan}
over Petri Nets, from which it takes the name (S and T are the initials of
the German words for Place and Transition).
This semantics drops the assumption that actions are {\em atomic} 
activities, hence, unobservable in the middle of their evolution.
This is implemented by splitting every action in two distinct phases: the
{\em beginning} and the {\em ending} which, instead, are considered atomic.
Additionally, in order to prevent possible confusion in the presence of 
autoconcurrent actions, every ending phase is unambiguously related to 
its own beginning phase through some supplementary information.
In the version of ST semantics we exploit, a causal link connects every ending
phase to the corresponding beginning phase \cite{GorLan}. This is achieved by 
equipping each ending phase of an action with a ``relative pointer'' to 
indicate the number of phases which have occurred from the beginning of 
that action.

ST semantics expresses an elementary form of duration,
as many action phases can be executed in between a beginning and its end.
Moreover, ST semantics is {\em the} semantics for the operation of {\em action
refinement}. This operation substitutes the execution of a process for
an action, thereby
introducing the possibility of relating descriptions of the same system 
at different levels of detail.
It has been extensively studied in the semantic domain
of event structures \cite{GlGo2,DaDe}, where an event is replaced by 
a whole structure.
ST-bisimulation equivalence has been proved to be a congruence for this 
operation in \cite{Glabbeek} and the coarsest congruence contained in 
interleaving bisimulation in \cite{Vog}.   

In this paper, we define an ST operational semantics in SOS style \cite{Plotkin}
for a process algebra equipped with the TCSP parallel composition 
operator, the ACP sequential composition operator and the refinement one.
The transition system we define is labelled on action phases; hence, two 
agents are ST-bisimulation equivalent if their corresponding states are
strongly bisimilar.
The transition system specification (TSS, for short) we propose fits the 
{\em tyft} format of \cite{GroVaan}. Therefore, we can exploit a nice result 
of that paper, namely that strong bisimulation is a congruence.
Then, we provide a sound and complete axiomatization for
ST-bisimulation: to obtain this, we conservatively extend the TSS by adding
some auxiliary operators, following the lines of the algorithm defined in 
\cite{Aceto}.

We claim that the operational description we provide for the operator of 
action refinement is in perfect agreement (apart from the way the empty
refinement is dealt with) with the denotational one in terms of flow event 
structures described in \cite{GlGo2}. Our claim is based on 
a similar proof, provided in \cite{Busi}, where a slightly different 
language and a slightly different version of ST semantics are considered.
We argue that our way of dealing with the empty refinement, which can
be useful in applications \cite{GlGo2}, is more
satisfactory than the one of \cite{GlGo1}, and that event structures
are not expressive enough to model this type of refinement.

\section{Labelled Transition Systems}
We recall the basic, relevant notions about transition system specification 
from \cite{GroVaan}, incorporating a recent improvement reported
in \cite{Fok,vGamast}.

Let $V$ be a denumerable set of variables; $x$, $y$, $z$ are typical 
elements of $V$.
A single sorted signature $\Sigma$ is a pair $(F, \sharp)$, where $F$ is a 
set of function names disjoint with $V$, and $\sharp:F\rightarrow\omega$ 
is a rank function which gives the arity of a function name.
With $\opent(\Sigma)$ and $T(\Sigma)$ we denote the set of open and 
closed terms respectively over signature $\Sigma$. $V(t)\subseteq V$ 
denotes the set of variables in a term $t$. A substitution $\sigma$ is a 
mapping $V\rightarrow \opent(\Sigma)$, extended homomorphically to 
terms. 
%The composition of substitutions $\sigma\circ\rho$ is defined by: 
%$\sigma\circ\rho(x) = \sigma(\rho(x))$ for $x\in V$.

\begin{definizione}
A {\em transition system specification} (TSS) is a triple $(\Sigma, A, R)$ 
with $\Sigma$ a signature, $A$ a set of labels and $R$ a set of rules of the 
form
$\bigfrac{\{t_{i}\deriv{a_{i}}t'_{i}\mid i\in I\}}{t\deriv{a}t'}$
with $I$ an index set, $t_{i}, t'_{i}, t, t'\in 
\opent(\Sigma)$, $a_{i}, a\in A$ for $i\in I$. 
\fine
\end{definizione}
If $r$ is a rule satisfying the above format, then the elements of 
$\{t_{i}\deriv{a_{i}}t'_{i}\mid i\in I\}$ are called the {\em premises} 
of $r$ and $t\deriv{a}t'$ is called the {\em conclusion} of $r$.
A rule of the form $\frac{\emptyset} {t\deriv{a}t'}$ is called an 
axiom, which, if no confusion can arise, is also written as $t\deriv{a}t'$. 
An expression of the form $t\deriv{a}t'$ with $a\in A$ and 
$t,t'\in \opent(\Sigma)$ is called a transition (labelled with $a$).
The letters $\phi$, $\psi$, $\chi$ are used to range over transitions.
The notions `substitution', `$V(\cdot)$' and `closed' extend to
transitions and rules as expected.

\begin{definizione}
Let $P = (\Sigma, A, R)$ be a TSS. A {\em proof} of a transition $\psi$ 
from $P$ is a well-founded, upwardly branching tree of which the nodes are 
labelled by transitions $t\deriv{a}t'$ with $t, t'\in \opent(\Sigma)$ and 
$a\in A$, such that: the root is labelled with $\psi$, and if $\chi$ is 
the label of a node $q$ and $\{\chi_{i}\mid i\in I\}$ is the set of 
labels of the nodes directly above $q$, then there is a rule 
$\bigfrac{\{\phi_{i}\mid i\in I\}}{\phi}$ in $R$ and a substitution 
$\sigma$ such that $\chi = \sigma(\phi)$ and $\chi_{i} = \sigma(\phi_{i})$ 
for $i\in I$.
If there exists a proof of $\psi$ from $P$, then  $\psi$ 
is {\em provable} from $P$ (notation $P\vdash\psi$).
\fine\end{definizione}

\begin{definizione}
A {\em labelled transition system (LTS)} is a structure $(S, A, 
\rightarrow)$ where $S$ is a set of {\em states}, $A$ an {\em alphabet}, and 
$\rightarrow\subseteq S\times A \times S$ a {\em transition relation}.
We write $t\deriv{a}t'$ to indicate that $(t,a,t')\in\rightarrow$.
\fine\end{definizione}

\begin{definizione}
Let ${\cal A} = (S, A, \rightarrow)$ be an LTS. A relation $R\subseteq 
S\times S$ is a {\em (strong) bisimulation} if it 
satisfies:
\begin{itemize}\vspace{-2ex}
\item
if $(s,t)\in R$ and $s\deriv{a}s'$, then there exists $t'\in S$ 
with $t\deriv{a}t'$ and $(s',t')\in R$;\vspace{-2ex}
\item
if $(s,t)\in R$ and $t\deriv{a}t'$, then there exists $s'\in 
S$ with $s\deriv{a}s'$ and $(s',t')\in R$.\vspace{-2ex}
\end{itemize}
Two states $s,t\in S$ are {bisimilar} in ${\cal A}$, notation ${\cal A}: 
s \bisimm{} t$, 
if there exists a  bisimulation containing the pair $(s, t)$. Note that 
bisimilarity is an equivalence relation.
\fine
\end{definizione}

\begin{definizione}
Let $P = (\Sigma, A, R)$ be a TSS. The transition system $TS(P)$ 
specified by $P$ is the triple
$TS(P) = (T(\Sigma), A, \rightarrow_{P})$
where the relation $\rightarrow_{P}$ is defined by: $t\deriv{a}_{P}\,t'$ iff 
$P\vdash t\deriv{a}t'$.

We say that two terms $t, t'\in T(\Sigma)$ are ($P$-)bisimilar, notation 
$t\bisimm{P} \, t'$, if $TS(P): t\bisimm{} t'$.
We write $t\bisimm{} t'$ if it is clear from the context what $P$ is.
\fine\end{definizione}

TSSs do not always generate LTSs for which bisimulation is a 
congruence, but they do if their rules satisfy the format below.

\begin{definizione}
Let $\Sigma = (F,\sharp)$ be a signature and let $P = (\Sigma, A, R)$ be a TSS.
 A rule in $R$ is in {\em tyft format} if it has the form
$\bigfrac{\{t_{i}\deriv{a_{i}}y_{i}\mid i\in I\}}{f(x_{1},
\ldots,x_{\sharp(f)})\deriv{a} t}$
with $f$ a function name from $F$, $x_{i}$ $(1\leq 
i\leq \sharp(f))$ and $y_{i}$ $(i\in I)$ are all different variables,
$a_{i}, a\in A$ and $t_{i}, t\in \opent(\Sigma)$ for $i\in I$.
$P$ is in {\em tyft} format if all the rules in $R$ are in {\em tyft} format. 
\fine
\end{definizione}

\begin{teorema}
Let $\Sigma = (F,\sharp)$ be a signature and $P = (\Sigma,A, R)$ a  TSS. 
If $P$ is in {\em tyft} format then strong 
bisimulation is a congruence for all function names in $F$. 
\fine
\end{teorema}
\pagebreak
\begin{definizione}
Let $P = (\Sigma, A, R)$ be a TSS and let $r$ be a rule in $R$.
The {\em bound} variables of $r$ are recursively defined as the ones that
occur in the left hand side of the conclusion or in the right hand
side of a premise $t\deriv{a}t'$, where $t$ contains bound variables only.
A rule $r$ is {\em pure} if all variables that occur in it are bound. 
The TSS $P$ is called pure if all rules in $R$ are pure.
\fine
\end{definizione}

Given two TSSs $P_{0}$ and $P_{1}$ we use $P_{0}\oplus P_{1}$ to denote 
their componentwise union, which is only defined if function names that 
occur in both the signatures of $P_{0}$ and $P_{1}$ are given the same 
arity. If $P_{0}$ and $P_{1}$ are in {\em tyft} format and 
some other conditions are satisfied, we have that the outgoing transitions 
in 
the transition system defined by $P_{0}$ of terms in the signature of 
$P_{0}$ are the same as the outgoing transitions of these terms in the 
transition system defined by $P_{0}\oplus P_{1}$. 

\begin{definizione}
Let $P_{i} = (\Sigma_{i}, A_{i}, R_{i})$ $(i=0,1)$ be two TSSs with $P = 
P_{0}\oplus P_{1}$ defined. Let $P = (\Sigma, A, R)$. We say that $P$ is a 
{\em conservative extension} of $P_{0}$ and that $P_{1}$ can be added 
conservatively to $P_{0}$ if for all $t\in 
T(\Sigma_{0})$, $a\in A$ and $t'\in 
T(\Sigma)$: 

\vspace{.3cm}
\noindent \hfill
$P\vdash t\deriv{a}t' \; \Longleftrightarrow \; P_{0}\vdash t\deriv{a}t'$
\fine
\end{definizione}
Note that if $P$ is a conservative extension of $P_{0}$, $P$ is also a 
conservative extension up to bisimulation, i.e.\ for $t,t'\in 
T(\Sigma_{0})$: 
$t\bisimm{P} \, t' \; \Longleftrightarrow \; t\bisimm{P_{0}} \, t'$.

\begin{teorema}
Let $P_{0} = (\Sigma_{0}, A_{0}, R_{0})$ be a TSS in pure {\em tyft} format and 
let $P_{1} = (\Sigma_{1}, A_{1}, R_{1})$ be a TSS in {\em tyft} format such 
that no rule of $R_{1}$ contains a function name from $\Sigma_{0}$ in the 
source of its conclusion. Let $P = P_{0}\oplus P_{1}$ be defined. Then $P_{1}$
can be added conservatively to $P_{0}$.
\fine
\end{teorema}

\section{The Language}
Let $\M$ be a countable set of actions;
$a, b, c, d$ range over $\M$ and $S$ over the subsets of $\M$.
The process terms are generated by the following syntax:

\[t ::= \nil\mid\delta\mid a\mid t\seq t'\mid t+t'\mid t\para t'\mid 
t\refin{t'}\]

Intuitively, $\nil$ is the successfully terminated process, 
whereas $\delta$ is the deadlocked process. The operators $\seq$ and $+$ 
are the ACP sequential and alternative composition, respectively.
With $\para$ we mean the TCSP parallel composition, where synchronisation 
over actions in $S$ is required\footnote{One could consider also more
general parallel operators, like the ACP one. Our work can be easily
adapted to ACP and similar languages.}. When set $S$ is empty (i.e.\ when
no synchronization is allowed), we usually omit the subscript $S$ in 
$\para$. Finally $\refin{}$ is the refinement operator as defined
e.g.\ in \cite{DegGor}.

Recursion can be added and modelled in our operational approach in the
usual way (see \cite{GorLan2} for a possible operational ST semantics 
for recursion).
However, as our main concern is the axiomatisation, we prefer to
restrict our attention to the finite calculus above.

\section{Operational Semantics}\label{operational}
To define the operational semantics, we need a more generous 
signature to represent the states.
Let $k$ range over integers.
Let $\Sigma = (F,\sharp)$, where 
\[\begin{array}{rcl}
F & = & \{\nil, \delta, +, \seq\} \cup \{a\mid a\in \M\} \cup 
\{a^{1} \mid a\in \M\} \cup \{[k]\mid k\neq 0\}\\
& &  \cup \{\para\mid S\subseteq\M\} \cup 
\{\refin{}\mid a\in \M\}\cup \{\merge{k}\mid k>0\}\\
\multicolumn{3}{l}{\sharp(\nil) = \sharp(\delta) = \sharp(a) =
	\sharp(a^{1}) = 0} \\
\multicolumn{3}{l}{\sharp([k]) = 1}  \\
\multicolumn{3}{l}{\sharp(+) = \sharp(\seq) = \sharp(\para) =
	\sharp(\refin{}) = \sharp(\merge{k}) = 2}
\end{array}\]
As any action is split in two phases, we need a unary operator to
represent the state of its intermediate execution.
An action $a$ performs its beginning (denoted, with abuse of notation,
$a$ as well), reaching $a^1$. This performs the ending of the action
$a$, where the superscript $1$ states that this ending refers to the 
just performed transition. In general, the
causal pointer from an ending to its beginning is implemented as a
superscript number $k$ stating that its beginning has been executed $k$
transitions before.
The {\em delay} operator $[k]$ suitably updates the pointers. It will be
introduced in a context of parallel composition and refinement.
The {\em merge} operator $\merge{k}$ is used when merging the executions
of a refined agent and the activated refining agent. Intuitively,
it is a restricted form of parallel composition, as illustrated 
in Section 6.

Let $\M^{\omega} = \{\mu^{k}\mid\mu\in \M\wedge k>0 \}$ be the
set of {\em endings}; 
let $\M_{ST} = \M\cup \M^{\omega}$ be the set of {\em phases},
where a label in $\M$ is called a {\em beginning}; 
$\eta$ ranges over $\M_{ST}$ 
and $\theta$ ranges over $\M_{ST}\cup\{\surd\}$, where action $\surd$
(sometimes called ``tick'') denotes clean termination.

Let $P = (\Sigma, A, R)$ be the TSS where $A = \M_{ST}\cup\{\surd\}$ 
and $R$ is the set of rules listed in Table \ref{rules}  
 commented upon below.
The auxiliary functions used in the rules are defined in
Table~\ref{func}.
\begin{table}[htb]
{\renewcommand{\arraystretch}{1.4}
\[\begin{array}{|l|}
\hline
\begin{array}{@{}l|l|l@{}}
\name{a} = a & \idx{a} = 0 & \trans{a}{k} = a\\
\name{a^{k}} = a & \idx{a^{k}} = k & \trans{a^{h}}{k} = \left\{
\begin{array}{@{}ll@{}}
a^{h+sg(k)} & \mbox{ if }h\geq |k| \\
a^{h} & \mbox{ otherwise }
\end{array}\right.\\
\name{\surd} = \surd~~ & & \trans{\surd}{k} = \surd 
\end{array}\\
\hline
\begin{array}{@{}l|l@{}}
\sg{k} = \left\{
\begin{array}{ll}
1 & \mbox{ if }k>0 \\
- 1 & \mbox{ if }k<0 
\end{array}\right.\hspace{1.1cm} & 
\incr{k} = k + sg(k) 
\end{array}\\
\hline
\end{array}\]}\vspace{-1ex}
\caption{Auxiliary functions on action phases} \label{func}
\end{table}
The functions name and index are intuitively clear. They extract from
a label the name of the action and the associated index, respectively.
Function $\sg{k}$ returns the sign of the integer $k$, while
$\incr{k}$ increases the absolute value of $k$. Finally, function $f$
updates the index of the label to which it is applied.\footnote{From
the definition of $f$ we cannot exclude to obtain action endings with
a zero or negative index.  However, we have that terms reachable from
elements of the language contain positive indexes only.}

\begin{table}[hp]
{\renewcommand{\arraystretch}{1.4}
\[\begin{array}{|c|}
\hline
\begin{array}{lcllcl}
(ACT1) & a\deriv{a}a^{1} &
(ACT2) & a^{1}\deriv{a^{1}}\nil &\\

(TICK) & \nil\deriv{\surd}\delta &
(DELAY) & \bigfrac{x\deriv{\theta}x'}
{[k]x\deriv{\trans{\theta}{k}}[\incr{k}]x'}   & \\

(SEQ1) & \bigfrac{x\deriv{\eta}x'}{x\seq y\deriv{\eta}x'\seq
y}\hspace{1cm} &
(SEQ2) & \bigfrac{x\deriv{\surd}x' \spazio y\deriv{\theta}y'}{x\seq
y\deriv{\theta} y'} &\\

(ALT1) & \bigfrac{x \deriv{\theta} x'} {x + y \deriv{\theta}
x'}   &
(ALT2) & \bigfrac{y \deriv{\theta} y'} {x + y \deriv{\theta}
y'}   &
\end{array} \\
\begin{array}{lcl}
(PAR1) & \bigfrac{x \deriv{\eta} x'} {x \para y \deriv{\eta} x'\para
[1]y}   &
\name{\eta}\not\in S \\
(PAR2) & \bigfrac{y \deriv{\eta} y'} {x \para y \deriv{\eta} [1]x\para
y'}   &
\name{\eta}\not\in S \\
(PAR3) & \bigfrac{x \deriv{\theta} x'\spazio y \deriv{\theta} y'}  {x
\para y \deriv{\theta} x'\para y'}   &  \name{\theta}\in
S\cup\{\surd\}
\end{array}\\
\hline
\begin{array}{lcl}
(REF1) & \bigfrac{x \deriv{\theta} x'} {x  \refin{y} \deriv{\theta}
x'\refin{y}}   & \theta \neq a\\

(REF2) & \bigfrac{x \deriv{a} x'\spazio y \deriv{\eta} y'}
{x\refin{y}\deriv{\eta} x'\refin{y}\merge{1} y'} &\\

(REF3) & \bigfrac{x\deriv{a}x'\spazio x'\deriv{a^{1}}x''\spazio
[-1][-1](x''\refin{y})\deriv{\theta}x''' \spazio
y\deriv{\surd}y'}{x\refin{y}\deriv{\theta}x'''}\hspace{-40.89372pt} &
\\

(MERGE1) & \bigfrac{x \deriv{\eta} x'} {x\merge{k} y
\deriv{\eta} x'\merge{k+1}[1]y} & \idx{\eta}\neq k\\

(MERGE2) & \bigfrac{y \deriv{\eta} y'} {x\merge{k} y  \deriv{\eta}
[1]x\merge{k+1} y'}  &\\

(MERGE3)  & \bigfrac{x \deriv{a^{k}} x'\spazio [-1]x'
\deriv{\theta} x''\spazio   y\deriv{\surd}y'} {x\merge{k}y
\deriv{\theta} x''} &
\end{array} \\
\hline
\end{array}\]
}
\caption{Rules for basic operators}  \protect\label{rules}
\end{table}

Axiom $({\it ACT}1)$ represents the starting of an action, while $({\it
ACT}2)$
accounts for the execution of the ending. $({\it TICK})$ is the rule for
the term $\nil$, which performs $\surd$ and terminates.
The rules for sequential and alternative composition are
standard (see e.g.\ \cite{GroVaan}).
The rules for the TCSP-like parallel composition are almost standard.
According to $({\it PAR}1)$, the asynchronous execution of a phase
from the left subagent can be performed if this phase is part of an
action not in the synchronisation set $S$; note, however, that the
right subagent is
delayed (i.e.\ the delay $[1]$ operator is applied to it), because
the pointers of all ending phases it will execute that point back to
before the current state must be incremented by one, as they refer to
transitions which are one step further back.
Rule $({\it PAR}3)$ needs no delay as
both subagents take part in the synchronisation; note that the
termination signal $\surd$ can only be performed synchronously by the
two subagents. The rule for the delay operator might appear a bit
clumsy, as it works for integers $k$ which can also be negative. A
negative delay is needed when skipping some transitions, as now
the pointers are to be decreased. The operator $[k]$ increments
pointers by 1 if $k$ is positive; it decrements by 1 if $k$ is
negative. Thus decrementing by $2$ needs to be expressed as
$[-1][-1]$; not as $[-2]$. The value of $|k|$ specifies {\em which}
pointers need to be adapted; namely all pointers that point back at
least $k$ phases before the current state.

More interesting are the rules for refinement. Rule $(REF1)$ accounts
for the case when the performed phase belongs to an action which is not
to be refined. On the contrary, $(REF2)$ states that whenever the agent
under refinement, $x$, starts the execution of the action to be refined,
$a$, then $x[a\leadsto y]$ performs the first, non tick, phase the
refining agent $y$ is able to do; the reached state is the merge of the
two subagents, where the parameter $1$ of the merge operator
remembers the index of the ending phase of the refined action.
Particular care should be devoted to rule $(REF3)$ which deals with the
case when $y$ can properly terminate, as in the so-called {\em empty}
refinement $\refin{\nil}$ (see Section 6 for a longer discussion). If
$x$ is ready to
start the execution of $a$, then it will complete it, becoming $x''$,
and then we will take the first transition the refinement of $x''$ is
able to do, remembering to update the pointers, as we have skipped two
transitions (the one for $a$ and the other for $a^1$).
The three rules for the merge operator state that the refined agent
$x$ can always perform a phase asynchronously, provided that this phase
is not the ending of the action which has been refined (see rule
$({\it MERGE}1)$ with its side condition); that the refining agent can
proceed
without any constraint (see rule $({\it MERGE}2)$); and that the merged
execution of the two ends when $x$ is ready to perform the ending of
the refined action and $y$ can terminate properly.

It is worth-while observing that the transitions are labelled
with parameters that range over actions and natural numbers,
and not directly with actions, as required by the {\em tyft} format;
so, every rule in our TSS is a rule schema corresponding to an
infinite set of rules.

\begin{proposizione}
$P$ is pure and in {\em tyft} format.
Strong bisimulation is a congruence for all function names in $F$.
\fine
\end{proposizione}

\section{Axiomatisation}\label{axiomatisation}
In this section we introduce a set of auxiliary operators; then we define 
an axiomatisation and prove its soundness and completeness with respect 
to bisimulation.

\subsection{Auxiliary Operators}
First we introduce a set of auxiliary operators, that are necessary to 
obtain the axiomatisation.
Let $\Sigma' = (F', \sharp')$, where:
\[\begin{array}{rcl}
F'& =& F \cup \{a^{+}\mid a\in \M\}\cup \{a^{k}\mid a\in \M\wedge 
k\geq 2\}\\
&&\cup \{\lpar, \sync\mid S\subseteq\M\} \cup 
\{\lmerge{k}, \rmerge{k}\mid k>0\}\cup \{\rtom\} \\
\multicolumn{3}{l}{\mbox{if $f\in F$ then $\sharp'(f) = \sharp(f)$}} \\
\multicolumn{3}{l}{\sharp'(a^{+}) = \sharp'(a^{k}) = 0} \\
\multicolumn{3}{l}{\sharp'(\lpar) = \sharp'(\sync) =
\sharp'(\lmerge{k}) = \sharp'(\rmerge{k}) = \sharp'(\rtom) = 2}
\end{array}\]
In this setting, it is essential to introduce a syntactical 
distinction between actions and beginnings. To this aim, we introduce
the auxiliary beginnings of the form $a^+$, which can perform the
beginning $a$ and then terminate successfully. The operators of the 
form $a^k$, for any $k \geq 2$, are needed as
we  have labels of this kind in the operational rules of the previous
section. The left-parallel $\lpar$ and the synchronisation-parallel
$\sync$ are useful for the axiomatisation of the parallel operator
$\para$. They play the same r\^ole as the left-merge and communication
merge of ACP \cite{BK-ACP}. However, whereas the left-merge of \cite{BK-ACP}
insists that the first {\em action} in a parallel composition comes from the
argument on the left, our $\lpar$ only insists that the first {\em
phase}
comes from the argument on the left. As far as the mnemonics concerns,
$\lpar$ points to the {\em left}, whereas the left merge is shaped
like an L\@; there is no need for a right-merge here.
The auxiliary operators $\lmerge{k}$ and $\rmerge{k}$ play a similar
r\^ole in the axiomatisation of the $\merge{k}$. Due to the
asymmetry between the refined and the refining process both are needed
here. $\rtom$ is used to axiomatise the refinement operator.

Let $P' = (\Sigma', A, R')$ a TSS, 
where $R'$ is the set of rules listed in 
Tables \ref{rules} and \ref{rulesAux}.
\begin{table}[htb]
{\renewcommand{\arraystretch}{1.4}
$$\begin{array}{|c|}
  \hline
\begin{array}{lclc}
(ACT3) & a^{+}  \deriv{a} \nil  & 
(ACT4) & a^{k}  \deriv{a^{k}} \nil \hspace{2cm} k>1  \\

(RTOM1) & \bigfrac{y \deriv{\eta} y'} {x\rtom y  \deriv{\eta}
x\merge{1} y'}  &
(RTOM2)  & \bigfrac{x \deriv{a^{1}} x'\spazio [-1][-1]x'
\deriv{\theta} x''\spazio   y\deriv{\surd}y'} {x\rtom y
\deriv{\theta} x''}  \\

(RME1) & \bigfrac{y \deriv{\eta} y'} {x\rmerge{k} y  \deriv{\eta}
[1]x\merge{k+1} y'}  &
(RME2)  & \bigfrac{x \deriv{a^{k}} x'\spazio [-1]x'
\deriv{\theta} x''\spazio   y\deriv{\surd}y'} {x\rmerge{k}y
\deriv{\theta} x''}  \\
\end{array}
\\
\begin{array}{lcl}
(LME) & \bigfrac{x \deriv{\eta} x'} {x\lmerge{k} y
\deriv{\eta} x'\merge{k+1}[1]y} & \idx{\eta}\neq k\\

(LPAR) & \bigfrac{x \deriv{\eta} x'} {x \lpar y \deriv{\eta} 
x'\para [1]y}   & \name{\eta}\not\in S \\

(SYNC) & \bigfrac{x \deriv{\theta} x'\spazio y \deriv{\theta} y'} 
{x \sync y \deriv{\theta} x'\para y'}   & \name{\theta}\in 
S\cup\{\surd\} \\
\end{array}\\
\hline
\end{array}$$\vspace{-3ex}
\caption{Rules for auxiliary operators}\label{rulesAux}
}
\end{table}
The only rules we comment on are those for
$\rtom$. The first rule states that the next transition, if not tick,
must be taken from the right subagent; the reached state is the merge
of the two, with pointer one. The second rule, instead, covers the case
when $y$ can terminate. This rule is similar to $(REF3)$. In this
way $x\rtom y$ behaves exactly like $x\refin{y}$ when the latter is
about to start refining an action $a$.

\begin{proposizione}
$P'$ is in {\em tyft} format.
Strong bisimulation is a congruence for all function names in $F'$.
$P'$ is a conservative extension of $P$.
\fine
\end{proposizione}

The binary operators are left associative and binding priority 
is defined in decreasing order as follows: 
$\seq > [k] > \refin{} > \para,\lpar,\sync,\merge{k},\lmerge{k},\rmerge{k},
\rtom > +$.

\subsection{Axiomatisation}
Let $\M^{+}=\{\mu^{+}\mid \mu\in \M\}$.
Let $\lambda$ range over $\M^{+}\cup \M^{\omega}\cup\{\delta\}$.
We extend the auxiliary functions introduced in the previous section in the 
following way:
\[\begin{array}{|l|l|l|}
\hline
\name{a^{+}} = a 	&\idx{a^{+}} = 0  & \trans{a^{+}}{k} = a^{+} \\
\name{\delta} = \delta	&\idx{\delta} = 0 & \trans{\delta}{k} = \delta \\
\hline
\end{array}\]

\begin{table}[hp]
{\renewcommand{\arraystretch}{1.4}
$$\begin{array}{@{}|l|@{}}
  \hline
\begin{array}{lrcl|lrcl}
(alt1) & x + y & = & y + x & 
(seq1) & (x y) z & = & x (y z)\\
(alt2) & (x + y) + z & = & x + (y + z)\hspace{1.5cm} & 
(seq2) & (x+y) z & = & x z + y z  \\
(alt3) & x + x & = & x & 
(seq3) & \delta x & = & \delta  \\
(alt4) & x + \delta & = & x &
(seq4) & \nil x & = & x \\
&&&&
(seq5) & x \nil & = & x  
\end{array} \\
\hline
\begin{array}{lrcll}
(act) & a & = & a^{+} a^{1} & 
\end{array}\\
\hline
\begin{array}{lrcll}
(par) & x\para y & = & x\lpar y + y\lpar x + x\sync y \hspace{-19.19388pt} & 
\end{array}\\
\hline
\begin{array}{lrcll}
(lpar1) & \lambda x\lpar y & = & \lambda(x\para [1]y) & \mbox{  if  
}\name{\lambda}\not\in S \\
(lpar2)  & \lambda x\lpar y & = & \delta & \mbox{  if  
}\name{\lambda}\in S \\
(lpar3) & \nil\lpar x & = & \delta & \\
(lpar4) & (x+y)\lpar z & = & x\lpar z + y\lpar z & 
\end{array}\\
\hline
\begin{array}{lrcll}
(sync1) & \lambda x\sync \lambda y & = & \lambda(x\para y) & 
\mbox{ if }\name{\lambda}\in S \\
(sync2) & \lambda x\sync \lambda' y & = & \delta & 
\mbox{ if }\name{\lambda}\not\in S \vee \lambda\neq\lambda'\\
(sync3) & \nil \sync \lambda y& = & \delta & \\
(sync4) & \nil\sync \nil & = & \nil & \\
(sync5) & (x+y)\sync z & = & x\sync z + y\sync z & \\
(sync6) & x\sync y & = & y\sync x & 
\end{array}\\
\hline
\begin{array}{lrcll}
(delay1) & [k](\lambda x) & = & \trans{\lambda}{k}([\incr{k}]x) & \\
(delay2) & [k]\nil & = & \nil & \\
(delay3) & [k](x+y) & = & [k]x + [k]y & \\
\end{array}\\
\hline
\end{array}$$}
\caption{Axioms for all the operators (except refinement)} \label{axiom1}
\end{table}

Let ${\cal T}$ be the axiom set in Tables \ref{axiom1} and 
\ref{axiom2}.
Our axioms for the interaction between $\parallel$ and the empty
process is a mild variation on the treatment of \cite{Vrancken}.
While the axioms for the alternative, sequential and parallel
composition are almost standard, the other axioms are not so usual.
First, observe axiom $({\it act})$. It states that any action $a$ should
be
intended as composed of the sequence of its beginning and its ending
(with pointer $1$). The three axioms for the delay operator reflect
clearly its operational definition. More intriguing is the case of
refinement; in particular, $({\it ref}2)$ shows that the refinement can
start
by dropping the beginning of the refined action and giving priority
to the refining subagent $y$. Note that no action has been extracted
from the term, so, no phase has been ``executed''.
This is done by the first application of axiom $({\it rtom}1)$, if $y$
is not
terminated, or of $({\it rtom}2)$, if $y$ terminates properly.
The axioms for $\lmerge{k}$ and $\rmerge{k}$ are intuitively clear, as
$({\it lmerge}1)$ corresponds to the operational rule $({\it
MERGE}1)$, $({\it rmerge}1)$
to $({\it MERGE}2)$ and $({\it rmerge}2)$ to $({\it MERGE}3)$.
Finally, note that the axioms for $\rtom$ and $\rmerge{k}$ are
very similar: they differ only in the application of the delay operator
in the first two axioms.

\begin{table}[hp]
{\renewcommand{\arraystretch}{1.4}
$$\begin{array}{|lrcll|}
\hline
({\it ref}1) & (\lambda x)\refin{y} & = & \lambda (x\refin{y}) & \mbox{  if  
}\lambda\not=a^{+} \\
({\it ref}2) & (a^{+} x)\refin{y} & = & (x\refin{y})\rtom y & \\
({\it ref}3) & \nil\refin{y} & = & \nil & \\
({\it ref}4) & (x+y)\refin{z} & = & x\refin{z} + y\refin{z} & \\
\hline
(rtom1) & x\rtom\lambda y & = & \lambda (x\merge{1}y) & \\
(rtom2) & a^{1} x\rtom\nil & = & [-1][-1]x& \\
(rtom3) & \lambda x\rtom\nil & = & \delta & \mbox{ if 
}\idx{\lambda}\neq 1 \\
(rtom4) & \nil\rtom\nil & = & \delta &\\
(rtom5) & (x+y)\rtom\nil & = & x\rtom\nil + y\rtom\nil & \\
(rtom6) & x\rtom(y+z) & = & x\rtom y + x\rtom z & \\
\hline
(merge) & x\merge{k} y & = & x\lmerge{k} y + x\rmerge{k} y & \\
\hline
(lmerge1) & \lambda x\lmerge{k}y & = & \lambda (x\merge{k+1}[1]y) & 
\mbox{ if }\idx{\lambda}\neq k\\
(lmerge2) & \lambda x\lmerge{k}y & = & \delta & \mbox { if } \idx{\lambda}=k 
\\
(lmerge3) & \nil\lmerge{k}x & = & \delta &\\
(lmerge4) & (x+y)\lmerge{k}z & = & x\lmerge{k}z + y\lmerge{k}z & \\
\hline
(rmerge1)  & x\rmerge{k}\lambda y & = & \lambda ([1]x\merge{k+1}y) &\\
(rmerge2) &  a^{k} x\rmerge{k}\nil & = & [-1]x& \\
(rmerge3) & \lambda x\rmerge{k}\nil & = & \delta & \mbox{ if 
}\idx{\lambda}\neq k \\
(rmerge4) & \nil\rmerge{k}\nil & = & \delta &\\
(rmerge5) & (x+y)\rmerge{k}\nil & = & x\rmerge{k}\nil + y\rmerge{k}\nil & \\
(rmerge6) & x\rmerge{k}(y+z) & = & x\rmerge{k}y + x\rmerge{k}z & \\
  \hline
\end{array}$$}
\caption{Axioms for the refinement operator} \label{axiom2}
\end{table}

\subsection{Soundness and Completeness}
We cannot apply the algorithm presented in \cite{Aceto} because the rules 
of our TSS do not fit the GSOS format used in that paper, due to the presence in our TSS of
lookahead and of an infinite set of rules and operators. However, we follow the lines 
presented there.

Given a set $E$ of equations between terms, and $t=t'$ another
equation, we write $E \vdash t=t'$ to indicate that the equation
$t=t'$ is derivable from $E$ by means of equational logic.
The rules of equational logic assert that equality is a congruence 
that it is preserved by instantiation of variables.
For a formal definition see, e.g.\ \cite{Hen}.

In the following we state that the theory ${\cal T}$ is sound and 
complete with respect to $\bisimm{}$.

\begin{teorema}  \label{consistaxiom}
If $(t = t')\in{\cal T}$ then for any closed substitution $\rho$ we have 
$\rho(t)\bisimm{}\rho(t')$.
\dimo
We report the proofs for a selected set of significant axioms.
\\
Let $\rho$ be a closed substitution.
\\
{\bf (ref2)}
We want to prove that $\rho((a^{+}x)\refin{y})\bisimm{}\rho((x\refin{y})\rtom 
y)$, that is\\
$(a^{+}\rho(x))\refin{\rho(y)} \bisimm{}(\rho(x)\refin{\rho(y)}) 
\rtom \rho(y)$.
        
If $(a^{+}\rho(x))\refin{\rho(y)}\deriv{\theta}t$ three cases may occur.
\begin{itemize}\vspace{-1ex}
\item
The transition is obtained by applying $({\it REF}1)$. Then  the transition 
$a^{+}\rho(x)\deriv{\theta}$ is derivable, with $\theta\neq a$. 
This transition can be obtained in two ways:
\\
by $({\it SEQ}1)$, so we need that $a^{+}\deriv{\theta}$, but the 
only transition for $a^{+}$ is $a^{+}\deriv{a}\epsilon$, hence $\theta = a$ 
(contradiction); or
\\
by $({\it SEQ}2)$, but we need that $a^{+}\deriv{\surd}$ 
(contradiction).\vspace{-1ex}
\item
The transition is obtained by applying $({\it REF}2)$. Then we have that 
$\theta\neq\surd$,
$a^{+}\rho(x)\deriv{a}u$, $\rho(y)\deriv{\theta}v$ and $t = 
u\refin{\rho(y)}\merge{1}v$.
The transition $a^{+}\rho(x)\deriv{a}u$
can be obtained only by an application of $({\it ACT}3)$ and $({\it
SEQ}1)$, so we  have that $u = \nil\rho(x)$, from which $t\hspace{-1.59pt} =
\nil\rho(x)\refin{\rho(y)}\merge{1}v$.
Applying $({\it RTOM}1)$ to the transition $\rho(y)\deriv{\theta}v$ (remember 
that $\theta\neq\surd$) we obtain 
$(\rho(x)\refin{\rho(y)}) \rtom \rho(y)\deriv{\theta} (\rho(x)\refin{\rho
(y)})\merge{1}v$.
 From the soundness of axiom $({\it seq}4)$ we have that 
$\nil\rho(x)\bisimm{}\rho(x)$, thus 
from the congruence property of $\bisimm{}$ we have 
$t\bisimm{}(\rho(x)\refin{\rho (y)})\merge{1}v$.\vspace{-1ex}
\item
The transition is obtained by applying $({\it REF}3)$. Then we have 
$a^{+}\rho(x)\deriv{a}u$, $u\deriv{a^{1}}u'$, $[-1][-1](u'\refin{\rho(y)}) 
\deriv{\theta}t$ and $\rho(y)\deriv{\surd}v$.
As in the previous case, we have $u = \nil\rho(x)$. The only
explanation for the transition $\nil\rho(x)\deriv{a^{1}}u'$ is through
$({\it SEQ}2)$ and $({\it TICK})$, thus it must be that $\rho(x)\deriv{a^{1}}u'$.
Being $a^{1}\neq a$, with an application of $({\it REF}1)$ to this transition
we obtain $\rho(x)\refin{\rho(y)}\deriv{a^{1}}u'\refin{\rho(y)}$.
Applying $({\it RTOM}2)$ yields $(\nil\rho(x)\refin{\rho(y)})\rtom\rho(y)
\deriv{\theta} t$.\vspace{-1ex}
\end{itemize}
Symmetrically, we obtain that if $(\rho(x)\refin{\rho(y)})\rtom\rho(y)
\deriv{\theta}t$ there exists an $u$ such that 
$(a^{+}\rho(x))\refin{\rho(y)}\deriv{\theta}u$ and $t\bisimm{} u$.

\noindent
{\bf (delay1)}
We want to prove that $[k](\lambda \rho(x)) \bisimm{}\trans{\lambda}{k}
([\incr{k}]\rho(x))$.

Suppose that $[k](\lambda \rho(x))\deriv{\theta}t$. This transition can 
be obtained only by $({\it DELAY})$; so there exist
$\theta'$ and $u$ such that $\lambda\rho(x)\deriv{\theta'}u$, $\theta = 
\trans{\theta'}{k}$ and $t = [\incr{k}]u$.
 From $\lambda\rho(x)\deriv{\theta'}u$ we can derive that $\lambda\neq\delta$,
$\theta'=\lambda$ and $u = \nil\rho(x)$. Hence $\trans{\lambda}{k} = \theta$
and with (${\it ACT}$3 or 4) and $({\it SEQ}1)$ we obtain that 
$\trans{\lambda}{k}([\incr{k}]\rho(x))\deriv{\theta}\nil([\incr{k}]\rho(x))$.
 From the soundness of axiom $(seq4)$ and the congruence property of 
$\bisimm{}$ we have that $[\incr{k}]\nil\rho(x)\bisimm{}
\nil([\incr{k}]\rho(x))$.

The other direction of the proof is similar.

\noindent
{\bf (rtom2)}  
We want to prove that $(a^{1}\rho(x))\rtom\nil \bisimm{}[-1][-1]\rho(x)$.
        
Suppose that $(a^{1}\rho(x))\rtom\nil\deriv{\theta}t$.
Because the only possible transition for $\nil$ is 
$\nil\deriv{\surd}\delta$, the transition above  cannot be obtained by an 
application of the rule $({\it RTOM}1)$. Hence $({\it RTOM}2)$ has
been applied.
As the only transition for $a^{1}\rho(x)$ is $a^{1}\rho(x)
\deriv{a^{1}}\nil\rho(x)$ it must be that $[-1][-1]\nil\rho(x)\deriv{\theta}t$.
 From the soundness of axiom $({\it seq}4)$ and the congruence property of 
$\bisimm{}$ we have that $[-1][-1]\nil\rho(x)\bisimm{}
[-1][-1]\rho(x)$, so we have that $[-1][-1]\rho(x)\deriv{\theta}u$ 
and $t\bisimm{} u$.
        
Again the other direction of the proof is similar.
\fine
\end{teorema}

\begin{corollario}  \label{consist}
If ${\cal T}\vdash t = t'$ then for any closed substitution $\rho$ we have
$\rho(t)\bisimm{}\rho(t')$.
\fine
\end{corollario}

\begin{definizione}
A term $t\in T(\Sigma')$ is in {\em normal form} if it can be generated by 
the following grammar:
\[ n::= \nil\mid \delta \mid a^{+}\seq n \mid a^{k}\seq n \mid n + n' \]
A term $t\in T(\Sigma')$ can be {\em brought in normal form} if
there is a term $n$ in normal form with ${\cal T} \vdash t=n$.
\fine
\end{definizione}

\begin{definizione}
Let $n$ be a term in normal form. The length of $n$ is defined in the 
following way:
\[\begin{array}{l}
l(\nil) = 1 \hspace{1cm}
l(a^{+}\seq n)  =  l(n) + 1 \\
l(\delta)  =  1\hspace{1cm} 
l(a^{k}\seq n)  =  l(n) + 1 \\
l(n+n')  =  l(n) + l(n') + 1
\end{array}\vspace{-4.5ex}\]
\fine
\end{definizione}

\begin{lemma}    \label{operatornorm}
Let $n$ and $m$ be terms in normal form. Then 
\newcounter{itm}
\begin{list}{\theitm.}{\leftmargin20pt\labelwidth15pt\labelsep5pt
\usecounter{itm}\topsep 0pt\itemsep 0pt\parsep 0pt}
\item the term $n\seq m$
can be brought in normal form;
\item for all $k\neq 0$ there exists a term $n'$ in normal form with
${\cal T} \vdash [k]n = n'$ and $l(n')=l(n)$;
\item the terms $n\lpar m$, $n\sync m$ and $n\para m$
can be brought in normal form;
\item for all $k>0$ the terms $n\rmerge{k}m$, $n\lmerge{k}m$ and $n\merge{k}m$
can be brought in normal form;
\item the term $n\rtom m$ can be brought in normal form;
\item and the term $n\refin{m}$ can be brought in normal form.
\end{list}
\dimo
We establish part 4 with induction on the sum of the length of $n$ and $m$.
The other parts proceed likewise.
\\
Let $n$ and $m$ be two terms in normal form and $l(n) + l(m) = i$.
We first prove that there exists a term $p$ in normal form such that
${\cal T}\vdash n\rmerge{k} m = p$.
\begin{list}{$\bullet$}{\leftmargin20pt\labelwidth15pt\labelsep5pt
\topsep 4pt\itemsep 0pt\parsep 0pt}
\item  
        if $m$ is $\nil$ we can have the following cases:
        \begin{list}{\bf --}{\leftmargin20pt\topsep 0pt\itemsep 0pt\parsep 0pt}
        \item  
                if $n$ is $\nil$, we have that $\nil\rmerge{k}\nil = 
                \delta$ $({\it rmerge}4)$, and $\delta$ is in normal form.      
        \item 
                if $n$ is $\delta$, we use that $\delta = 
                \delta x$ (seq3). Thus, using $({\it rmerge}3)$ we have 
                $\delta \rmerge{k} \nil = \delta x \rmerge{k} \nil = \delta$.
        \item
                if $n$ is $a^{+} n'$ we have 
                $a^{+}n'\rmerge{k}\nil = \delta$, by $({\it rmerge}3)$.
        \item
                if $n$ is $a^{h}n'$ and $h\neq k$, we also have
                $a^{h}n'\rmerge{k}\nil = \delta$.
        \item
                if $n$ is $a^{k}n'$, we have $a^{k}n'\rmerge{k}\nil =
                [-1]n'$ by $({\it rmerge}2)$, on which we apply part 2 of the lemma.
        \item
        if $n$ is $n'+n''$, we have 
        $(n'+n'')\rmerge{k}\nil = n'\rmerge{k}\nil + n''\rmerge{k}\nil$ by
        $({\it rmerge}5)$. As $l(n'),l(n'')<l(n)$, we may apply the induction
        hypothesis, so there must be terms $p'$ and $p''$ 
        in normal form such that $n'\rmerge{k}\nil = p'$ and
        $n''\rmerge{k}\nil = p''$. It follows that
        $(n'+n'')\rmerge{k}\nil = p'+p''$.
        \end{list}
\item
        if $m$ is $\delta$: $n\rmerge{k}\delta \stackrel{seq3}{=}
        n\rmerge{k}(\delta x) \stackrel{rmerge 1}{=}
        \delta([1]n\merge{k+1} x) \stackrel{seq3}{=} \delta$. 
\item
        if $m$ is $a^{+} m'$: by $({\it rmerge}1)$ we obtain $n\rmerge{k} (a^{+}m') =
        a^{+}([1]n\merge{k+1}m')$.
        By part 2 of the lemma there exists a term $n'$ in normal form 
        such that $[1]n = n'$ and $l(n) = l(n')$.
        As equality is a congruence we have $[1]n\merge{k+1}m' =
        n'\merge{k+1}m'$. Moreover,  
        $l(n') + l(m')<i$, so, by induction, there exists a term $p'$ in 
        normal form such that $n'\merge{k+1}m' = p'$; it follows
        that $n\rmerge{k} a^{+} m' = 
        a^{+} p'$, where $a^{+} p'$ is in normal form.
\item
        if $m$ is $a^{k} m'$, the proof is equal to the above one.
\item
        if $m$ is $m'+m''$, by $({\it rmerge}6)$ we obtain $n\rmerge{k} 
        (m'+m'') = n\rmerge{k}m' + n\rmerge{k}m''$, which by induction
        can be brought in normal form.
\end{list}
Following the same lines, we can bring $n\lmerge{k}m$ in normal form.
Finally, $n\merge{k}m$ is brought in normal form through an application
of $(merge)$, using the normalisation of $n\rmerge{k}m$ and $n\lmerge{k}m$.
\fine
\end{lemma}

\begin{teorema}  \label{normform}
Let $t\in T(\Sigma')$.
There exists then a term $n$ in normal form such that  ${\cal 
T}\vdash t = n$.
\fine
\end{teorema}
This theorem follows by induction from lemma \ref{operatornorm}.
Due to the presence of axioms like $({\it rtom}2)$, lemma \ref{operatornorm}
cannot be replaced by a simpler lemma, only obtaining {\em head normal
forms}, as in \cite{Aceto}.

\begin{lemma}  \label{normCompl}
Let $n$, $m$ be closed terms in normal form.
If $n\bisimm{} m$ then ${\cal T}\vdash n = m$.
\dimo
Standard (see \cite{HenMil}).
\fine
\end{lemma}

\begin{corollario}
Let $t,t'\in T(\Sigma')$.
If $t\bisimm{} t'$ then ${\cal T}\vdash t = t'$.
\fine
\end{corollario}

\section{Concluding Remarks}
In this section, we discuss some further issues. First we provide an 
alternative operational description of refinement which exploits the 
parallel composition operator (with synchronisation allowed on 
a special end action $e$ only). Then, we compare 
the various approaches to the empty refinement (i.e.\ when the
refining agent is properly terminated) that appear in the literature.
Finally, we comment on related work on other operational
versions of ST semantics and definitions of action refinement. 

\subsection{Coding Refinement with Parallel Composition}
The operational description of action refinement and its 
axiomatisation we provide in Sections \ref{operational} and
\ref{axiomatisation} have the merits
of being ``context-free'', in the sense that these rules and 
axioms can be ``plugged in'' in any other operational 
and axiomatic description of a process algebra, provided that
this algebra is equipped with choice and action-prefix operators.

Anyway, it is easy to see that the merge operator is indeed a
kind of parallel composition, preventing synchronisations between
the refined agent and the refining one. \nopagebreak
Hence, with the aim at minimising the number of rules and axioms, 
here we present an alternative description of action refinement 
which implements the merge through a slight modification of 
parallel composition, using also the sequential composition
operator. 
In the following, operators $\merge{k}$, $\rtom$, $\rmerge{k}$ and 
$\lmerge{k}$ are no longer
used. On the other hand, we introduce a new constant $e$, exploited to
signal termination of the refining agent (not to be confused with 
$\surd$), and a new unary operator $\sk$ which ``skips'' the transitions
labelled by $e$.

The idea consists in replacing the ending phase of the currently refined
action with the special action $e$, which will be 
added also at the end of the refining term. 
Then we put in parallel the remaining part of the refined term 
with the refining one, preventing any synchronisation on normal
actions, but forcing the synchronisation on label $e$.
Subsequently, the now ``useless'' $e$-labelled transitions are skipped
via the new unary operator $\sk$. In the following,
labels $\eta$ and $\theta$ range also over $e$.
The rules for the new operators are listed below:

\[\begin{array}{|lcl|}
  \hline
&&\\
(END) & e\deriv{e}\nil &\\
&&\\
(SKIP1) & \bigfrac{x\deriv{\theta}x'}{\sk(x)\deriv{\theta}\sk(x')} & 
\theta\neq e \\
&&\\
(SKIP2) & \bigfrac{x\deriv{e}x'\spazio 
[-1]x'\deriv{\theta}x''}{\sk(x)\deriv{\theta}x''} &\\
&&\\
\hline
\end{array}\]

The rules for parallel composition are to be modified slightly in order
to cope with the new label $e$, which is always a synchronisation action
(similarly to $\surd$).
The other rules in the original TSS are unchanged, except for the fact
that now the variables $\eta$ and $\theta$ can take also the value $e$.
The three rules for refinement are now replaced by the two rules
below, where the second one covers also the case of empty refinement.
\[\begin{array}{|lcl|}
  \hline
&&\\
(REF1) & \bigfrac{x \deriv{\theta} x'} {x  \refin{y} \deriv{\theta}
x'\refin{y}}   & \theta \neq a\\
&&\\
(REF2) & \bigfrac{x \deriv{a} x'\spazio
\sk([-1](x'\refin{y})\parallel y e)\deriv{\theta}y'}
{x\refin{y}\deriv{\theta} y'} &\\
&&\\
\hline
\end{array}\]

The delay rule remains the same, but function $f$ is
changed by substituting the end action $e$ for the ending phase 
of the refined action.
$$
\trans{a^{h}}{k} = \left\{
\begin{array}{ll}
a^{h} & \mbox{ if }h\leq|k|-1 \\
e & \mbox{ if }h=-k \\
a^{h+sg(k)} & \mbox{ otherwise }
\end{array}\right. 
$$
Note that the value of $\trans{a^h}{-h}$ is not significant in the
preceding sections; if we would have had an action $e$, we could just
as well have defined $f$ as above from the beginning.

Also for the axiomatisation, all the axioms related to the dropped
operators are removed. Moreover, the axioms for the synchronisation merge
take into account the fact that $e$ is a synchronisation action.
Below the axioms for the new operators and for the new definition of
action refinement are reported, where now $\lambda$ can also take 
the value $e$.

\[\begin{array}{|lrcl|}
  \hline
(ref1) & (\lambda x)\refin{y} & = & 
\begin{array}{lr}
\lambda (x\refin{y}) & \mbox{  if  
}\lambda\not=a^{+} 
\end{array}\\
(ref2) & (a^{+} x)\refin{y} & = & \sk([-1](x\refin{y})\parallel ye)  \\
(ref3) & \nil\refin{y} & = & \nil  \\
(ref4) & (x+y)\refin{z} & = & x\refin{z} + y\refin{z}  \\
\hline
(skip1) & \sk(\lambda x) & = & 
\begin{array}{lr}
\lambda \sk(x) & \mbox{  if  }\lambda\neq e
\end{array} \\
(skip2) & \sk(e x) &=& [-1]x  \\
(skip3) & \sk(\nil)& = &\nil \\
(skip4) & \sk(x+y) &=& \sk(x) + \sk(y) \\
\hline
\end{array}\]

The reader can easily get convinced that this formulation is
equivalent to the one of Sections 4 and 5.


\subsection{Empty Refinements}

There exists no general agreement on what an empty refinement, 
i.e.\ the refinement of an action into a successfully terminated 
process, should be. Our proposal differs from those that
already appeared in the literature.

In \cite{GlGo1} an interpretation of the empty refinement is 
offered in the domain of prime event structures, according to which 
events refined into the empty structure are simply erased; 
a consequence of this decision is that the congruence result for ST
bisimulation semantics does not hold in this approach, as shown in
\cite{Glabbeek}. Moreover they argue that these {\em forgetful
refinements} can drastically change the behaviour of concurrent
systems and can not be explained by a change in the level of
abstraction at which these systems are regarded \cite{GlGo2}.
In \cite{DegGor}, the empty refinement is treated as if the refining 
agent were deadlocked. The justification for this proposal is
that empty refinement is an erroneous step in the top-down
development procedure. In this way, the congruence property is kept.
We could obtain the same result by skipping rule $({\it REF}3)$.

Now we introduce an example to illustrate the differences among
these interpretations of empty refinement.
Let $t = (a b \parallel_{b} (b+c) \parallel_{c}c d )\parallel_{ad} a d$.
In Figure \ref{t} this expression is depicted as an event structure.
The densely dotted line indicates syntactic conflict, as specified by
the $+$-operator in $t$. The sparsely dotted line indicates inherited
or semantic conflict: the events $b$ and $d$ cannot occur in the same
run as $c$ is a prerequisite of $d$ and in (syntactic) conflict with $b$.

\begin{figure}[htb]
\begin{center}
\setlength{\unitlength}{1in}
\begin{picture}(1,.9)(0,.1)
\put(0,1){$a$}
\put(0,0){$b$}
\put(1,1){$c$}
\put(1,0){$d$}

\put(0.03,.95){\vector(0,-1){.8}}
\put(0.13,.95){\vector(1,-1){.8}}
\put(1.03,.95){\vector(0,-1){.8}}
\multiput(.08,.06)(.03,.03){30}{$\cdot$}
\multiput(.11,0)(.1,0){9}{$\cdot$}
\end{picture}
\end{center}
\caption{Event structure representation of $t$}
\label{t}
\end{figure}

\begin{figure}[htb]
\begin{center}
\setlength{\unitlength}{.7cm}
\begin{picture}(18,5)(.5,0)
\put(1,5){\vector(0,-1){1}}
\put(1,4){\vector(0,-1){1}}
\put(1,3){\vector(0,-1){1}}
\put(1,2){\vector(0,-1){1}}
\put(1.1,-0.5){\tt a)}
\put(1.6,4.4){$a$}
\put(1.6,3.4){$a^{1}$}
\put(1.6,2.4){$b$}
\put(1.6,1.4){$b^{1}$}

\put(8,5.5){\vector(0,-1){1}}
\put(8,4.5){\vector(0,-1){1}}
\put(8,3.5){\vector(1,-1){1}}
\put(8,3.5){\vector(-1,-1){1}}
\put(9,2.5){\vector(1,-1){1}}
\put(7,2.5){\vector(-1,-1){1}}
\put(6,1.5){\vector(0,-1){1}}
\put(10,1.5){\vector(0,-1){1}}
\put(8.2,5){$a$}
\put(8.2,4){$a^{1}$}
\put(7.1,3){$b$}
\put(6.1,2){$b^{1}$}
\put(8.8,3){$d$}
\put(9.8,2){$d^{1}$}
\put(5.4,1){$\surd$}
\put(10.2,1){$\surd$}
\put(7.9,-0.5){\tt b)}

\put(16,5.5){\vector(-1,-1){1}}
\put(15,4.5){\vector(0,-1){1}}
\put(15,3.5){\vector(1,-1){1}}
\put(15,3.5){\vector(-1,-1){1}}
\put(16,2.5){\vector(0,-1){1}}
\put(14,2.5){\vector(0,-1){1}}
\put(14,1.5){\vector(0,-1){1}}
\put(16,1.5){\vector(0,-1){1}}

\put(16,5.5){\vector(1,-1){1}}
\put(17,4.5){\vector(1,-1){1}}
\put(18,3.5){\vector(0,-1){1}}
\put(18,2.5){\vector(0,-1){1}}
\put(18,1.5){\vector(0,-1){1}}
\put(15.1,5){$a$}
\put(16.7,5){$a$}
\put(14.4,4){$a^{1}$}
\put(17.5,4.2){$a^{1}$}
\put(14.1,3){$b$}
\put(17.4,3){$d$}
\put(13.4,2){$b^{1}$}
\put(17.4,2){$d^{1}$}
\put(15.7,3){$d$}
\put(16.2,2){$d^{1}$}
\put(13.4,1){$\surd$}
\put(16.2,1){$\surd$}
\put(17.3,1){$\surd$}
\put(14.9,-0.5){\tt c)}
\end{picture}
\end{center}
\caption[Three views on forgetful refinement]{$t[c\leadsto \nil]$
according to {\tt a)} \cite{DegGor}, {\tt b)} \cite{GlGo1} and {\tt
c)} \cite{Vrancken}} \label{opera}
\end{figure}

If we refine the action $c$ into $\nil$ in $t$, following the paradigm
of \cite{DegGor}, event $c$ is blocked and the resulting system is
equivalent to $a b \delta$, corresponding with the ST transition system
in Figure \ref{opera}a. If we, in the spirit of \cite{GlGo1}, simply
erase event $c$ in a model of event structures (such as {\em flow
event structures} \cite{Boudol}) where semantic conflict is merely a
matter of interpretation, we would obtain a system that is equivalent
to $a(b\|d)$, in which the conflict between $b$ and $d$ is dropped.
However, the forgetful refinements of \cite{GlGo1,Glabbeek} are
considered on {\em prime} event structures \cite{NPW}, were semantic
conflict has the same status as syntactic conflict. Here the result is
$a(b+d)$, corresponding to the ST transition system in Figure
\ref{opera}b. A reason to dislike this result is that the choice
between $b$ and $d$ is made only after the $a$ occurred, whereas in
the original system a commitment to do $d$ could be made earlier
through the occurrence of $c$. Hence this notion of forgetful
refinement can mask deadlock behaviour of concurrent systems.
In \cite{Vrancken} the empty refinement is called `renaming into
$\nil$' and $\refin{\nil}$ is denoted $\nil_{\{a\}}$. His solution
would yield $a(b+d)+ad$, which better captures the branching structure
between the executions $ab$ and $ad$. But \cite{Vrancken} works in
interleaving semantics (and doesn't consider other types of action
refinement) and consequently his solution cannot capture the fact that
the choice between these executions can be made at any moment during
the execution of $a$. This is captured by the operational semantics
defined in Section 4. We obtain the transition system in Figure
\ref{ours}.

\begin{figure}[htb]
\begin{center}
\setlength{\unitlength}{.7cm}
\begin{picture}(10,4.5)(0,1)
\put(5,5.5){\vector(-1,-1){1}}
\put(5,5.5){\vector(1,-1){1}}
\put(4,4.5){\vector(-1,-1){1}}
\put(4,4.5){\vector(1,-1){1}}
\put(6,4.5){\vector(1,-1){1}}
\put(3,3.5){\vector(-1,-1){1}}
\put(3,3.5){\vector(1,-1){1}}
\put(2,2.5){\vector(0,-1){1}}
\put(4,2.5){\vector(0,-1){1}}
\put(2,1.5){\vector(0,-1){1}}
\put(4,1.5){\vector(0,-1){1}}
\put(5,3.5){\vector(0,-1){1}}
\put(5,2.5){\vector(0,-1){1}}
\put(5,1.5){\vector(0,-1){1}}
\put(7,3.5){\vector(0,-1){1}}
\put(7,2.5){\vector(0,-1){1}}
\put(7,1.5){\vector(0,-1){1}}
\put(4.1,5){$a$}
\put(5.7,5){$a$}
\put(3.1,4){$a^{1}$}
\put(4.7,4){$a^{1}$}
\put(6.7,4){$a^{1}$}
\put(2.1,3){$b$}
\put(1.4,2){$b^{1}$}
\put(3.7,3){$d$}
\put(4.1,2){$d^{1}$}
\put(1.4,1){$\surd$}
\put(4.1,1){$\surd$}
\put(5.2,3){$d$}
\put(5.2,2){$d^{1}$}
\put(5.2,1){$\surd$}
\put(7.2,3){$d$}
\put(7.2,2){$d^{1}$}
\put(7.2,1){$\surd$}
\end{picture}
\end{center}
\caption{The ST transition system for $t[c\leadsto \nil]$ according 
to our rules.}
\label{ours}
\end{figure}

As this transition system cannot be obtained as the image
of an event structure, it follows that event structures are not
expressive enough for this type of empty refinement.

\subsection{Related Work}
In this section, we briefly describe some related work
on alternative operational ST semantics and on alternative operational
definitions of action refinement.

\paragraph{Different Approaches to ST Semantics} 
We restrict our attention to those proposals for which ST-bisimulation
semantics is defined as standard bisimulation on a transition system
labelled on suitable phases of actions. 

In \cite{AH1} Aceto and Hennessy study a finite process algebra
equipped with a parallel composition operator which does not permit 
synchronisation. For this simple language they define, as we do here,
a transition system labelled on action phases, where however the
endings are not provided with pointers.
Standard bisimulation equivalence gives rise to an equivalence
relation called by the authors {\em timed} equivalence,
which is also known in the literature under the name of 
{\em split$_{2}$} equivalence \cite{Glabbeek,GorLan}. 
Timed equivalence coincides with ST-bisimulation equivalence because of the
limited expressive power of the language they investigate.
An elegant equational characterisation of timed equivalence
is provided.

An operational ST semantics for full CCS \cite{Mil} is reported in 
\cite{GorLan2} where the pointers from endings to
beginnings are ``absolute'', i.e.\ the index $k$ in $a^k$
indicates that the ending refers to the $k$-th started
action. 
This makes the definition of an operational semantics much more
involuted because there is the need of a global counter (states are
pairs $\langle t, z \rangle$, where $t$ is a process term and $z$ is
a natural number) in order to implement the absolute referencing, and
rules must be specialised to beginnings and endings (hence, duplicated)
because only at beginnings pointers are increased. In this paper, no
axiomatisation is proposed and action refinement is not considered. 

In \cite{Hen2}, an operational semantics with ``weak''
transitions (i.e.\ transitions corresponding to those of weak
bisimulation \cite{Mil}) for a CCS-like language is presented.
However, the transition system generated is infinitely-branching
also for finite (i.e.\ recursion free) agents. 
Moreover, the operational rules for parallel composition are
context-dependent. On this basis, a non-standard proof system is proposed,
composed of conditional, context-dependent equations. Also in this
paper action refinement is not considered.
 
\paragraph{Other Operational Semantics for Action Refinement}
There are three papers dealing with this problem, the first one 
working with timed semantics \cite{AH1}, the second one with
a causal semantics \cite{DegGor} and the last one with the even finer 
semantics of event isomorphism \cite{Ren}.

In \cite{AH1} an operational semantics in SOS style
for the operator of action refinement --- $x\refin{y}$ --- is 
defined following tightly the inductive structure of the term 
$x$ to which the operator is applied.
For instance, if $x = x_1 + x_2$, then $x\refin{y}$ can do
whatever $x_1\refin{y}$ and $x_2\refin{y}$ are able to do.
This definition is equivalent to making a complete syntactic subsitution
of the refining agent $y$ for any occurrence of $a$ in $x$ before
executing the agent. (Compare the classic notion of the ``dynamic''
copy rule opposed to the static one for the implementation
of procedure calls.)
This operational semantics, however, does not scale easily
to langauges which include communication and restriction; 
moreover, the basic 
intuition of refinement in such a case is no longer in full 
agreement with the corresponding operation on Event Structures.

In \cite{DegGor} a causal operational semantics is introduced
for action refinement in a finite language which is very close
to ours (the only difference is that we take ACP sequential
composition instead of CCS action prefixing). This work
relies upon previous work \cite{DaDe}, where Darondeau and Degano 
prove that the inductive definition of action refinement they 
propose on Causal Trees coincides with the one they propose
on a special subclass of Event Structures, called {\em $\Delta$-free}.
Our work owes some basic intuition to \cite{DegGor}, which 
is similar in spirit, except for the way the empty
refinement is dealt with.

In \cite{Ren} Rensink shows that action refinement can receive
a simple operational treatment when working with the very concrete 
semantics induced by event isomorphism. This definition
is proved to agree with a denotational operation of refinement
defined over his model of {\em families of posets}.

In our opinion, the main merit of our proposal w.r.t. the last two
is that we (arguably) use the ``right'' semantics,  
as ST-bisimulation equivalence has been proved to be the coarsest
congruence contained in interleaving bisimulation \cite{Vog}. 
However,
the other two proposals define transition systems which are smaller
because actions do not have to be split in phases.

\begin{thebibliography}{10}

\bibitem{Aceto}
{\sc L.~Aceto, B.~Bloom \& F.W. Vaandrager} (1994):
\newblock {\em Turning {SOS} rules into equations.}
\newblock {\sl Information and Computation} 111(1), pp. 1--52.
\vspace{-1ex}
\bibitem{AH1}
{\sc L.~Aceto \& M.~Hennessy} (1993):
\newblock {\em Towards action-refinement in process algebras.}
\newblock {\sl Information and Computation} 103(2), pp. 204--269.
\vspace{-1ex}
\bibitem{BK-ACP}
{\sc J.A. Bergstra \& J.W. Klop} (1986):
\newblock {\em Algebra of communicating processes.}
\newblock In J.W.~de Bakker, M.~Hazewinkel \& J.K. Lenstra, editors: {\sl Mathematics and Computer Science}, CWI Monograph 1, North-Holland, Amsterdam, pp. 89--138.
\vspace{-1ex}
\bibitem{Boudol}
{\sc G.~Boudol} (1990):
\newblock {\em Flow event structures and flow nets.}
\newblock In I.~Guessarian, editor: {\sl Semantics of Systems of Concurrent Processes, {\rm Proceedings LITP Spring School on Theoretical Computer Science, La Roche Posay, France}}, {\sl \rm LNCS} 469, Springer-Verlag, pp. 62--95.
\vspace{-1ex}
\bibitem{Busi}
{\sc N.~Busi} (1993):
\newblock {\em Raffinamento di azioni in linguaggi concorrenti.}
\newblock Master's thesis, Universit\`{a} di Bologna.
\vspace{-1ex}
\bibitem{DaDe}
{\sc Ph. Darondeau \& P.~Degano} (1993):
\newblock {\em Refinement of actions in event structures and causal trees.}
\newblock {\sl Theoretical Computer Science} 118(1), pp. 21--48.
\vspace{-1ex}
\bibitem{DegGor}
{\sc P.~Degano \& R.~Gorrieri}:
\newblock {\em A causal operational definition of action refinement.}
\newblock {\sl Information and Computation}.
\newblock To appear.
\vspace{-1ex}
\bibitem{Fok}
{\sc W.J. Fokkink} (1994):
\newblock {\em The tyft/tyxt format reduces to tree rules.}
\newblock In {\sl Proc. Theoretical Aspects of Computer Science, {\rm Sendai, Japan}}, {\sl \rm LNCS} 789, Springer-Verlag, pp. 440--453.
\vspace{-1ex}
\bibitem{Glabbeek}
{\sc R.J.~van Glabbeek} (1990):
\newblock {\em The refinement theorem for {ST}-bisimulation semantics.}
\newblock In M.~Broy \& C.B. Jones, editors: {\sl {\rm Proceedings IFIP TC2 Working Conference on} Programming Concepts and Methods, {\rm Sea of Gallilea, Israel}}, North-Holland, pp. 27--52.
\vspace{-1ex}
\bibitem{vGamast}
{\sc R.J.~van Glabbeek} (1993):
\newblock {\em Full abstraction in structural operational semantics (extended abstract).}
\newblock In M.~Nivat, C.~Rattray, T.~Rus \& G.~Scollo, editors: {\sl {\rm Proceedings of the Third International Conference on} Algebraic Methodology and Software Technology (AMAST'93), {\rm Twente, The Netherlands, June 1993}}, Workshops in Computing, Springer-Verlag, pp. 77--84.
\vspace{-1ex}
\bibitem{GlGo1}
{\sc R.J.~van Glabbeek \& U.~Goltz} (1989):
\newblock {\em Equivalence notions for concurrent systems and refinement of actions.}
\newblock In A.~Kreczmar \& G.~Mirkowska, editors: {\sl {\rm Proceedings} Mathematical Foundations of Computer Science 1993 (MFCS), {\rm Por{\pa}bka-Kozubnik, Poland}}, {\sl \rm LNCS} 379, Springer-Verlag, pp. 237--248.
\vspace{-1ex}
\bibitem{GlGo2}
{\sc R.J.~van Glabbeek \& U.~Goltz} (1990):
\newblock {\em Refinement of actions in causality based models.}
\newblock In J.W. de~Bakker, W.P.~de Roever \& G.~Rozenberg, editors: {\sl {\rm REX Workshop on} Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness, {\rm Mook, The Netherlands 1989}}, {\sl \rm LNCS} 430, Springer-Verlag, pp. 267--300.
\vspace{-1ex}
\bibitem{GlaVaan}
{\sc R.J.~van Glabbeek \& F.W. Vaandrager} (1987):
\newblock {\em Petri net models for algebraic theories of concurrency.}
\newblock In J.W.~de Bakker, A.J. Nijman \& P.C. Treleaven, editors: {\sl Proceedings PARLE conference, {\rm Eindhoven}, Vol. II (Parallel Languages)}, {\sl \rm LNCS} 259, Springer-Verlag, pp. 224--242.
\vspace{-1ex}
\bibitem{GorLan2}
{\sc R.~Gorrieri \& C.~Laneve} (1991):
\newblock {\em The limit of split$_{n}$ bisimulations for {CCS} agents.}
\newblock In A.~Tarlecki, editor: {\sl {\rm Proceedings} Mathematical Foundations of Computer Science 1991 (MFCS), {\rm Poland}}, {\sl \rm LNCS} 520, Springer-Verlag, pp. 170--180.
\vspace{-1ex}
\bibitem{GorLan}
{\sc R.~Gorrieri \& C.~Laneve}:
\newblock {\em Split and {ST} bisimulation semantics.}
\newblock {\sl Information and Computation}.
\newblock To appear.
\vspace{-1ex}
\bibitem{GroVaan}
{\sc 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.
\vspace{-1ex}
\bibitem{Hen}
{\sc M.~Hennessy} (1988):
\newblock {\em Algebraic Theory of Processes}.
\newblock MIT Press, Cambridge, Massachusetts.
\vspace{-1ex}
\bibitem{Hen2}
{\sc M.~Hennessy} (1991):
\newblock {\em A proof system for weak {ST} bisimulation over a finite process algebra.}
\newblock Technical report, Computer Science Department, University of Sussex.
\vspace{-1ex}
\bibitem{HenMil}
{\sc M.~Hennessy \& R.~Milner} (1985):
\newblock {\em Algebraic laws for nondeterminism and concurrency.}
\newblock {\sl Journal of the ACM} 32(1), pp. 137--161.
\vspace{-1ex}
\bibitem{Mil}
{\sc R.~Milner} (1989):
\newblock {\em Communication and Concurrency}.
\newblock Prentice-Hall International, Englewood Cliffs.
\vspace{-1ex}
\bibitem{NPW}
{\sc M.~Nielsen, G.D. Plotkin \& G.~Winskel} (1981):
\newblock {\em Petri nets, event structures and domains, part {I}.}
\newblock {\sl Theoretical Computer Science} 13(1), pp. 85--108.
\vspace{-1ex}
\bibitem{Plotkin}
{\sc G.D. Plotkin} (1981):
\newblock {\em A structural approach to operational semantics.}
\newblock Report DAIMI FN-19, Computer Science Department, Aarhus University.
\vspace{-1ex}
\bibitem{Ren}
{\sc A.~Rensink} (1993):
\newblock {\em Models and Methods for Action Refinement}.
\newblock PhD thesis, University of Twente.
\vspace{-1ex}
\bibitem{Vog}
{\sc W.~Vogler} (1993):
\newblock {\em Bisimulation and action refinement.}
\newblock {\sl Theoretical Computer Science} 114(1), pp. 173--200.
\vspace{-1ex}
\bibitem{Vrancken}
{\sc J.L.M. Vrancken} (1986):
\newblock {\em The algebra of communicating processes with empty process.}
\newblock Report FVI 86-01, Dept. of Computer Science, University of Amsterdam.

\end{thebibliography}

\end{document}
