\documentclass[runningheads]{llncs}
\usepackage{hyperref}
\usepackage{breakurl}
\usepackage{graphicx}
\usepackage{stmaryrd}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{mathrsfs}
\usepackage{times}
\input{macro-springer.tex}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%               Conflict replicating implementation                    %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\UI}{\Omega}             % Undo interfaces
\newcommand{\UIij}{\UI_{i}}          % Undo interface (i)
\newcommand{\ui}{\mbox{\it \i}}      % linking undo interfaces to transitions
\newcommand{\dist}[1][p]{\textsf{distribute}_#1}
\newcommand{\ini}[1][j]{\textsf{initialise}_#1}
\newcommand{\trans}[2][h]{\textsf{transfer}^#1_#2}
\newcommand{\exec}[2][i]{\textsf{execute}^#1_#2}
\newcommand{\fetch}[1][p,c]{\textsf{fetch}_{i,j}^{#1}}
\newcommand{\fetched}[2][i]{\textsf{fetched}^#1_#2}
\newcommand{\comp}[2][i]{\textsf{finalise}^#1}

\newcommand{\fire}{\textsf{fire}}
\newcommand{\undo}[1][i]{\textsf{undo}_{#1}}
\newcommand{\und}[1][f]{\textsf{undo}(#1)}
\newcommand{\undone}{\textsf{undone}}
\newcommand{\reset}[1][i]{\textsf{reset}_{#1}}
\newcommand{\elide}[1][i]{\textsf{elide}_{#1}}
\newcommand{\ack}[1][i]{\textsf{ack}_{#1}}
\newcommand{\keep}[1][i]{\rho_{#1}}
\newcommand{\Fired}{\textsf{fired}}
\newcommand{\take}{\textsf{take}}
\newcommand{\took}{\textsf{took}}

\newcommand{\Pre}{\textsf{pre}}
\newcommand{\transin}[2][h]{\textsf{trans}^#1_#2\textsf{-in}}
\newcommand{\transout}[2][h]{\textsf{trans}^#1_#2\textsf{-out}}
\newcommand{\fetchin}[1][p,c]{\textsf{fetch}_{i,j}^{#1}\textsf{-in}}
\newcommand{\fetchout}[1][p,c]{\textsf{fetch}_{i,j}^{#1}\textsf{-out}}

\newcommand{\ina}{\mbox{\scriptsize (\textit{in})}\;}
\newcommand{\out}{\mbox{\scriptsize (\textit{out})}\;}
\newcommand{\early}{\mbox{\scriptsize (\textit{early})}\;}
\newcommand{\late}{\mbox{\scriptsize (\textit{late})}\;}
\newcommand{\far}{\mbox{\scriptsize (\textit{far})}\;}
\newcommand{\weight}[1]{\hfill\mbox{\scriptsize $F'(#1)$}}

\newcommand{\leqc}{\leq^\#\!}
\newcommand{\confeq}{\mathbin{\plat{$\stackrel{\#}{=}$}}}
\newcommand{\confeqscript}{\stackrel{\#}{=}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%                          General maths                               %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\nat}{\bbbn}
\newcommand{\Int}{\bbbz}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%                        Petri net semantics                           %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\marking}[1]{\llbracket#1\rrbracket}  % token replacement function
\newcommand{\NF}{\mbox{\it NF}}                          % normal forms
\newcommand{\opt}[1]{\mbox{\tiny\rm(}#1\mbox{\tiny\rm)}} % optional action
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%                         Petri net images                             %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{pstricks}
\usepackage{pst-node}
\usepackage{graphicx}

\newrgbcolor{darkblue}{0 0 0.5}
\newrgbcolor{darkred}{0.7 0 0}

\newcounter{netimage}
\def\pn#1{n\thenetimage-#1}
\def\p#1:#2;{\cnode #1{0.3}{n\thenetimage-#2}}
\def\P#1:#2;{\p #1:#2;\pscircle*#1{0.1}}
\def\q#1:#2:#3;{\p #1:#2;\rput#1{\rput[l](0.45,0){\large #3}}}
\def\Q#1:#2:#3;{\P #1:#2;\rput#1{\rput[l](0.45,0){\large #3}}}
\def\qq#1:#2:#3;{\p #1:#2;\rput#1{\rput[t](0,-0.5){\large #3}}}
\def\ql#1:#2:#3;{\p #1:#2;\rput#1{\rput[r](-0.45,0){\large #3}}}
\def\qr#1:#2:#3;{\p #1:#2;\rput#1{\rput[l](0.45,0){\large #3}}}
\def\qt#1:#2:#3;{\p #1:#2;\rput#1{\rput[b](0,0.45){\large #3}}}
\def\qb#1:#2:#3;{\p #1:#2;\rput#1{\rput[t](0,-0.45){\large #3}}}
\def\Ql#1:#2:#3;{\P #1:#2;\rput#1{\rput[r](-0.45,0){\large #3}}}
\def\Qr#1:#2:#3;{\P #1:#2;\rput#1{\rput[l](0.45,0){\large #3}}}
\def\Qt#1:#2:#3;{\P #1:#2;\rput#1{\rput[b](0,0.45){\large #3}}}
\def\Qb#1:#2:#3;{\P #1:#2;\rput#1{\rput[t](0,-0.45){\large #3}}}
\def\qx#1:#2:#3:#4;{\p #1:#2;\rput#1{\rput#4{\large #3}}}
\def\QXX#1:#2:#3:#4:#5;{\p #1:#2;\rput#1{\rput#4{\large #3}}\pscircle*#5{0.1}}
\def\s#1:#2:#3;{\p #1:#2;\rput#1{\rput(-0.03,0){\large #3}}}
\def\t#1:#2:#3;{\rput#1{\rnode{n\thenetimage-#2}{\psframebox{%
  \vbox to 0.6cm{\vfil\hbox to 0.6cm{\hfil\Large #3\hfil}\vfil}}}}}
\def\u#1:#2:#3:#4;{\rput#1{\rnode{n\thenetimage-#2}{\psframebox{%
  \vbox to 0.6cm{\vfil\hbox to 0.6cm{\hfil\Large #3\hfil}\vfil}}}}%
  \rput#1{\rput[l](0.6,0){\large #4}}}
\def\ut#1:#2:#3:#4;{\rput#1{\rnode{n\thenetimage-#2}{\psframebox{%
  \vbox to 0.6cm{\vfil\hbox to 0.6cm{\hfil\Large #3\hfil}\vfil}}}}%
  \rput#1{\rput[b](0,0.6){\large #4}}}
\def\ub#1:#2:#3:#4;{\rput#1{\rnode{n\thenetimage-#2}{\psframebox{%
  \vbox to 0.6cm{\vfil\hbox to 0.6cm{\hfil\Large #3\hfil}\vfil}}}}%
  \rput#1{\rput[t](0,-0.6){\large #4}}}
\def\ul#1:#2:#3:#4;{\rput#1{\rnode{n\thenetimage-#2}{\psframebox{%
  \vbox to 0.6cm{\vfil\hbox to 0.6cm{\hfil\Large #3\hfil}\vfil}}}}%
  \rput#1{\rput[r](-0.6,0){\large #4}}}
\def\ur#1:#2:#3:#4;{\rput#1{\rnode{n\thenetimage-#2}{\psframebox{%
  \vbox to 0.6cm{\vfil\hbox to 0.6cm{\hfil\Large #3\hfil}\vfil}}}}%
  \rput#1{\rput[l](0.6,0){\large #4}}}
\def\a#1->#2;{\ncline{->}{n\thenetimage-#1}{n\thenetimage-#2}}
\def\aBack#1->#2;{\ncline{-}{n\thenetimage-#1}{n\thenetimage-#2}\ncline[nodesep=0.2]{-<}{n\thenetimage-#1}{n\thenetimage-#2}}
\def\aEarly#1->#2;{\ncline{->}{n\thenetimage-#1}{n\thenetimage-#2}\ncline[nodesep=0.25]{-<}{n\thenetimage-#1}{n\thenetimage-#2}}
\def\aLate#1->#2;{\ncline{->}{n\thenetimage-#1}{n\thenetimage-#2}\ncline[nodesep=0.6]{-<}{n\thenetimage-#1}{n\thenetimage-#2}}
\def\aUndo#1->#2;{\ncline[arrowinset=0]{->}{n\thenetimage-#1}{n\thenetimage-#2}}
\def\aReset#1->#2;{\ncline[arrowinset=0]{->}{n\thenetimage-#1}{n\thenetimage-#2}\ncline[linecolor=white,arrowinset=0,arrowscale=0.6,linestyle=none,nodesep=0.07]{->}{n\thenetimage-#1}{n\thenetimage-#2}}
\let\aFar\aLate
\let\aNear\aEarly
\let\aAck\aReset
\def\A#1->#2;{\ncarc[arcangle=22]{->}{n\thenetimage-#1}{n\thenetimage-#2}}
\def\B#1->#2;{\ncarc[arcangle=-18]{->}{n\thenetimage-#1}{n\thenetimage-#2}}
\def\BB#1->#2;{\ncarc[arcangle=-32]{->}{n\thenetimage-#1}{n\thenetimage-#2}}
\def\avlinearc{0.2}
\def\av#1[#2]-#3->[#4]#5;{
  \SpecialCoor
  \psline[linearc=\avlinearc]{->}([angle=#2]n\thenetimage-#1)#3([angle=#4]n\thenetimage-#5)
}
\def\interface#1:#2:#3:#4;{\rput#1{\rnode{n\thenetimage-#2}{\psframebox*[fillstyle=solid,fillcolor=black]{\vbox to 0.5cm{\vfill\hbox to 0.05cm{}}}}\rput[lt](0,-0.1){#4}}\ncline{-}{n\thenetimage-#2}{n\thenetimage-#3}}
\def\r{n\thenetimage-}

% There must be a better way, but alas it works
\makeatletter
\long\def\petrinet(#1)#2\end{\psscalebox{0.7}{\pspicture(#1)\stepcounter{netimage}#2\endpspicture}\end}
\def\endpetrinet{}
\makeatother

\psset{arrowsize=5pt}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\titlerunning{On Distributability of Petri Nets}
\title{On Distributability of Petri Nets
\texorpdfstring{\newline\normalsize(extended abstract)\thanks{This work was
    partially supported by the DFG (German Research Foundation).}}{}}
\authorrunning{R.J. van Glabbeek, U. Goltz and J.-W. Schicke-Uffmann}

\author{
Rob van Glabbeek \inst{1,2} \and
Ursula Goltz \inst{3} \and
Jens-Wolfhard Schicke-Uffmann \inst{3}
}
\institute{
NICTA, Sydney, Australia
\and
School of Computer Sc.\ and Engineering, University of New South Wales,
Sydney, Australia
\and
Institute for Programming and Reactive Systems, TU Braunschweig, Germany\\[1ex]
 \email{rvg@cs.stanford.edu} \qquad
 \email{goltz@ips.cs.tu-bs.de} \qquad \email{drahflow@gmx.de}
}

\begin{document}
\maketitle

\begin{abstract}
We formalise a general concept of distributed systems as sequential
components interacting asynchronously.  We define a corresponding
class of Petri nets, called LSGA nets, and precisely characterise
those system specifications which can be implemented as LSGA nets up
to branching ST-bisimilarity with explicit divergence.
\end{abstract}

\section{Introduction}
The aim of this paper is to contribute to a fundamental understanding
of the concept of a distributed reactive system and the paradigms of
synchronous and asynchronous interaction. We start by giving an
intuitive characterisation of the basic features of distributed
systems. In particular we assume that distributed systems consist of
components that reside on different locations, and that any signal
from one component to another takes time to travel.  Hence the only
interaction mechanism between components is asynchronous
communication.

Our aim is to characterise which system specifications may be implemented as
distributed systems.  In many formalisms for system specification or design,
synchronous communication is provided as a basic notion; this happens for
example in process algebras.  Hence a particular challenge is that it may be
necessary to simulate synchronous communication by asynchronous communication.
 
Trivially, any system specification may be implemented distributedly by locating
the whole system on one single component. Hence we need to pose some additional
requirements. One option would be to specify locations for system activities and
then to ask for implementations satisfying this distribution and still
preserving the behaviour of the original specification. This is done in
\cite{BCD02}. Here we pursue a different approach. We add another requirement to
our notion of a distributed system, namely that its components only allow
sequential behaviour. We then ask whether an arbitrary system specification may
be implemented as a distributed system consisting of sequential components in an
optimal way, that is without restricting the concurrency of the original
specification. This is a particular challenge when synchronous communication
interacts with concurrency in the specification of the original system. We will
give a precise characterisation of the class of distributable systems, which
answers in particular under which conditions synchronous communication may be
implemented in a distributed setting.  \pagebreak
  
For our investigations we need a model which is expressive enough to represent
concurrency. It is also useful to have an explicit representation of the
distributed state space of a distributed system, showing in particular the local
control states of components. We choose Petri nets, which offer these
possibilities and additionally allow finite representations of infinite
behaviours. We work within the class of \emph{structural conflict nets}
\cite{glabbeek11ipl}\linebreak[3]---a proper generalisation of the class of
one-safe place/transition systems,
where conflict and concurrency are clearly separated.

For comparing the behaviour of systems with their distributed implementation we
need a suitable equivalence notion. Since we think of open systems interacting
with an environment, and since we do not want to restrict concurrency in
applications, we need an equivalence that respects branching time and
concurrency to some degree. Our implementations use transitions which are
invisible to the environment, and this should be reflected in the equivalence
by abstracting from such transitions. However, we do not want implementations to
introduce divergence. In the light of these requirements we work with two
semantic equivalences. \emph{Step readiness equivalence} is one of the
weakest equivalences that captures branching time, concurrency and divergence to some
degree; whereas \emph{branching ST-bisimilarity with explicit divergence}
fully captures branching time, divergence, and those aspects of concurrency that
can be represented by concurrent actions overlapping in time.
We obtain the same characterisation for both notions of equivalence, and thus
implicitly for all notions in between these extremes.

We model distributed systems consisting of sequential components as an
appropriate class of Petri nets, called \emph{LSGA nets}.  These are obtained by
composing nets with sequential behaviour by means of an asynchronous parallel
composition. We show that this class corresponds exactly to a more abstract
notion of distributed systems, formalised as \emph{distributed nets}
\cite{glabbeek08syncasyncinteractionmfcs}.

We then consider distributability of system specifications which are represented
as structural conflict nets. A net $N$ is \emph{distributable} if there exists a
distributed implementation of $N$, that is a distributed net which is
semantically equivalent to $N$.  In the implementation we allow unobservable
transitions, and labellings of transitions, so that single actions of the
original system may be implemented by multiple transitions. However, the system
specifications for which we search distributed implementations are \emph{plain}
nets without these features.

We give a precise characterisation of distributable nets in terms of a
semi-structural property.  This characterisation provides a formal proof that
the interplay between choice and synchronous communication is a key issue for
distributability.

\section{Basic Notions}
\label{basic}

We consider here general labelled place/transition nets with arc weights. Arc weights
are not necessary for the results of the paper, but are included for the sake of generality.

We will employ the following notations for multisets.

\begin{definition}\rm\label{df-multiset}
Let $X$ be a set.
\vspace{-1.5ex}
\begin{itemize}
\item A {\em multiset} over $X$ is a function $A\!:X \rightarrow \bbbn$,
  \ie $A\in \powermultiset{X}$.
\item $x \in X$ is an \defitem{element of} a multiset $A\in\nat^X$, notation $x \in
  A$, iff $A(x) > 0$. 
\item For multisets $A$ and $B$ over $X$ we write $A \leq B$ iff
 \mbox{$A(x) \leq B(x)$} for all $x \inp X$;
\pagebreak[3]
\\ $A + B$ denotes the multiset over $X$ with $(A + B)(x):=A(x)+B(x)$,
\\ $A \mathord\setminus B$ denotes the multiset over $X$ with $(A - B)(x):=\max(A(x)-B(x),0)$, and
for $k\inp\nat$ the multiset $k\cdot A$ is given by $(k \cdot A)(x):=k\cdot A(x)$.
\item The function $\emptyset\!:X\rightarrow\nat$, given by
  $\emptyset(x):=0$ for all $x \inp X$, is the \emph{empty} multiset.
\item If $A$ is a multiset over $X$ and $Y\subseteq X$ then
  $A\restrictedto Y$ denotes the multiset over $Y$ defined by
  $(A\restrictedto Y)(x) := A(x)$ for all $x \inp Y$.
\item The cardinality $|A|$ of a multiset $A$ over $X$ is given by
  $|A| := \sum_{x\in X}A(x)$.
\item A multiset $A$ over $X$ is \emph{finite}
  iff $\{x \mid x\inp A\}$ is finite, i.e., iff $|A|<\infty$.
\end{itemize}
\end{definition}
Two multisets $A\!:\!X \mathord\rightarrow \bbbn$ and $B\!:\!Y\mathord\rightarrow \bbbn$
are \emph{extensionally equivalent} iff
$A\restrictedto (X\mathord\setminus Y) \mathord= \emptyset$,
$B \restrictedto (Y\mathord\setminus X) \mathbin= \emptyset$, and
$A\restrictedto (X\cap Y) \mathbin= B\restrictedto (X\cap Y)$.
In this paper we often do not distinguish extensionally equivalent
multisets. This enables us, for instance, to use $A + B$ even
when $A$ and $B$ have different underlying domains.

A multiset $A$ with $A(x) \in\{0,1\}$ for all $x$ is
identified with the set $\{x \mid A(x)=1\}$.

\vspace{-0.4ex}
\begin{definition}\rm\label{df-nst}
  Let \Act{} be a set of \emph{visible actions} and
  $\tau\mathbin{\not\in}\Act$ be an \emph{invisible action}.\\
  A (\emph{labelled}) \defitem{Petri net} (\emph{over \plat{$\Act\dcup\{\tau\}$}}) is a tuple
  $N = (S, T, F, M_0, \ell)$ where
  \begin{itemize}\vspace{-1ex}
    \item $S$ and $T$ are disjoint sets (of \defitem{places} and \defitem{transitions}),
    \item $F: (S \times T \cup T \times S) \rightarrow \bbbn$
      (the \defitem{flow relation} including \defitem{arc weights}),
    \item $M_0 : S \rightarrow \bbbn$ (the \defitem{initial marking}), and
    \item \plat{$\ell: T \into \Act \dcup \{\tau\}$} (the \defitem{labelling function}).
  \end{itemize}
\end{definition}

\noindent
Petri nets are depicted by drawing the places as circles and the
transitions as boxes, containing their label.  Identities of places
and transitions are displayed next to the net element.  When
$F(x,y)>0$ for $x,y \inp S\cup T$ there is an arrow (\defitem{arc})
from $x$ to $y$, labelled with the \emph{arc weight} $F(x,y)$.
Weights 1 are elided.  When a Petri net represents a concurrent
system, a global state of this system is given as a \defitem{marking},
a multiset $M$ of places, depicted by placing $M(s)$ dots
(\defitem{tokens}) in each place $s$.  The initial state is $M_0$.

To compress the graphical notation, we also allow universal
quantifiers of the form $\forall x. \phi(x)$ to appear
in the drawing (cf.~\reffig{conflictrepl}).
A quantifier replaces occurrences of $x$ in element identities
with all concrete values for which $\phi(x)$ holds, possibly
creating a set of elements instead of the depicted single one.
An arc of which only one end is replicated by a given quantifier
results in a fan of arcs, one for each replicated element.
If both ends of an arc are affected by the same quantifier,
an arc is created between pairs of elements corresponding to the same $x$,
but not between elements created due to differing values of $x$.

The behaviour of a Petri net is defined by the possible moves between
markings $M$ and $M'$, which take place when a finite multiset $G$ of
transitions \defitem{fires}.  In that case, each occurrence of a
transition $t$ in $G$ consumes $F(s,t)$ tokens from each 
place $s$.  Naturally, this can happen only if $M$ makes all these
tokens available in the first place.  Next, each $t$ produces $F(t,s)$ tokens
in each $s$.  \refdf{firing} formalises this notion of behaviour.

\begin{definition}\rm\label{df-preset}
Let $N = (S, T, F, M_0, \ell)$ be a Petri net and $x\inp S\cup T$.\\
The multisets $\precond{x},~\postcond{x}: S\cup T \rightarrow
\bbbn$ are given by $\precond{x}(y)=F(y,x)$ and
$\postcond{x}(y)=F(x,y)$ for all $y \inp S \cup T$.
If $x\in T$, the elements of $\precond{x}$ and $\postcond{x}$ are
called \emph{pre-} and \emph{postplaces} of $x$, respectively.
These functions extend to multisets
$X:S \cup T \rightarrow\bbbn$ as usual, by
$\precond{X} := \sum_{x \in S \cup T}X(x)\cdot\precond{x}$ and
$\postcond{X} := \sum_{x \in S \cup T}X(x)\cdot\postcond{x}$.
\vspace{-.21ex}
\end{definition}

\begin{definition}\rm\label{df-firing}
Let $N \mathbin= (S, T, F, M_0, \ell)$ be a Petri net,
$G \inp \bbbn^T\!$, $G$ non-empty and finite, and $M, M' \inp \bbbn^S\!$.
$G$ is a \defitem{step} from $M$ to $M'$,
written \plat{$M~[G\rangle_N~ M'$}, iff
$^\bullet G \subseteq M$ ($G$ is \defitem{enabled}) and
$M' = (M \setminus \mbox{$^\bullet G$}) + G^\bullet$. 
\end{definition}
\vspace{-0.5ex}

\noindent
Note that steps are (finite) multisets, thus allowing self-concurrency,
\ie the same transition can occur multiple times in a single step.

In our nets transitions are labelled with \emph{actions} drawn from a
set \plat{$\Act \dcup \{\tau\}$}.
%This makes it possible to see these
%nets as models of \defitem{reactive systems} that interact with their
%environment.
A transition $t$ can be thought of as the occurrence of
the action $\ell(t)$. If $\ell(t)\inp\Act$, this occurrence can be
observed and influenced by the environment, but if $\ell(t)\mathbin=\tau$,
it cannot and $t$ is an \defitem{internal} or \defitem{silent} transition.
Transitions whose occurrences cannot be distinguished by the
environment carry the same label. In particular, since
the environment cannot observe the occurrence of internal
transitions at all, they are all labelled $\tau$.

To simplify statements about behaviours of nets, we use some abbreviations.
\vspace{-.21ex}

\begin{definition}\em
  Let $N = (S, T, F, M_0, \ell)$ be a Petri net.\vspace{-.5ex}
\\We write $M_1 \production{\alpha}_N M_2$, for $\alpha\in\Act\dcup\{\tau\}$, when $\exists\, t \mathbin\in T
      .~ \alpha \mathbin= \ell(t) \wedge M_1~[\{t\}\rangle_N~ M_2$.
\\
      Furthermore, for $\,a_1 a_2 \cdots a_n \in \Act^*$ we write
      $M_1 \Goesto[\,a_1 a_2 \cdots a_n~]_N M_2$ when\vspace{-4pt}
      \[
      M_1
      \Goesto_N \production{a_1}_N
      \Goesto_N \production{a_2}_N
      \Goesto_N \cdots
      \Goesto_N \production{a_n}_N
      \Goesto_N
      M_2\vspace{-4pt}
      \]
      where $\Goesto_N$ denotes the reflexive and
      transitive closure of $\production{\tau}_N$.

  \noindent
  For \plat{$\alpha\in\Act\dcup\{\tau\}$}, we write $M_1
  \goesto[\opt{\alpha}]_N M_2$ for $M_1 \goesto[\alpha]_N M_2
  \vee (\alpha=\tau \wedge M_1=M_2)$, meaning that in case
  $\alpha=\tau$ performing a $\tau$-transition is optional.
  We write $M_1 \goesto[\alpha]_N$ for $\exists M_2. M_1
  \production{\alpha}_N M_2$, and $M_1 \arrownot\production{\alpha}_N$ for $\nexists M_2. M_1
  \production{\alpha}_N M_2$.
  Likewise $M_1 [G\rangle_N$ abbreviates $\exists M_2. M_1 [G\rangle_N M_2$.
%
  We omit the subscript $N$ if clear from context.
\vspace{-.21ex}
\end{definition}

\begin{definition}\rm\label{df-onesafe}
  Let $N = (S, T, F, M_0, \ell)$ be a Petri net.
\begin{itemize}\vspace{-1ex}
\item
  A marking $M \in \bbbn^S$ is said to be \defitem{reachable in $N$} iff there is a
  $\sigma \in \Act^*$ such that $M_0 \Production{\sigma}_N M$. The set of all
  \defitem{reachable markings of $N$} is denoted by $[M_0\rangle_N$.
\item
  $N$ is \defitem{one-safe}
  iff $M \in [M_0\rangle_N \implies \forall x \in S.\, M(x) \leq 1$.
\item
  The \defitem{concurrency relation} $\mathord{\concurrent} \subseteq
  T^2$ is given by $t \concurrent u \equivalent \exists
  M \inp [M_0\rangle.\, M [\{t,u\}\rangle$.
\item
  $N$ is a \defitem{structural conflict net} iff
  for all $t,u\in T$ with $t\smile u$ we have $\precond{t} \cap \precond{u} = \emptyset$.
\end{itemize}
\end{definition}
We use the term \defitem{plain nets} for Petri nets where $\ell$ is
injective and no transition has the label $\tau$, \ie essentially
unlabelled nets. 

This paper first of all aims at studying finite Petri nets: nets with finitely many places
and transitions. However, our work also applies to infinite nets with the properties that
$\precond{t} \ne \varnothing$ for all transitions $t\in T$, and
any reachable marking (a) is finite, and (b) enables only finitely many transitions.
Henceforth, we call such nets \emph{finitary}. Finitariness can be ensured by requiring
$|M_0| \mathbin< \infty \wedge \forall t \in T.\, \precond{t} \ne \varnothing \wedge
\forall x \in S\cup T.\, |\postcond{x}| < \infty$.

We use the following variant of readiness semantics \cite{OH86} to
compare behaviour.
\vspace{-.21ex}

\begin{definition}\rm\label{df-readypair}
  {Let $N = (S, T, F, M_0, \ell)$ be a Petri net, $\sigma \in \Act^*$ and
  $X \subseteq \powermultiset{\Act}$.}\\
  $\rpair{\sigma, X}$ is a \defitem{step ready pair} of $N$ iff\vspace{-3pt}
  $$\exists M. M_0 \Production{\sigma} M \wedge M \arrownot\production{\tau}
  \wedge \, X = \{\ell(G) \mid M [G\rangle\}.$$\\[-3ex]
  Here we extend the labelling function $\ell$ to finite multisets of transitions elementwise.\\
  We write $\readyset(N)$ for the set of all step ready pairs of $N$.\\
  Two Petri nets $N_1$ and $N_2$ are \defitem{step readiness equivalent},
  $N_1 \mathbin{\approx_\mathscr{R}} N_2$, iff $\readyset(N_1) \mathbin= \readyset(N_2)$.
\end{definition}

\noindent
\emph{ST-bisimilarity} was proposed in \cite{GV87} as a non-interleaved version of
bisimilarity that respects causality to the extent that it can be expressed in terms of
the possibility of durational actions to overlap in time. It was extended to a setting
with internal actions in \cite{Vo93}, based on the notion of \emph{weak bisimilarity} of \cite{Mi89}.
Here we apply the same idea, but based on \emph{branching bisimilarity} \cite{GW96}, which
unlike weak bisimilarity fully respects the branching structure of related systems.

An \emph{ST-marking} of a net $N\mathbin=(S,T,F,M_0,\ell)$ is a pair $(M,U)\inp\nat^S \mathord\times T^*$
of a normal marking, together with a sequence of transitions \emph{currently firing}.
The \emph{initial} ST-marking is $\mathfrak{M_0}:=(M_0,\varepsilon)$.
The elements of $\Act^\pm:=\{a^+,\, a^{-n} \mid a \inp \Act, ~n\mathbin> 0\}$ are called
\emph{visible action phases}, and \plat{$Act^\pm_\tau:=\Act^\pm\dcup\{\tau\}$}.
For $U\in T^*$, we write $t\in^{(n)}U$ if $t$ is the  \plat{$n^{\it th}$}
element of $U$. Furthermore $U^{-n}$ denotes $U$ after removal of the \plat{$n^{\it th}$}
transition.

\begin{definition}\rm
Let $N=(S,T,F,M_0,\ell)$ be a Petri net, labelled over \plat{$\Act\dcup\{\tau\}$}.

The \emph{ST-transition relations} $\goesto[\eta]$ for $\eta\inp\Act^\pm_\tau$ between ST-markings are given by\vspace{1pt}

$(M,U)\goesto[a^+](M',U')$ iff $\exists t\inp T.~ \ell(t)=a \wedge M[\{t\}\rangle
\wedge M'=M-\precond{t} \wedge U'=U t$.

$(M,U)\goesto[a^{-n}](M',U')$ iff $\exists t\in^{(n)} U.~\ell(t)=a \wedge
 U'=U^{-n} \wedge M'=M+\postcond{t}$.

$(M,U)\goesto[\tau](M',U')$ iff $M\goesto[\tau]M' \wedge U'=U$.
\end{definition}
Now \emph{branching ST-bisimilarity} is \emph{branching bisimilarity} \cite{GW96},
applied to the labelled transition system made up of ST-markings of nets and the
ST-transitions between them.

\begin{definition}\rm
Two Petri nets $N_1$ and $N_2$ are \emph{branching ST-bisimilar} iff there exists a
relation $\mathcal{R}$ between the ST-markings of $N_1$ and $N_2$
%---an \emph{branching ST-bisimulation}---
such that, for all $\eta\inp\Act^\pm_\tau$:\vspace{-1.5ex}
\begin{enumerate}
\item $\mathfrak{M_0}_1\mathcal{R}\mathfrak{M_0}_2$;
\item if $\mathfrak{M}_1\mathcal{R}\mathfrak{M}_2$ and
  $\mathfrak{M}_1\goesto[\eta]\mathfrak{M}'_1$
  then $\exists \mathfrak{M}^\dagger_2,\mathfrak{M}'_2$ such that\\
  $\mathfrak{M}_2\Goesto[] \mathfrak{M}^\dagger_2 \goesto[\opt{\eta}] \mathfrak{M}'_2$,
  ~$\mathfrak{M}_1\mathcal{R}\mathfrak{M}^\dagger_2$ and $\mathfrak{M}'_1\mathcal{R}\mathfrak{M}'_2$;
% and vice versa:
\item if $\mathfrak{M}_1\mathcal{R}\mathfrak{M}_2$ and
  $\mathfrak{M}_2\goesto[\eta]\mathfrak{M}'_2$
  then $\exists \mathfrak{M}^\dagger_1,\mathfrak{M}'_1$ such that\\
  $\mathfrak{M}_1\Goesto[] \mathfrak{M}^\dagger_1 \goesto[\opt{\eta}] \mathfrak{M}'_1$,
  ~$\mathfrak{M}^\dagger_1\mathcal{R}\mathfrak{M}_2$ and $\mathfrak{M}'_1\mathcal{R}\mathfrak{M}'_2$.
\end{enumerate}
\end{definition}
If a system has the potential to engage in an infinite sequence of internal actions, one
speaks of \emph{divergence}.  Branching bisimilarity \emph{with explicit divergence}
\cite{GW96}, is a variant of branching bisimilarity that fully respects the diverging
behaviour of related systems. Since here we only compare systems of which one admits no
divergence at all, the definition simplifies to the requirement that the other system may
not diverge either. We write $N_1\approx^\Delta_{bSTb}N_2$ iff $N_1$ and $N_2$ are
branching ST-bisimilar with explicit divergence.

\section{Distributed Systems}
\label{distributed systems}
In this section, we stipulate what we understand by a distributed
system, and subsequently formalise a model of distributed systems in
terms of Petri nets.
\begin{itemize}
\vspace{-.5ex}
\item A distributed system consists of components residing on different locations.
\item Components work concurrently.
\item Interactions between components are only possible by explicit communications.
\item Communication between components is time consuming and asynchronous.
\vspace{-.5ex}
\end{itemize}
Asynchronous communication is the
only interaction mechanism in a
distributed system for exchanging signals or information.
\begin{itemize}
\vspace{-.5ex}
\item The sending of a message happens always strictly before its receipt (there is a causal relation between sending and receiving a message).
\item A sending component sends without regarding the state of the
  receiver; in particular there is no need to synchronise with a receiving component.
  After sending the sender continues its behaviour independently of receipt of the message.
\vspace{-.5ex}
\end{itemize}
As explained in the introduction, we will add another requirement to
our notion of a distributed system, namely that its components only
allow sequential behaviour.

Formally, we model distributed systems as nets consisting of component
nets with sequential behaviour and interfaces in terms of input and
output places.

\begin{definition}\rm\label{df-component}
  Let $N \mathbin= (S, T, F, M_0, \ell)$ be a Petri net,
  $I, O \mathbin\subseteq S$,
  $I\mathop\cap O\mathbin=\emptyset$ and
  $\postcond{O} = \varnothing$.\vspace{-1ex}
  \begin{enumerate}
    \item $(N, I, O)$ is a \defitem{component with interface $(I, O)$}.
    \item $(N, I, O)$ is a \defitem{sequential} component with interface $(I,
      O)$ iff $\exists Q \mathbin\subseteq S \mathord\setminus (I \cup O)$ with
      $\forall t \in T. |\precond{t} \restrictedto Q| = 1 \wedge
          |\postcond{t}\! \restrictedto Q| = 1$ and
        $|M_0 \restrictedto Q| = 1$.
  \end{enumerate}
\end{definition}
An input place $i\inp I$ of a component $\mathcal{C}$ can be regarded as a mailbox of
$\mathcal{C}$ for a specific type of messages.  An output place $o\inp
O$, on the other hand, is an address outside $\mathcal{C}$ to which $\mathcal{C}$
can send messages. Moving a token into $o$ is like posting a
letter. The condition $\postcond{o}=\varnothing$ says that a message,
once posted, cannot be retrieved by the component.

A set of places like $Q$ above is called an \emph{$S$-invariant}.
The requirements guarantee that the number of tokens in these places
remains constant, in this case $1$. It follows that no two transitions
can ever fire concurrently (in one step).
Conversely, whenever a net is sequential, in the sense that no two
transitions can fire in one step, it is easily converted into a
behaviourally equivalent net with the required $S$-invariant, namely by
adding a single marked place with a self-loop to all transitions.
This modification preserves virtually all semantic equivalences on
Petri nets from the literature, including $\approx^\Delta_{bSTb}$.

Next we define an operator for combining components with asynchronous
communication by fusing input and output places.

\begin{definition}\rm\label{df-parcomp}
  Let $\indexset$ be an index set.\\
  Let $((S_k, T_k, F_k, {M_0}_k, \ell_k), I_k, O_k)$ with $k \in \indexset$
  be components with interface such that
  $(S_k \cup T_k) \cap (S_l \cup T_l) = (I_k \cup O_k) \cap (I_l \cup O_l)$
  for all $k, l \in \indexset$ with $k\neq l$
  (components are disjoint except for interface places)
  and moreover $I_k \cap I_l = \varnothing$ for all $k, l \in \indexset$ with $k\neq l$
  (mailboxes cannot be shared; the recipient of a message is always unique).

\noindent
  Then the \defitem{asynchronous parallel composition} of
  these components is defined by\vspace{-.5ex}
  \begin{equation*}
  \Big\|_{i \in \indexset} ((S_k, T_k, F_k, {M_0}_k, \ell_k), I_k, O_k) =
    ((S, T, F, {M_0}, \ell), I, O)\vspace{-.5ex}
  \end{equation*}
  with
  $S \mathord= \bigcup_{k \in \indexset} S_k,~
  T \mathord= \bigcup_{k \in \indexset} \!T_k,~
  F \mathord= \bigcup_{k \in \indexset} \!F_k,~
  M_0 \mathord= \sum_{k \in \indexset} \!{M_0}_k,~
  \ell \mathord= \bigcup_{k \in \indexset} \!\ell_k$
  (componentwise union of all nets),
  $I \mathord= \bigcup_{k \in \indexset} I_k$
  (we accept additional inputs from outside), and
  $O \mathord= \bigcup_{k \in \indexset} O_k \setminus \bigcup_{k \in \indexset} I_k$
  (once fused with an input, $o\inp O_I$ is no longer an output).
\end{definition}

\begin{observation}
  $\|$ is associative.
\end{observation}
  This follows directly from the associativity of the (multi)set union
  operator.\qed

\noindent
We are now ready to define the class of nets representing systems 
of asynchronously communicating sequential components.

\begin{definition}\rm\label{df-LSGA}
  $\!$A Petri net $N$ is an \defitem{LSGA net} (a \defitem{locally sequential
  globally asynchronous net}) iff there exists an index set
  $\indexset$ and sequential components with interface
  $\mathcal{C}_k,~ k \inp \indexset$, such that $(N, I, O) = \|_{k \in \indexset} \mathcal{C}_k$
  for some $I$ and $O$.\pagebreak[3]
\end{definition}

\noindent
Up to $\approx^\Delta_{bSTb}$---or any reasonable equivalence
preserving causality and branching time but abstracting from internal
activity---the same class of LSGA systems would have been obtained if
we had imposed, in Def.~\ref{df-component}, that $I$, $O$ and $Q$ form
a partition of $S$ and that $\precond{I}=\emptyset$.
However, it is essential that our definition allows multiple
transitions of a component to read from the same input place.

In the remainder of this section we give a more abstract
characterisation of Petri nets representing distributed systems,
namely as \emph{distributed} Petri nets, which we introduced in
\cite{glabbeek08syncasyncinteractionmfcs}. This will be useful in
Section~\ref{distributable}, where we investigate
distributability using this more semantic characterisation. We show
below that the concrete characterisation of distributed systems as
LSGA nets and this abstract characterisation agree.

Following \cite{BCD02}, to arrive at a class of nets representing distributed systems,
we associate \emph{localities} to the elements of a net $N=(S,T,F,M_0,\ell)$.
We model
this by a function \mbox{$D: S\cup T \rightarrow\Loc$}, with $\Loc$ a
set of possible locations.  We refer to such a
function as a \defitem{distribution} of $N$.  Since the identity of
the locations is irrelevant for our purposes, we can just as well
abstract from $\Loc$ and represent $D$ by the equivalence relation
$\equiv_D$ on $S\cup T$ given by $x \equiv_D y$ iff $D(x)=D(y)$.

Following \cite{glabbeek08syncasyncinteractionmfcs}, we impose a fundamental
restriction on distributions, namely that when two transitions
can occur in one step, they cannot be co-located. This reflects our
assumption that at a given location \visible actions can only occur
sequentially.

In \cite{glabbeek08syncasyncinteractionmfcs} we observed that
Petri nets incorporate a notion of synchronous interaction, in that a
transition can fire only by synchronously taking the tokens from all
of its preplaces. In general the behaviour of a net would change
radically if a transition would take its input tokens one by one---in
particular deadlocks may be introduced. Therefore we insist that in a
distributed Petri net, a transition and all its input places reside on
the same location. There is no reason to require the same for the
output places of a transition, for the behaviour of a net would not
change significantly if transitions were to deposit their output tokens
one by one \cite{glabbeek08syncasyncinteractionmfcs}.

This leads to the following definition of a distributed Petri net.

\begin{definition}[\cite{glabbeek08syncasyncinteractionmfcs}]
  \rm\label{df-distributed}\,
    A Petri net $N = (S, T, F, M_0, \ell)$ is \defitem{distributed}
    iff there exists a distribution $D$ such that
  \begin{list}{{\bf --}}{\leftmargin 25pt
                        \labelwidth\leftmargini\advance\labelwidth-\labelsep
                        \topsep 0pt \itemsep 0pt \parsep 0pt}
    \item[(1)]
      $\forall s \in S, ~t \in T.~\hspace{1pt}s \in \precond{t}
      \implies t \equiv_D s$,
    \item[(2)]
     $\forall t,u\in T.~t \concurrent u \implies t\not\equiv_D u$.
  \end{list}
  $N$ is \emph{essentially distributed} if (2) is weakened to
  $\forall t,u\inp T.~t \concurrent u \wedge \ell(t)\neq\tau \implies t\not\equiv_D u$.
\end{definition}

\noindent
A typical example of a net which is not distributed is shown in
\reffig{fullM} on Page \pageref{fig-fullM}. Transitions $t$ and $v$ are
concurrently executable
and hence should be placed on different locations. However,
both have preplaces in common with $u$ which would enforce putting all
three transitions on the same location. In fact, distributed nets can
be characterised in the following semi-structural way.

\begin{observation}\it\label{distributed}
A Petri net is distributed iff there is no sequence $t_0,\ldots,t_n$ of
transitions with $t_0 \smile t_n$ and
$\precond{t_{i-1}}\cap\precond{t_{i}}\neq\emptyset$ for $i=1,\ldots,n$.\qed
\end{observation}

\noindent
It turns out that the classes of LSGA nets and distributable
nets essentially coincide. Moreover, up to $\approx^\Delta_{bSTb}$
these classes also coincide with the more liberal notion of essentially
distributed nets, permitting concurrency of internal transitions at the same
location. We will make use of that in proving our main theorem.

\begin{theorem}\label{thm-LSGA}
  Any LSGA net is distributed, and for any essentially distributed net $N$ there
  is an LSGA net $N'$ with $N'\approx^\Delta_{bSTb} N$.
\end{theorem}
\begin{proof}
  In the full version of this paper \cite{GGSdistributability}.
\qed
  \pagebreak[3]
\end{proof}

\begin{observation}\it\label{distributed-structuralconflict}
  Every distributed Petri net is a structural conflict net.\qed
  \vspace{-1ex}
\end{observation}

\begin{corollary}\it\label{LSGA-structuralconflict}
  Every LSGA net is a structural conflict net.\qed
\end{corollary}


\section{Distributable Systems}
\label{distributable}

We now consider Petri nets as specifications of concurrent
systems and ask the question which of those specifications can be
implemented as distributed systems. This question can be formalised as
\begin{quote}\em
Which Petri nets are semantically equivalent to distributed nets?
\end{quote}
Of course the answer depends on the choice of a suitable
semantic equivalence. 
Here we will answer this question using the two equivalences introduced in Section \ref{basic}.
We will give a precise characterisation of those nets for which we can find semantically equivalent distributed nets. For the negative part of this characterisation, stating that certain nets are not distributable, we will use step readiness
equivalence, which is one of the simplest and least discriminating
equivalences imaginable that abstracts from internal actions, but
preserves branching time, concurrency and divergence to some small
degree. As explained in \cite{glabbeek08syncasyncinteractionmfcs}, giving
up on any of these latter three properties would make any Petri net
distributable, but in a rather trivial and
unsatisfactory way.
For the positive part, namely that all other nets are indeed distributable, 
we will use the most discriminating equivalence for which our implementation works, namely branching
ST-bisimilarity with explicit divergence, which is finer than
step readiness equivalence. Hence we will obtain the strongest possible results for both directions and it turns out that the concept of distributability is fairly robust w.r.t.\ the choice of
a suitable equivalence: any equivalence notion between step readiness
equivalence and branching ST-bisimilarity with explicit divergence will yield
the same characterisation.

\begin{definition}\rm\label{df-distributable}
  A Petri net $N$ is \defitem{distributable} up to an equivalence
  $\approx$ iff there exists a distributed net $N'$ with $N' \approx N$.
\end{definition}

\noindent
Formally we give our characterisation of distributability by classifying which
finitary plain structural conflict nets can be implemented as distributed nets,
and hence as LSGA nets. In such implementations, we use invisible
transitions. We study the concept ``distributable'' for plain nets only, but in
order to get the largest class possible we allow non-plain implementations,
where a given transition may be split into multiple transitions carrying the
same label.

It is well known that sometimes a global protocol is necessary to implement
synchronous interaction present in system specifications. In
particular, this may be needed for deciding choices in a coherent
way, when these choices require agreement of multiple components.
The simple net in \reffig{fullM} shows a typical situation of this
kind. Inde-\linebreak\pagebreak%
\begin{figure}[h]
\begin{minipage}[b]{0.55\linewidth}\normalsize
pendent decisions of the two choices might lead to a
deadlock. As remarked in \cite{glabbeek08syncasyncinteractionmfcs}, for
this particular net there exists no satisfactory distributed
implementation that fully respects the reactive behaviour of the
original system. Indeed such \structuralM-structures, representing
interference between concurrency and choice, turn out to play a crucial
r\^ole for characterising distributability.
\end{minipage}\hfill
\begin{minipage}[b]{0.38\linewidth}
\vspace{-4ex}
  \begin{center}
    \begin{petrinet}(6,3,4)
      \Q (2,3):p1:$p$;
      \Q (4,3):p2:$q$;
      \u (1,1):t1:$a$:$t$;
      \u (3,1):t2:$b$:$u$;
      \u (5,1):t3:$c$:$v$;

      \a p1->t1;
      \a p1->t2;
      \a p2->t2;
      \a p2->t3;
    \end{petrinet}
  \end{center}
\vspace{-4ex}
  \caption{A fully marked \structuralM.}
  \label{fig-fullM}
\vspace{2ex}
\end{minipage}
\vspace{-5ex}
\end{figure}

\begin{definition}\rm\label{df-fullM}
  Let $N = (S, T, F, M_0, \ell)$ be a Petri net.
  $N$ has a \defitem{fully reachable \visible pure \structuralM} iff
  $\exists t,u,v \in T.
  \precond{t} \cap \precond{u} \ne \varnothing \wedge
  \precond{u} \cap \precond{v} \ne \varnothing \wedge
  \precond{t} \cap \precond{v} = \varnothing \wedge
  \exists M \in [M_0\rangle.
  \precond{t} \cup \precond{u} \cup \precond{v} \subseteq M$.
\end{definition}

\noindent
Note that \refdf{fullM} implies that $t\neq u$, $u\neq v$ and $t\neq v$.

\smallskip

We now give an upper bound on the class of distributable nets by adopting a
result from \cite{glabbeek08syncasyncinteractionmfcs}.

\begin{theorem}\label{thm-trulysyngltfullm}
  Let $N$ be a plain structural conflict Petri net. 
  If $N$ has a fully reachable \visible pure {\structuralM}, then $N$ is
  not distributable up to step readiness equivalence.
\end{theorem}
\begin{proof}
In \cite{glabbeek08syncasyncinteractionmfcs} this theorem was obtained for
plain one-safe nets.\footnote{In \cite{glabbeek08syncasyncinteractionmfcs} the
theorem was claimed and proven only for plain nets with a fully reachable
\emph{visible} pure {\structuralM}; however, for plain nets the
requirement of visibility is irrelevant.} The proof applies verbatim to plain
structural conflict nets as well.
\qed\end{proof}

\noindent
Since $\approx^\Delta_{bSTb}$ is finer than $\approx_\mathscr{R}$,
this result holds also for distributability up to $\approx^\Delta_{bSTb}$
(and any equivalence between $\approx_\mathscr{R}$ and $\approx^\Delta_{bSTb}$).

In the following, we establish that this upper bound is tight, and hence a finitary plain structural conflict net is distributable iff it has no fully reachable \visible
pure \structuralM. For this, it is helpful to first introduce macros in Petri nets for reversibility of transitions.

\subsection{Petri nets with reversible transitions}

A \emph{Petri net with reversible transitions} generalises the notion
of a Petri net; its semantics is given by a translation to an
ordinary Petri net, thereby interpreting the reversible transitions
as syntactic sugar for certain net fragments.  It is defined as a tuple
$(S,T,\UI,\ui,F,M_0,\ell)$ with $S$ a set of places, $T$ a set of (reversible)
transitions, labelled by \plat{$\ell:T\rightarrow\Act\dcup\{\tau\}$}, $\UI$ a set of
\emph{undo interfaces} with the relation $\ui\subseteq \UI\times T$
linking interfaces to transitions, $M_0 \inp \nat^S$ an initial marking, and
$$F\!: (S\times T\times \{{\scriptstyle \it in,~early,~late,~out,~far}\} \rightarrow \nat)$$
the flow relation. For $t\inp T$ and ${\scriptstyle \it type} \in
\{{\scriptstyle \it in,~early,~late,~out,~far}\}$, the multiset of places
$t^{\it type}\inp\nat^S$ is given by $t^{\it type}(s) = F(s,t,{\scriptstyle \it type})$.
When $s\inp t^{\it type}$ for ${\scriptstyle \it type} \in
\{{\scriptstyle \it in,~early,~late}\}$, the place $s$ is called a
\emph{preplace} of $t$ of type {\scriptsize \it type\/};
when $s\inp t^{\it type}$ for ${\scriptstyle \it type} \in
\{{\scriptstyle \it out,~far}\}$, $s$ is called a
\emph{postplace} of $t$ of type {\scriptsize \it type}.
For each undo interface $\omega\inp \UI$ and transition $t$ with $\ui(\omega,t)$ there must be places
$\undo[\omega](t)$, $\reset[\omega](t)$ and $\ack[\omega](t)$ in $S$.
A transition with a nonempty set of interfaces is called \emph{reversible};
the other (\emph{standard}) transitions may have pre- and postplaces
of types {\scriptsize \it in} and {\scriptsize \it out} only---for these
transitions $t^{\it in}\mathbin=\precond{t}$ and $t^{\it out}\mathbin=\postcond{t}$.
In case $\UI=\emptyset$, the net is just a normal Petri net.
\pagebreak

A global state of a Petri net with reversible transitions is given by a marking
\mbox{$M\mathord{\in}\nat^S\!\!$}, together with the state of each reversible transition ``currently
in progress''.  Each transition in the net can fire as usual. A reversible transition can
moreover take back (some of) its output tokens, and be \emph{undone} and
\emph{reset}.  When a transition $t$ fires, it consumes $\sum_{{\scriptstyle \it
type}\in\{{\scriptstyle \it in,~early,~late}\}} F(s,t,{\scriptstyle \it type})$
tokens from each of its preplaces $s$ and produces $\sum_{{\scriptstyle \it
type}\in\{{\scriptstyle \it out,~far}\}} F(s,t,{\scriptstyle \it type})$
tokens in each of its postplaces $s$.  A reversible transition $t$ that has fired
can start its reversal by consuming a token from $\undo[\omega](t)$ for one of
its interfaces $\omega$.  Subsequently, it can
take back one by one a token from its postplaces of type {\scriptsize \it
far}. After it has retrieved all its output of type
{\scriptsize \it far}, the transition is undone, thereby returning
$F(s,t,{\scriptstyle \it early})$ tokens in each of its preplaces $s$ of type
{\scriptsize \it early}.
Afterwards, by
consuming a token from $\reset[\omega](t)$, for the same interface $\omega$ that
started the undo-process, the transition terminates its chain of activities by
returning $F(s,t,{\scriptstyle \it late})$ tokens in each of its {\scriptsize
\it late} preplaces $s$.  At that occasion it also produces a token in
$\ack[\omega](t)$. Alternatively, two tokens in $\undo[\omega](t)$ and
$\reset[\omega](t)$ can annihilate each other without involving the transition
$t$; this also produces a token in $\ack[\omega](t)$. The latter mechanism comes in action
when trying to undo a transition that has not yet fired.

\reffig{reversible} shows the translation of a reversible transition
$t$ with $\ell(t)\mathbin=a$ into a ordinary net fragment.  The
arc weights on the green (or grey) arcs are inherited from the
untranslated net; the other arcs have weight~1.
\begin{figure}[ht]
\vspace{-2ex}
  \begin{center}
    \begin{petrinet}(10,4)
      \qt(3,3):in:$(in)$;
      \qt(1,3):late:$(late)$;
      \qt(7,3):early:$(early)$;
      \q(9,3):undo:$\undo[\omega](t)$;
      \q(9,2):reset:$\reset[\omega](t)$;
      \q(9,1):ack:$\ack[\omega](t)$;
      \ql(1,1):far:$(far)$;
      \qb(5,1):out:$(out)$;
      \ub(4,2):t:$a$:$t$;

      \interface(7,2):ti:t:$\omega$;

      \a in->t;
      \aLate late->t;
      \aEarly early->t;
      \a t->out;
      \aFar t->far;
      \aUndo undo->ti;
      \aReset reset->ti;
      \aAck ti->ack;
    \end{petrinet}
  \end{center}
  \vspace{0.5ex}
  \begin{center}
    \begin{petrinet}(14,8)
      \psset{linecolor=green}
      \ql(1,4):far:$f$;
      \ql(1,7):out:$o$;
      \qt(1,8):in:$i$;
      \qt(5,8):late:$l$;
      \qt(13,8):early:$e$;

      \psset{linecolor=black}
      \qb(4.5,1):take:$\take(f,t)$;
      \ub(7,1):tundop:$\tau$:$t \cdot \undo[](f)$;
      \qb(9.5,1):took:$\took(f,t)$;

      \ub(3,2):tundoa:$\tau$:$t \cdot \undo[\omega]$;
      \ur(11,2):tundone:$\tau$:$t \cdot \undone$;

      \qr(3,4):fired:$\Fired(t)$;
      \ql(11,4):p2:$\rho(t)\!$;

      \ut(3,7):tfire:$a$:$t \cdot \fire$;
      \ut(11,7):treseta:$\tau$:$t \cdot \reset[\omega]$;

      \psset{linecolor=darkred}
      \qr(5.25,3.75):undoa:$\undo[\omega](t)$;
      \qb(8.75,3):pa:$\keep[\omega](t)$;
      \ul(6,5):elidea:$\tau$:$t \cdot \elide[\omega]$;
      \qt(8.75,6):acka:$\ack[\omega](t)$;
      \qb(8.5,5):reseta:$\reset[\omega](t)$;

      {
        \darkblue
        \rput[tr](1,3.5){\large $\forall f \in t^{\,\it far}$}
        \rput[tr](1,6.5){\large $\forall o \in t^{out}$}
        \rput[rb](0.5,8.45){\large $\forall i \in t^{in}$}
        \rput[rb](4.5,8.45){\large $\forall l \in t^{late}$}
        \rput[lb](13.5,8.45){\large $\forall e \in t^{early}$}
        \rput(5,6){\large $\forall \omega. \ui(\omega, t)$}
      }

      \psset{linecolor=black}
      \a tfire->fired;
      \a fired->tundoa;
      \a tundoa->take;
      \a take->tundop;
      \a tundop->took;
      \a took->tundone;
      \a tundone->p2;
      \a p2->treseta;

      \psset{linecolor=green}
      \a in->tfire;
      \a tfire->out;
      \a tfire->far;
      \a far->tundop;
      \a tundone->early;
      \a treseta->late;
      \av early[180]-(8,8)->[15]tfire;
      \a late->tfire;

      \psset{linecolor=darkred}
      \a tundoa->pa;
      \a pa->treseta;
      \a undoa->tundoa;
      \a undoa->elidea;
      \a elidea->acka;
      \a treseta->acka;
      \a reseta->elidea;
      \a reseta->treseta;
    \end{petrinet}
  \end{center}
\vspace{-1ex}
\caption{A reversible transition and its macro expansion.}
\label{fig-reversible}
\end{figure}

\subsection{The conflict replicating implementation}

Now we establish that a finitary plain structural conflict net that has no fully reachable
\visible pure \structuralM\ is distributable.  We do this by proposing the \emph{conflict
replicating implementation} of any such net, and show that this implementation is always
(a) essentially distributed, and (b) equivalent to the original net. In order to get the strongest
possible result, for (b) we use branching ST-bisimilarity with explicit divergence.

\begin{figure}
\vspace{-1em}
  \begin{center}
    \begin{petrinet}(17,26.8)
      {
        \darkblue

        \rput[lb](11,16){\large$\begin{array}{l}\displaystyle
          \forall j \in T'\\
          \forall p \in \precond{j}\\
          \forall h <^\# j\\
          \forall i \leq^\# j\\
          \forall k \geq^\# j\\
          \forall l >^\# j\\
          \forall q \in \precond{i}\\
          \forall c \in \postcond{q}\\
          \forall r \in \postcond{i\,}\\
          \forall t \in \UIij := \begin{array}[t]{@{}l@{}}
          \{\ini[c]\mid c\confeq i\} +\mbox{}\\ \{\trans[b]{c} \mid b <^\# c \confeq i\}
          \end{array}
        \end{array}$}
      }

      {
        \darkred

        \rput[r](4.75,21){$F(p,j)$}
        \rput[r](4.85,1.6){$F(i,r)$}
        \rput[b](4,8.65){$F(q,i)$}
      }

      \ql(5,26):p:$p$;
      \ul(5,24):distributep:$\tau$:$\dist$;
      \qx(5,22):pj:$p_j$:(-0.45,-0.45);
      \qr(8,19):prejk:$\Pre^j_k$;
      \Qr(7,21):readyinitialisej:$\pi_j$;
      \ul(5,20):initialisej:$\tau$:$\ini$;
      \qr(5,18):transin:$\transin{j}$;
      \Ql(3,16):pconh:$\pi_{h\#j}$;
      \ur(5,16):trans:$\tau$:$\trans{j}$;
      \qr(5,14):transout:$\transout{j}$;
      \ql(3,14):prehj:$\Pre^i_j$;
      \Qt(7,12):pconj:$\pi_{j\#l}$;
      \ul(5,12):executehj:\makebox[0pt]{$\ell(i)$}:;
      \rput[l](5.2,11.3){\large $\exec{j}$}
      \qb(1,10):undohjt:$\undo(t)$;
      \ql(5,10):fetchphjin:$\fetchin[q,c]$;
      \ql(3,8.5):pbackbottom:$q_c$;
      \ur(5,8.5):fetchphj:$\tau$:$\fetch[q,c]$;
      \ql(5,7):fetchphjout:$\fetchout[q,c]$;
      \ul(5,5.5):fetchedhj:$\tau$:$\fetched{j}$;
      \qr(7,4):ackhjt:$\ack(t)$;
      \ql(3,4):resethjt:$\reset(t)$;
      \ul(5,2.5):completehj:$\tau$:$\comp{j}$;
      \ql(5,1):r:$r$;

      \a p->distributep;
      \aBack pbacktop->distributep;
      \a distributep->pj;
      \aEarly pj->initialisej;
      \aLate readyinitialisej->initialisej;
      \aFar initialisej->prejk;
      \aFar initialisej->transin;
      \aEarly transin->trans;
      \aLate pconh->trans;
      \aFar trans->transout;
      \B prehj->executehj;
      \B executehj->prehj;
      \A transout->executehj;
      \A executehj->transout;
      \a pconj->executehj;
      \a executehj->undohjt;
      \a executehj->fetchphjin;
      \a fetchphjin->fetchphj;
      \a pbackbottom->fetchphj;
      \a fetchphj->fetchphjout;
      \a fetchphjout->fetchedhj;
      \a fetchedhj->resethjt;
      \a ackhjt->completehj;
      \a completehj->r;
      \BB fetchedhj->pconj;
    \end{petrinet}
  \end{center}
  \vspace{-2ex}
  \caption{The conflict replicating implementation}
  \label{fig-conflictrepl}\vspace{-1pt}
\end{figure}

To define the conflict replicating implementation of a net $N=(S,T,F,M_0,\ell)$
we fix an arbitrary well-ordering $<$ on its transitions. We let
$b,c,h,i,j,k,l$ range over these ordered transitions, and write\vspace{-1ex}
\begin{itemize}
\item $i\mathbin\#j$ iff $i\mathord{\neq}j \wedge 
  \precond{i} \cap \precond{j} \mathbin{\ne} \varnothing$
  ~(transitions $i$ and $j$ are \emph{in conflict}),
  ~and $i \confeq j$ iff ~$i\# j \vee i\mathbin=j$,
\item $i <^\#\! j$ iff ~$i<j \wedge i\mathbin{\#} j$,
  ~and $i \leqc j$ iff ~$i <^\#\! j \vee i=j$.\vspace{-1ex}
\end{itemize}
\reffig{conflictrepl} shows the conflict replicating implementation $N$.  It is presented
as a Petri net $\impl{N}=(S',T',F',\UI,\ui,M'_0,\ell')$ with reversible transitions.  The set
$\UI$ of undo interfaces (not drawn) is $T$, and for $i\inp \UI$ we
have $\ui(i,t)$ iff $t\inp \UIij$, where the sets of transitions
\plat{$\UI_i\inp\nat^{T'}$} are specified in \reffig{conflictrepl}. The implementation $\impl{N}$
inherits the places of $N$ (\ie $S'\supseteq S$), and we postulate that
$M'_0\mathord\upharpoonright S = M_0$.  Given this, \reffig{conflictrepl} is not merely an
illustration of $\impl{N}$---it provides a complete and accurate description of it, thereby
defining the conflict replicating implementation of any net. In interpreting this figure
it is important to realise that net elements are completely determined by their name
(identity), and exist only once, even if they show up multiple times in the figure. For
instance, the place $\pi_{h\#j}$ with $h\mathord=2$ and $j\mathord=5$ (when using
natural numbers for the transitions in $T$) is the same as the place \plat{$\pi_{j\#l}$}
with $j\mathord=2$ and $l\mathord=5$; it is a standard preplace of \plat{$\exec{2}$} (for
all $i\leqc 2$), a standard postplace of $\fetched{2}$, as well as a late preplace of \plat{$\trans[2]{5}$}.

The r\^ole of the transitions $\dist$ for $p\inp S$ is to distribute a
token in $p$ to copies $p_j$ of $p$ in the localities of all
transitions $j\inp T$ with $p\inp \precond{j}$.  In case $j$ is
enabled in $N$, the transition $\ini$ will become enabled in $\impl{N}$.
These transitions put tokens in the places \plat{$\Pre^j_k$}, which
are preconditions for all transitions \plat{$\exec[j]{k}$}, which
model the execution of $j$ at the location of $k$.  When two
conflicting transitions $h$ and $j$ are both enabled in $N$, the first
steps $\ini[h]$ and $\ini$ towards their execution in $\impl{N}$ can happen
in parallel. To prevent them from executing both, \plat{$\exec[j]{j}$}
(of $j$ at its own location) is only possible after \plat{$\trans{j}$},
which disables $\exec[h]{h}$.

The main idea behind the conflict replicating implementation is that
a transition $h\inp T$ is primarily executed by a sequential component of
its own, but when a conflicting transition $j$ gets enabled, the
sequential component implementing $j$ may ``steal'' the possibility to
execute $h$ from the home component of $h$, and keep the options to do
$h$ and $j$ open until one of them occurs. To prevent $h$ and $j$ from
stealing each other's initiative, which would result in deadlock, a
global asymmetry is built in by ordering the transitions.
Transition $j$ can steal the initiative from $h$ only when $h<j$.

In case $j$ is also in conflict with a transition $l$, with $j<l$,
the initiative to perform $j$ may subsequently be stolen by $l$.
In that case either $h$ and $l$ are in conflict too---then $l$ takes
responsibility for the execution of $h$ as well---or $h$ and $l$ are
concurrent---in that case $h$ will not be enabled, due to the absence
of fully reachable pure \structuralM s in $N$.
The absence of fully reachable pure \structuralM s also guarantees that it
cannot happen that two concurrent transitions $j$ and $k$ both
steal the initiative from an enabled transition $h$.

After the firing of $\exec{j}$ all tokens that were left behind in the process of
carefully orchestrating this firing will have to be cleaned up, to prepare the
net for the next activity in the same neighbourhood. This is the reason for
the reversibility of the transitions preparing the firing of \plat{$\exec{j}$}.
Hence there is an undo interface for each transition $i\inp T'$, cleaning up the mess made in
preparation of firing \plat{$\exec{j}$} for some $j$.\linebreak[3] $\UIij$
is the multiset of all transitions $t$ that could possibly have
contributed to this. For each of them its interface $i$ is activated, by
\plat{$\exec{j}$} depositing a token in $\undo(t)$. When all preparatory transitions that
have fired are undone, tokens appear in the places $p_c$ for all
$p\mathop{\in}\precond{i}$ and $c\inp\postcond{p}$.
These are collected by $\fetch$, after which all $t\inp\UIij$ get a reset signal.
Those that have fired and were undone are reset, and those that never fired perform $\elide(t)$.
In either case a token appears in $\ack(t)$. These are collected by $\comp{j}$, which
finishes the execution of $i$ by depositing tokens in its postplaces.

\begin{proposition}\it\label{obs-cri-distributed}
  $\impl{N}$ is essentially distributed for every Petri net $N$.
\end{proposition}
\textit{Proof sketch.\/}
  We take the \emph{canonical} distribution $D$ of $N$, in which $\equiv_D$ is the
  equivalence relation on places and transitions \emph{generated} by Condition (1) of \refdf{distributed}.
  We need to show that $D$ satisfies the weakened Condition 2.
  Any location that harbours an external transition \plat{$\exec{j}$}
  for some $i\mathbin\leq j\inp T'$, also harbours
  \plat{$\ini\mathord\cdot\und[\Pre^i_j]$}, \plat{$\trans{j}\mathord\cdot\und[\transout{j}]$}
  for all $h\mathbin{<^\#} j$, \plat{$\exec{j}$} for all $i\leqc j$,
  and, for all $l>^\# j$, $\trans[j]{l}\mathord\cdot\fire$ and $\ini[l]\mathord\cdot\und[\mbox{$\transin[j]{l}$}]$.
  In \cite{GGSdistributability} we show that none of
  these transitions can happen concurrently with $\exec{j}$.
\hfill\rule{1.2ex}{1.2ex}

\begin{theorem}\label{thm-fullmgttrulysync}
  Let $N$ be a finitary plain structural conflict net
  without a fully reachable \visible pure \structuralM.
  Then $N$ is distributable up to $\approx^\Delta_{bSTb}$.
\end{theorem}
\begin{proof}
  In the full version of this paper \cite{GGSdistributability}.
  There we show that $\impl{N} \approx^\Delta_{bSTb} N$.
  Hence $\impl{N}$ is a essentially distributed implementation of $N$. 
  Now apply \refthm{LSGA}.
\qed
\end{proof}
Given the complexity of our construction, no techniques known to us were adequate for
performing this proof. We therefore had to develop an entirely new method for
rigorously proving the equivalence of two Petri nets up to $\approx^\Delta_{bSTb}$, one of
which known to be plain. This method is presented in \cite{GGSdistributability}.

\begin{corollary}\label{cor-fullmeqtrulysync}
  Let $N$ be a finitary  plain structural conflict net.
  Then $N$ is distributable iff it has no fully reachable
  \visible pure~\structuralM. \qed
\end{corollary}

\section{Conclusion}

In this paper, we have given a precise characterisation of
distributable Petri nets in terms of a semi-structural property. Moreover, we
have shown that our notion of distributability corresponds to an
intuitive notion of a distributed system by establishing that any
distributable net may be implemented as a network of asynchronously
communicating components.

In order to formalise what qualifies as a valid implementation, we
needed a suitable equivalence relation. We have chosen step readiness
equivalence for showing the impossibility part of our
characterisation, since it is one of the simplest and least
discriminating semantic equivalences imaginable that
abstracts from internal actions but preserves branching time,
concurrency and divergence to some small degree. For the positive
part, stating that all other nets are implementable, we have
introduced a combination of several well known rather discriminating
equivalences, namely a divergence sensitive version of branching
bisimulation adapted to ST-semantics.  Hence our characterisation is
rather robust against the chosen equivalence; it holds in fact for all
equivalences between these two notions.  However, ST-equivalence (and
our version of it) preserves the causal structure between action
occurrences only as far as it can be expressed in terms of the
possibility of durational actions to overlap in time. Hence a natural
question is whether we could have chosen an even stronger causality
sensitive equivalence for our implementability result, respecting
e.g.\ pomset equivalence or history preserving\linebreak bisimulation.  Our
conflict replicating implementation does not fully preserve the causal
behaviour of nets; we are convinced we have chosen the strongest
possible equivalence for which our implementation works.  It is an
open problem to find a class of nets that can be implemented
distributedly while preserving divergence, branching time and
causality in full.
%
Another line of research is to investigate which Petri nets can be implemented as distributed nets when relaxing the requirement of preserving the branching structure.
If we allow linear time correct implementations (using a step trace
equivalence), we conjecture that all Petri nets become distributable.
However, also in this case it is problematic, in fact even impossible in our setting, to
preserve the causal structure, as has been shown in \cite{EPTCS64.9}.
A similar impossibility result has been obtained in the world of the $\pi$-calculus in
\cite{EPTCS64.7}.
\advance\textheight 1pt

\advance\textheight -1pt The interplay between choice and synchronous communication has
already been investigated in quite a number of approaches in different frameworks. We
refer to \cite{glabbeek08syncasyncinteractionmfcs} for a rather comprehensive overview and
concentrate here on recent and closely related work.

The idea of modelling asynchronously communicating sequential components by sequential
Petri nets interacting though buffer places has already been considered in
\cite{reisig82buffersync}. There Wolfgang Reisig introduces a class of systems, represented
as Petri nets, where the relative speeds of different components are guaranteed to be
irrelevant.  His class is a strict subset of our LSGA nets, requiring additionally,
amongst others, that all choices in sequential components are free, \ie do not depend upon
the existence of buffer tokens, and that places are output buffers of only one component.
%
Another quite similar approach was taken in \cite{EHH10}, where
transition labels are classified as being either input or output.
There, asynchrony is introduced by adding new buffer places during
net composition.
This framework does not allow multiple senders for a single receiver.

Other notions of distributed and distributable Petri nets are proposed in
\cite{hopkins91distnets,BCD02,BD11}. In these works, given a distribution of the
transitions of a net, the net is distributable iff it can be implemented by a net that is
distributed w.r.t.\ that distribution. The requirement that concurrent transitions may not
be co-located is absent; given the fixed distribution, there is no need for such a
requirement. These papers differ from each other, and from ours, in what counts as a valid
implementation. A comparison of our criterion with that of Hopkins
\cite{hopkins91distnets} is provided in \cite{glabbeek08syncasyncinteractionmfcs}.

In \cite{glabbeek08syncasyncinteractionmfcs} we have obtained a characterisation similar to
Corollary~\ref{cor-fullmeqtrulysync}, but for a much more restricted notion of distributed
implementation (\emph{plain distributability}), disallowing nontrivial transition
labellings in distributed implementations.  We also proved that fully reachable pure
\structuralM s are not implementable in a distributed way, even when using transition
labels (\refthm{trulysyngltfullm}). However, we were not able to show that this upper
bound on the class of distributable systems was tight.  Our current work implies the
validity of Conjecture 1 of \cite{glabbeek08syncasyncinteractionmfcs}.
While in \cite{glabbeek08syncasyncinteractionmfcs} we considered only one-safe
place/transition systems, the present paper employs a more general class of
place/transition systems, namely structural conflict nets. This enables us to give a
concrete characterisation of distributed nets as systems of sequential components
interacting via non-safe buffer places.

%\bibliographystyle{eptcs}
%\bibliography{../our/petri}
\begin{thebibliography}{10}
\providecommand{\bibitemdeclare}[2]{}
\providecommand{\urlprefix}{Available at }
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\href}[2]{\texttt{#2}}
\providecommand{\urlalt}[2]{\href{#1}{#2}}
\providecommand{\doi}[1]{doi:\urlalt{http://dx.doi.org/#1}{#1}}
\providecommand{\bibinfo}[2]{#2}

\bibitemdeclare{article}{BCD02}
\bibitem{BCD02}
\bibinfo{author}{E.~Badouel}, \bibinfo{author}{B.~Caillaud} \&
  \bibinfo{author}{P.~Darondeau} (\bibinfo{year}{2002}):
  \emph{\bibinfo{title}{Distributing Finite Automata Through Petri Net
  Synthesis}}.
\newblock {\sl \bibinfo{journal}{Formal Aspects of Computing}}
  \bibinfo{volume}{13}(\bibinfo{number}{6}),
  pp. \bibinfo{pages}{447--470}.
%,  \doi{10.1007/s001650200022}.

\bibitemdeclare{inproceedings}{BD11}
\bibitem{BD11}
\bibinfo{author}{E.~Best} \& \bibinfo{author}{Ph. Darondeau}
  (\bibinfo{year}{2011}): \emph{\bibinfo{title}{Petri Net Distributability}}.
\newblock In: {\sl \bibinfo{booktitle}{Proceedings Ershov Informatics
  Conference (PSI'11), Novosibirsk, Russia}}, \bibinfo{series}{\rm LNCS},
  \bibinfo{publisher}{Springer}.
\newblock \bibinfo{note}{To appear}.

\bibitemdeclare{inproceedings}{EHH10}
\bibitem{EHH10}
\bibinfo{author}{D.~El{~}Hog{-}Benzina}, \bibinfo{author}{S.~Haddad} \&
  \bibinfo{author}{R.~Hennicker} (\bibinfo{year}{2010}):
  \emph{\bibinfo{title}{Process Refinement and Asynchronous Composition with
  Modalities}}.
\newblock In \bibinfo{editor}{N.~Sidorova} \& \bibinfo{editor}{A.~Serebrenik},
  editors: {\sl \bibinfo{booktitle}{{\rm {P}roceedings of the 2nd
  {I}nternational {W}orkshop on} {A}bstractions for {P}etri {N}ets and {O}ther
  {M}odels of {C}oncurrency {\rm ({APNOC}'10)}}}, \bibinfo{address}{Braga,
  Portugal}.
\newblock
  \urlprefix\url{http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EHH-apnoc10.pdf}.

\bibitemdeclare{article}{glabbeek11ipl}
\bibitem{glabbeek11ipl}
\bibinfo{author}{R.J. van Glabbeek}, \bibinfo{author}{U.~Goltz} \&
  \bibinfo{author}{J.-W. Schicke} (\bibinfo{year}{2011}):
  \emph{\bibinfo{title}{Abstract Processes of Place/Transition Systems}}.
\newblock {\sl \bibinfo{journal}{Information Processing Letters}}
  \bibinfo{volume}{111}(\bibinfo{number}{13}), pp. \bibinfo{pages}{626 -- 633},
  \doi{10.1016/j.ipl.2011.03.013}.

\bibitemdeclare{inproceedings}{glabbeek08syncasyncinteractionmfcs}
\bibitem{glabbeek08syncasyncinteractionmfcs}
\bibinfo{author}{R.J.~van Glabbeek}, \bibinfo{author}{U.~Goltz} \&
  \bibinfo{author}{J.-W. Schicke} (\bibinfo{year}{2008}):
  \emph{\bibinfo{title}{{On} Synchronous and Asynchronous Interaction in
  Distributed Systems}}.
\newblock In \bibinfo{editor}{E.~Ochma\'nski} \&
  \bibinfo{editor}{J.~Tyszkiewicz}, editors: {\sl
  \bibinfo{booktitle}{Mathematical Foundations of Computer Science 2008}}, {\sl
  \bibinfo{series}{\rm LNCS}} \bibinfo{volume}{5162},
  \bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{16--35},
  \doi{10.1007/978-3-540-85238-4\_2}.
\newblock \bibinfo{note}{Full version available as Technical Report 2008-03,
  TU-Braunschweig; \url{http://arxiv.org/abs/0901.0048}}.

\bibitemdeclare{techreport}{GGSdistributability}
\bibitem{GGSdistributability}
\bibinfo{author}{R.J.~van Glabbeek}, \bibinfo{author}{Goltz U} \&
  \bibinfo{author}{J.-W. Schicke-Uffmann} (\bibinfo{year}{2011}):
  \emph{\bibinfo{title}{On Distributability of Petri Nets}}.
\newblock \bibinfo{type}{Technical Report} \bibinfo{number}{2011-10},
  \bibinfo{institution}{TU Braunschweig}.
\newblock \urlprefix\url{http://theory.stanford.edu/~rvg/abstracts.html#95}.
\newblock \bibinfo{note}{Full version of this paper, to appear}.

\bibitemdeclare{inproceedings}{GV87}
\bibitem{GV87}
\bibinfo{author}{R.J.~van Glabbeek} \& \bibinfo{author}{F.W. Vaandrager}
  (\bibinfo{year}{1987}): \emph{\bibinfo{title}{Petri net models for algebraic
  theories of concurrency (extended abstract)}}.
\newblock In: {\sl \bibinfo{booktitle}{{\rm Proc.} PARLE '87}}, {\sl
  \bibinfo{series}{\rm LNCS}} \bibinfo{volume}{259},
  \bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{224--242}.
%,  \doi{10.1007/3-540-17945-3\_13}.
%\newblock \urlprefix\url{http://kilby.stanford.edu/~rvg/pub/petri.pdf}.

\bibitemdeclare{article}{GW96}
\bibitem{GW96}
\bibinfo{author}{R.J.~van Glabbeek} \& \bibinfo{author}{W.P. Weijland}
  (\bibinfo{year}{1996}): \emph{\bibinfo{title}{Branching Time and Abstraction
  in Bisimulation Semantics}}.
\newblock {\sl \bibinfo{journal}{Journal of the ACM}}
  \bibinfo{volume}{43}(\bibinfo{number}{3}), pp. \bibinfo{pages}{555--600},
  \doi{10.1145/233551.233556}.

\bibitemdeclare{inproceedings}{hopkins91distnets}
\bibitem{hopkins91distnets}
\bibinfo{author}{R.P. Hopkins} (\bibinfo{year}{1991}):
  \emph{\bibinfo{title}{Distributable nets}}.
\newblock In: {\sl \bibinfo{booktitle}{Advances in {P}etri Nets 1991}}, {\sl
  \bibinfo{series}{\rm LNCS}} \bibinfo{volume}{524},
  \bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{161--187},
  \doi{10.1007/BFb0019974}.

\bibitemdeclare{book}{Mi89}
\bibitem{Mi89}
\bibinfo{author}{R.~Milner} (\bibinfo{year}{1989}):
  \emph{\bibinfo{title}{Communication and Concurrency}}.
\newblock \bibinfo{publisher}{Prentice Hall}, \bibinfo{address}{Englewood
  Cliffs}.

\bibitemdeclare{article}{OH86}
\bibitem{OH86}
\bibinfo{author}{E.-R. Olderog} \& \bibinfo{author}{C.A.R. Hoare}
  (\bibinfo{year}{1986}): \emph{\bibinfo{title}{Specification-oriented
  semantics for communicating processes}}.
\newblock {\sl \bibinfo{journal}{Acta Informatica}} \bibinfo{volume}{23}, pp.
  \bibinfo{pages}{9--66}, \doi{10.1007/BF00268075}.

\bibitemdeclare{inproceedings}{EPTCS64.7}
\bibitem{EPTCS64.7}
\bibinfo{author}{K.~Peters}, \bibinfo{author}{J.-W. Schicke} \&
  \bibinfo{author}{U.~Nestmann} (\bibinfo{year}{2011}):
  \emph{\bibinfo{title}{Synchrony vs Causality in the Asynchronous
  Pi-Calculus}}.
\newblock In \bibinfo{editor}{B.~Luttik} \& \bibinfo{editor}{F.~Valencia},
  editors: {\sl \bibinfo{booktitle}{{\rm Proceedings 18th International
  Workshop on} Expressiveness in Concurrency, {\rm Aachen, Germany, 5th
  September 2011}}}, {\sl \bibinfo{series}{Electronic Proceedings in
  Theoretical Computer Science}}~\bibinfo{volume}{64}, pp.
  \bibinfo{pages}{89--103}, \doi{10.4204/EPTCS.64.7}.

\bibitemdeclare{article}{reisig82buffersync}
\bibitem{reisig82buffersync}
\bibinfo{author}{W.~Reisig} (\bibinfo{year}{1982}):
  \emph{\bibinfo{title}{Deterministic Buffer Synchronization of Sequential
  Processes}}.
\newblock {\sl \bibinfo{journal}{Acta Informatica}} \bibinfo{volume}{18}, pp.
  \bibinfo{pages}{115--134}, \doi{10.1007/BF00264434}.

\bibitemdeclare{inproceedings}{EPTCS64.9}
\bibitem{EPTCS64.9}
\bibinfo{author}{J.-W. Schicke}, \bibinfo{author}{K.~Peters} \&
  \bibinfo{author}{U.~Goltz} (\bibinfo{year}{2011}):
  \emph{\bibinfo{title}{Synchrony vs. Causality in Asynchronous Petri Nets}}.
\newblock In \bibinfo{editor}{B.~Luttik} \& \bibinfo{editor}{F.~Valencia},
  editors: {\sl \bibinfo{booktitle}{{\rm Proceedings 18th International
  Workshop on} Expressiveness in Concurrency, {\rm Aachen, Germany, 5th
  September 2011}}}, {\sl \bibinfo{series}{Electronic Proceedings in
  Theoretical Computer Science}}~\bibinfo{volume}{64}, pp.
  \bibinfo{pages}{119--131}, \doi{10.4204/EPTCS.64.9}.

\bibitemdeclare{article}{Vo93}
\bibitem{Vo93}
\bibinfo{author}{W.~Vogler} (\bibinfo{year}{1993}):
  \emph{\bibinfo{title}{Bisimulation and Action Refinement}}.
\newblock {\sl \bibinfo{journal}{Theor. Comput. Sci.}}
  \bibinfo{volume}{114}(\bibinfo{number}{1}), pp. \bibinfo{pages}{173--200},
  \doi{10.1016/0304-3975(93)90157-O}.

\end{thebibliography}

\end{document}
