\documentclass{entcs}
\headheight 10pt
\headsep 20pt
\footskip 20pt
\setlength{\topmargin}{-30pt}
\bibliographystyle{entcs/entcs}
\unitlength 1mm

\volume{Express 2004}
\def\firstheadline{~\hfill~}
\def\firstfootline{\hspace{-2.43333pt}\vbox{\footnotesize\rm
    \vspace{.1in}In {\sl Electronic Notes in Theoretical Computer
    Science} 128(2), April 2005: Proceedings of the 11th International
    Workshop on {\sl Expressiveness in Concurrency}, EXPRESS 2004, pp.~5--34.}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% THE NEXT LINES GIVE DEFINITIONS FOR THE THEOREM ENVIRONMENTS.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newenvironment{theorem}{\vspace{-\lastskip}\par\addvspace{.6pc plus
    .2pc minus .1pc}\begin{thm}}{\end{thm}\par\addvspace{.6pc plus
    .2pc minus .1pc}} \newenvironment{lemma}{\vspace{-\lastskip}\par
  \addvspace{.6pc plus .2pc minus .1pc}\begin{lem}}
  {\end{lem}\par\addvspace{.6pc plus .2pc minus .1pc}}
\newenvironment{proposition}{\vspace{-\lastskip}\par \addvspace{.6pc
    plus .2pc minus .1pc}\begin{prop}}{\end{prop}\par\addvspace{.6pc
    plus .2pc minus .1pc}}
\newenvironment{definition}{\vspace{-\lastskip}\par \addvspace{.6pc
    plus .2pc minus
    .1pc}\begin{defn}\rm}{\end{defn}\par\addvspace{.6pc plus .2pc
    minus .1pc}}
\newenvironment{proof}{\begin{pf}}{\qed\end{pf}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\dl}[1]{\mbox{\rm I\hspace{-0.75mm}#1}}	% openface letter
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}}	% no vertical space
\newfont{\fsc}{eusm10 scaled 1200}                      % frenchscript letters
\newcommand{\multi}{\mbox{\fsc M}}                      % french M (multisets)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%				Abbreviations			          %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\IN}{\dl{N}}			    % natural numbers
\newcommand{\eA}{{\rm A}}			    % automaton
\newcommand{\eB}{{\rm B}}			    % automaton
\newcommand{\eG}{{\rm G}}			    % 1-dim. automaton (graph)
\newcommand{\eN}{{\rm N}}			    % Petri net
\newcommand{\fA}{{\cal A}}			    % function into \IA
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}
\begin{frontmatter}
  \title{\bf{\large On the Expressiveness of}\\ Higher Dimensional
    Automata\\ \small (extended abstract)}
  \author{~~~R.J. van Glabbeek\thanksref{EPSRC}\thanksref{myemail}}
  \address{\footnotesize National ICT Australia\\
and School of Computer Science and Engineering\\
The University of New South Wales\\
Locked Bag 6016, Sydney, NSW 1466, Australia}
  \thanks[EPSRC]{This work was supported by EPSRC under grant number GR/S22097}
  \thanks[myemail]{Email:
  \href{mailto:rvg@cs.stanford.edu}{\texttt{\normalshape rvg@cs.stanford.edu}}}
\begin{abstract} 
  In this paper I compare the expressive power of several models of
  concurrency based on their ability to represent causal dependence.
  To this end, I translate these models, in behaviour preserving ways,
  into the model of higher dimensional automata, which is the most
  expressive model under investigation.  In particular, I propose four
  different translations of Petri nets, corresponding to the four
  different computational interpretations of nets found in the
  literature.
  
  \noindent
  I also extend various equivalence relations for concurrent systems
  to higher dimensional automata. These include the history preserving
  bisimulation, which is the coarsest equivalence that fully respects
  branching time, causality and their interplay, as well as the
  ST-bisimulation, a branching time respecting equivalence that takes
  causality into account to the extent that it is expressible by
  actions overlapping in time. Through their embeddings in higher
  dimensional automata, it is now well-defined whether members of
  different models of concurrency are equivalent.
\\[1em]\noindent
  {\it Keywords:\/}
  Concurrency, expressiveness, causality, higher dimensional automata,
  Petri nets, event structures, history preserving bisimulation,
  ST-bisimulation.
\end{abstract}
\end{frontmatter}
\addtolength{\textheight}{25pt} 

\section{A hierarchy of concurrency models}

\begin{figure}[t]
\begin{center}
\begin{picture}(0,80)(0,0)
\put(0,0){\makebox[0pt]{\textit{synchronisation trees} \cite{Mi80}}}
\put(0,3.5){\vector(0,1){10}}
\put(-1,15){\makebox[0pt]{\textit{prime event structures} \cite{Wi87a,Wi89}}}
\put(30,16){\vector(1,0){3}}
\put(30,16){\vector(-1,0){3}}
\put(51,15){\makebox[0pt]{$\left\{
        \mbox{\begin{tabular}{@{}l@{}}\textit{bundle e.s.} \cite{Lk92}\\[-3mm]
                          \textit{flow e.s.} \cite{Bo90}\\[-3mm]
                          \textit{stable e.s.}	\cite{Wi87a,Wi89}\\[-3mm]
                          \textit{safe Petri nets}\end{tabular}}\right.$}} 
\put(0,18.5){\vector(0,1){10}}
\put(0,33.5){\vector(0,1){10}}
\put(0,30){\makebox[0pt]{\textit{Winskel's event structures} \cite{Wi87a,Wi89}}}
\put(46,45){\makebox[0pt]{\textit{pure Petri nets}}}
\put(28,46){\vector(-1,0){3.5}}
\put(28,46){\vector(1,0){3}}
\put(-1.7,45){\makebox[0pt]{\textit{configuration structures} \cite{GP95}}}
\put(-3.5,48.5){\vector(-1,1){10}}
\put(-15,60){\makebox[0pt]{\textit{automata} \cite{vG96h}}}
\put(3.5,48.5){\vector(1,1){10}}
\put(15,60){\makebox[0pt]{\textit{Petri nets}}}
\put(-11.5,63.5){\vector(1,1){10}}
\put(11.5,63.5){\vector(-1,1){10}}
\put(0,75){\makebox[0pt]{\textit{higher dimensional automata} \cite{vG91}}}
\end{picture}
\end{center}
\caption{A hierarchy of concurrency models, ordered by expressive
  power up to history preserving bisimulation}
\label{hierarchy}
\end{figure}

\noindent
Figure~\ref{hierarchy} lists the main models of concurrency proposed
in the literature, ordered by expressive power. Of all models, the
labelled variant is understood. Here I only treat models of processes
that perform actions $a$, $b$, $c$, \ldots whose internal structure is
not further examined, and real-time and stochastic aspects of
processes are completely ignored. Furthermore, I only study the
representation of \emph{processes}, not the representation of
\emph{operators} on processes. I restrict myself to models that take
branching time fully into account, and hence skip models that
represent processes by the sets of their executions. Thus, the
expressive power of the models differs only to the extent that certain
forms of causal dependence are expressible.  I limit myself to models
that take a fully \emph{asynchronous} view on parallelism: whenever a
number of actions can happen simultaneously, this must be because they
are causally independent, and hence they can also happen in any
order. Because of this, I do not include Petri nets with inhibitor
arcs, or Chu spaces \cite{Chu}.

There is an arrow from model $A$ to model $B$ in
Figure~\ref{hierarchy} iff there exists a translation from processes
representable in model $A$ to processes representable in model $B$
that fully respects branching time, causality, and their interplay.
Thus a process and its translation ought to be \emph{history
preserving bisimulation equivalent} \cite{RT88,GG01}.  

Part of the contribution of this paper is a definition of what this
means. Forms of history preserving bisimulation were defined on
behaviour structures in \cite{RT88}, on stable event structures in
\cite{GG01}, and on Petri nets under the individual token
interpretation in \cite{BDKP91}; however, it has never been formally
defined what it means for an event structure, for instance, to be
history preserving bisimulation equivalent to a Petri net.

In Section~\ref{sec-hda} I introduce the model of higher dimensional
automata. Then, in Sections~\ref{sec-automata},~\ref{sec-event}
and~\ref{sec-Petri}, I define behaviour preserving translations from
the other models of Figure~\ref{hierarchy} into this model; for the
model of Petri nets I do this in four different ways, corresponding to
the four different computational interpretations of nets found in the
literature. In Section~\ref{sec-bisimulation} I define history
preserving bisimulation equivalence on higher dimensional
automata. The embeddings of the other models of concurrency into
higher dimensional automata make this definition apply to processes
representable in any of these models: two processes are equivalent iff
their representations as higher dimensional automata are. Naturally, I
have to ensure that the new definition agrees with the existing ones
on the models where it has already been defined. Demonstrating this is
deferred to the full version of this paper.

With this tool in hand, the hierarchy of Figure~\ref{hierarchy} is
justified in Section~\ref{counterexamples}. In particular,
counterexamples will be presented to illustrate the strictness of the
expressiveness ordering.

Besides history preserving bisimulation equivalence, I also define
\emph{interleaving bisimulation equivalence} \cite{Mi80,GG01} on
higher dimensional automata, and thus on the other models, as well as
\emph{ST-bisimulation equivalence} \cite{GV87}, a branching time
respecting semantic equivalence that takes causality into account to
the extent that it can be expressed by the possibility of durational
actions to overlap in time.  If I compare the models merely up to
{interleaving bisimulation equivalence} they turn out to be all
equally expressive.  If I compare them up to {ST-bisimulation
equivalence}, I conjecture that just two equivalence classes of models
remain: the models that do not take causality into account---{\sl in
Figure~\ref{hierarchy} just the model of synchronisation trees}---and
the models that do---{\sl in Figure~\ref{hierarchy} all other models}.
It follows that the more interesting hierarchy of
Figure~\ref{hierarchy} is due to causal subtleties that evaporate when
considering processes up to ST-bisimulation equivalence.

\section{Higher Dimensional Automata}\label{sec-hda}

One of the most commonly used models of concurrency is that of
\emph{automata}, also known as \emph{process graphs}, \emph{state
transition diagrams} or \emph{labelled transition systems}.  In
ordinary automata, the parallel composition P of two actions $a$ and
$b$ is displayed in the same way as a system M that executes $a$ and
$b$ in either order, ending in the same state each way, such that $a$
and $b$ are mutually exclusive (see Figure~\ref{parallelism}). Nevertheless,
it is often important to tell these systems apart. This happens for
instance when $a$ and $b$ take time: the total running time of M is at
least the sum of the running times of $a$ and $b$, whereas P may be as
quick as the maximum of the running times of $a$ and $b$.
Another occasion where it is essential to distinguish between P and
M is when designing systems using \emph{action refinement}, as
described in \cite{GG01}. In many other models of concurrency P and M
are represented distinctly. For the model of Petri nets, this is
illustrated in Figure~\ref{parallelism}.

\begin{figure}[htb]
%\input{mutex}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \graphtemp=.5ex\advance\graphtemp by 0.089in
    \rlap{\kern 0.000in\lower\graphtemp\hbox to 0pt{\hss P:\hss}}%
    \special{pn 8}%
    \special{ar 250 89 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.089in
    \rlap{\kern 0.250in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 250 179}%
    \special{pa 250 357}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 275 321}%
    \special{pa 250 357}%
    \special{pa 225 321}%
    \special{pa 275 321}%
    \special{fp}%
    \special{pa 161 536}%
    \special{pa 339 536}%
    \special{pa 339 357}%
    \special{pa 161 357}%
    \special{pa 161 536}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 0.250in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{pa 250 536}%
    \special{pa 250 714}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 275 679}%
    \special{pa 250 714}%
    \special{pa 225 679}%
    \special{pa 275 679}%
    \special{fp}%
    \special{ar 250 804 89 89 0 6.28319}%
    \special{ar 607 89 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.089in
    \rlap{\kern 0.607in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 607 179}%
    \special{pa 607 357}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 632 321}%
    \special{pa 607 357}%
    \special{pa 582 321}%
    \special{pa 632 321}%
    \special{fp}%
    \special{pa 518 536}%
    \special{pa 696 536}%
    \special{pa 696 357}%
    \special{pa 518 357}%
    \special{pa 518 536}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 0.607in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{pa 607 536}%
    \special{pa 607 714}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 632 679}%
    \special{pa 607 714}%
    \special{pa 582 679}%
    \special{pa 632 679}%
    \special{fp}%
    \special{ar 607 804 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.089in
    \rlap{\kern 2.714in\lower\graphtemp\hbox to 0pt{\hss M:\hss}}%
    \special{ar 2964 89 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.089in
    \rlap{\kern 2.964in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 2964 179}%
    \special{pa 2964 357}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2989 321}%
    \special{pa 2964 357}%
    \special{pa 2939 321}%
    \special{pa 2989 321}%
    \special{fp}%
    \special{pa 2875 536}%
    \special{pa 3054 536}%
    \special{pa 3054 357}%
    \special{pa 2875 357}%
    \special{pa 2875 536}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 2.964in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{pa 2964 536}%
    \special{pa 2964 714}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2989 679}%
    \special{pa 2964 714}%
    \special{pa 2939 679}%
    \special{pa 2989 679}%
    \special{fp}%
    \special{ar 2964 804 89 89 0 6.28319}%
    \special{ar 3321 446 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 3.321in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{ar 3143 468 143 143 -2.250941 -0.636548}%
    \special{sh 1.000}%
    \special{pa 3257 340}%
    \special{pa 3258 383}%
    \special{pa 3217 369}%
    \special{pa 3257 340}%
    \special{fp}%
    \special{ar 3143 425 143 143 0.636548 2.250941}%
    \special{sh 1.000}%
    \special{pa 3066 578}%
    \special{pa 3054 536}%
    \special{pa 3097 539}%
    \special{pa 3066 578}%
    \special{fp}%
    \special{ar 3679 89 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.089in
    \rlap{\kern 3.679in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 3679 179}%
    \special{pa 3679 357}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3704 321}%
    \special{pa 3679 357}%
    \special{pa 3654 321}%
    \special{pa 3704 321}%
    \special{fp}%
    \special{pa 3589 536}%
    \special{pa 3768 536}%
    \special{pa 3768 357}%
    \special{pa 3589 357}%
    \special{pa 3589 536}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 3.679in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{pa 3679 536}%
    \special{pa 3679 714}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3704 679}%
    \special{pa 3679 714}%
    \special{pa 3654 679}%
    \special{pa 3704 679}%
    \special{fp}%
    \special{ar 3679 804 89 89 0 6.28319}%
    \special{ar 3499 468 143 143 -2.505044 -0.890651}%
    \special{sh 1.000}%
    \special{pa 3426 369}%
    \special{pa 3385 383}%
    \special{pa 3386 340}%
    \special{pa 3426 369}%
    \special{fp}%
    \special{ar 3499 425 143 143 0.890651 2.505044}%
    \special{sh 1.000}%
    \special{pa 3546 539}%
    \special{pa 3589 536}%
    \special{pa 3577 578}%
    \special{pa 3546 539}%
    \special{fp}%
    \hbox{\vrule depth0.893in width0pt height 0pt}%
    \kern 3.768in
  }%
}%
\centerline{\raise 1em\box\graph}\vspace{-2.4cm}
\begin{center}
\begin{picture}(20,23.5)(-7,10)
\put(0,33.5){\vector(0,-1){3}}
\put(0,30){\circle{1}}
\put(-.35,29.65){\vector(-1,-1){9.3}}
\put(-8,25){$a$}
\put(-10,20){\circle{1}}
\put(-9.65,19.65){\vector(1,-1){9.3}}
\put(-8,13){$b$}
\put(0,10){\circle{1}}
\put(0.35,29.65){\vector(1,-1){9.3}}
\put(6,25){$b$}
\put(10,20){\circle{1}}
\put(9.65,19.65){\vector(-1,-1){9.3}}
\put(6,13){$a$}
\end{picture}
\end{center}
\caption{The automaton in the middle represents both
{\em parallelism}, as does the Petri net P, and
{\em mutual exclusion}, as does the Petri net M.}
\label{parallelism}
\end{figure}

Throughout the years, people have wondered whether the elegance of
automata could be combined with the expressiveness of models like
Petri nets or event structures, that are able to capture causal
relationships between action occurrences.  These relationships include
the causal independence of $a$ and $b$ in P, the dependence of $b$ on
$a$ in the left branch of the automaton representing M, and the
dependence of $a$ on $b$ in the right branch. As a result, several
models of concurrency have been proposed that are essentially
automata, upgraded with some extra structure to express causal
independence \cite{Sh85,Bz87,RT88,Sta89,WN95}.

In \cite{vG88a} it was pointed out that ordinary automata, without
such extra structure, are already sufficiently expressive to capture
these causal relationships.  All that is needed is a reading of
automata that assumes squares to represent concurrency, and
nonconfluent branching to represent a choice or conflict. Under this
\emph{concurrent interpretation} the automaton of
Figure~\ref{parallelism} represents parallelism only, whereas mutual
exclusion is represented by the automaton of Figure~\ref{choice}.
\begin{figure}[htb]
\begin{center}
\begin{minipage}{2.5in}
\begin{center}
\begin{picture}(20,23.5)(50,10)
\put(60,33.5){\vector(0,-1){3}}
\put(60,30){\circle{1}}
\put(59.65,29.65){\vector(-1,-1){9.3}}
\put(52,25){$a$}
\put(50,20){\circle{1}}
\put(50,19.5){\vector(0,-1){9}}
\put(51,14){$b$}
\put(50,10){\circle{1}}
\put(60.35,29.65){\vector(1,-1){9.3}}
\put(66,25){$b$}
\put(70,20){\circle{1}}
\put(70,19.5){\vector(0,-1){9}}
\put(67,14){$a$}
\put(70,10){\circle{1}}
\end{picture}
\end{center}
\caption{Representation of mutual exclusion in ordinary automata under the
  concurrent interpretation }
\label{choice}
\end{minipage}
\hfill
\begin{minipage}{2.5in}
%\input{travel}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \special{pn 4}%
    \special{ar 515 172 25 25 0 6.28319}%
    \special{pa 515 0}%
    \special{pa 515 147}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 539 74}%
    \special{pa 515 147}%
    \special{pa 490 74}%
    \special{pa 539 74}%
    \special{fp}%
    \special{ar 1005 662 25 25 0 6.28319}%
    \special{pa 532 189}%
    \special{pa 988 644}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 953 575}%
    \special{pa 988 644}%
    \special{pa 918 610}%
    \special{pa 953 575}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.417in
    \rlap{\kern 0.760in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{ar 25 662 25 25 0 6.28319}%
    \special{pa 497 189}%
    \special{pa 42 644}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 111 610}%
    \special{pa 42 644}%
    \special{pa 77 575}%
    \special{pa 111 610}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.417in
    \rlap{\kern 0.270in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{ar 515 1152 25 25 0 6.28319}%
    \special{pa 988 679}%
    \special{pa 532 1135}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 601 1100}%
    \special{pa 532 1135}%
    \special{pa 567 1065}%
    \special{pa 601 1100}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.907in
    \rlap{\kern 0.760in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{pa 42 679}%
    \special{pa 497 1135}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 463 1065}%
    \special{pa 497 1135}%
    \special{pa 428 1100}%
    \special{pa 463 1065}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.907in
    \rlap{\kern 0.270in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{pn 14}%
    \special{pa 515 196}%
    \special{pa 515 319}%
    \special{pa 221 662}%
    \special{pa 613 1005}%
    \special{pa 528 1132}%
    \special{sp}%
    \special{pa 634 1084}%
    \special{pa 528 1132}%
    \special{pa 532 1016}%
    \special{fp}%
    \hbox{\vrule depth1.176in width0pt height 0pt}%
    \kern 1.029in
  }%
}%
\centerline{\box\graph}\vspace{1ex}
\caption{Travelling through the inside of a square}
\label{inside}
\end{minipage}
\end{center}
\end{figure}
The square of Figure~\ref{parallelism} is now seen as the
\emph{product} of the transitions $a$ and $b$ that form its sides.  As
each of these two transitions has 3 cells, a \emph{start node}, an
\emph{end node}, and the \emph{edge} between them, their product has 9
cells, namely the 4 nodes and 4 edges displayed in
Figure~\ref{parallelism}, and the \emph{inside of the square}. The
latter represents the concurrent execution of $a$ and $b$.

Modelling concurrency by means of squares (or cubes, hypercubes etc.\
in case of three or more concurrent actions) is particularly useful
when actions are thought to have a duration or structure. A concurrent
execution of $a$ and $b$ in the process $a \| b$ can then be thought
of as a continuous path through the surface of the square, starting at
the top and terminating at the bottom node, while being nondecreasing
when projected on any edge. The execution displayed in
Figure~\ref{inside} for instance passes through a point in which 50\%
of $a$ and about 17\% of $b$ has happened. As long as we want to
identify all such paths (when abstracting from timing information and
structural knowledge of $a$ and $b$) we simply represent their
equivalence class as the square.  In \cite{GV97} this representation
of concurrent systems turned out to be essential in finding and
explaining an essential counterexample in the study of semantic
equivalences.

The price to pay for this simple solution is that it is no longer
possible to represent the system M of Figure~\ref{parallelism} in such
a way that both executions $ab$ and $ba$ end up in the same state.  In
order to overcome this deficiency, and to distinguish \emph{choice},
as displayed in Figure~\ref{choice}, from \emph{mutual exclusion}, as
in M in Figure~\ref{parallelism}, Vaughan Pratt \cite{Pr91a} preferred
for every square, cube, hypercube etc.\ to indicate explicitly whether
it represents concurrency or not.  An $n$-dimensional hypercube that
represents the concurrent execution of the $n$ transitions that span
its sides is thought of as being ``filled in'', which is represented
by an additional $n$-dimensional cell in the automaton. Those that
represent mutual exclusion stay empty. This gives rise to what he
baptised \emph{higher dimensional automata}.

A totally sequential implementation of a system, in which no two
actions happen in parallel, can be represented by an ordinary
automaton, which is a higher dimensional automaton in which there are
no higher dimensional cells, so no squares are filled in.  At the
other side of the spectrum, the very same ordinary automata under the
concurrent interpretation of \cite{vG88a} form the special case of
higher dimensional automata in which \emph{every} (nondegenerate)
square, cube or hypercube is filled in. In between, Pratt's higher
dimensional automata can model systems that feature both parallelism
and mutual exclusion, without having to resort to untying the join of
two branches that surround an area of mutual exclusion.

The idea of higher dimensional automata above had to some extent been
contemplated before in \cite{Sh85} and applied in \cite{Pap86}.
However, \cite{Pr91a} offered the first formalisation of the idea.
Pratt's formalisation, based on $n$-categories, takes a
\emph{globular} or \emph{hemispherical} approach, in which an $n$-cell
has only two boundaries of dimension $n-1$. Desperate attempts by me
to fully grok the globular approach led to an exchange with Pratt in
December 1990 that gave rise to the joint conclusion that a \emph{cubical
approach}, in which an $n$-cell has $2n$ boundaries of dimension
$n-1$, would be preferable (and easier to understand). A \emph{higher
dimensional automaton} (HDA) was henceforth defined as a presheaf over
$\Box$, the category of \emph{cubical complexes}.%
\footnote{The objects of $\Box$ are the symbols 0,1,2,... denoting the
hypercubes of each dimension, and its morphisms from $k$ to $n$
are the embeddings of the $k$-dimensional hypercube as a $k$-dimensional
face of the $n$-dimensional hypercube. All dimensions are directed and
the morphisms preserve this direction. Thus, there are for example 6
morphisms from 2 to 3, corresponding to the fact that a cube has 6
sides.  A \emph{presheaf} over a category \textbf{C} is a functor
$F:\textbf{C}^{\rm op}\rightarrow \textbf{Set}$. Thus a presheaf $F$
over $\Box$ associates a set $F(n)$ to every object $n$ in
$\Box$. $F(n)$ is thought of as the set of $n$-dimensional hypercubes in
the HDA. Also, for every morphism $m:k\rightarrow n$, recognising the
$k$-dimensional hypercube as a face of the $n$-dimensional one, there
exists a function $F(m):F(n) \rightarrow F(k)$, giving for every
$n$-dimensional hypercube its $k$-dimensional face on the side
indicated by $m$. These functions must satisfy exactly those
composition laws that hold for the morphisms in $\Box$. The
advantage of the categorical approach is that the concept of a HDA is
thus completely defined without the need for figuring out these laws.}
%
At the occasion of proposing notions of \emph{bisimulation
equivalence}, {\em homotopy} and \emph{unfolding} for higher
dimensional automata in \cite{vG91}, I reworded this definition in
set-theoretical terms as follows.
\vspace{1em}\hrule

\begin{definition}\label{hda}
A \emph{cubical set} consists of a family of sets $(Q_n)_{n\geq 0}$
and for every $n\!\in\!\IN$ a family of maps $s_i,t_i:Q_n \rightarrow
Q_{n-1}$ for $1\leq i \leq n$, such that
\begin{center}
\mbox{}\hfill$\alpha_i\circ\beta_j = \beta_{j-1}\circ\alpha_i$\hfill
for all $1\leq i<j\leq n$ and $\alpha,\beta \in\{s,t\}$.\hfill(*)
\end{center}
A \emph{higher dimensional automaton}, labelled over an alphabet $A$, is a
tuple $(Q, s, t, I, F, l)$ with $(Q,s,t)$ a cubical set, $I\in Q_0$,
$F\subseteq Q_0$ and $l:Q_1\rightarrow A$, such that
$l(s_i(q))=l(t_i(q))$ for all $q\in Q_2$ and $i=1,2$.
\end{definition}

\noindent
The elements of $Q_0$ are called \emph{nodes} and those of $Q_1$,
$Q_2$ and $Q_3$ are \emph{edges}, \emph{squares} and \emph{cubes},
respectively. In general, the elements of $Q_n$ are called
\emph{$n$-dimensional hypercubes}, or \emph{$n$-cells}. An n-dimensional
hypercube represents a state of a concurrent system in which $n$
transitions are firing concurrently. Because the dimensions of the
hypercube are numbered $1,\dots,n$, these $n$ transitions are {\it de
facto} stored as a list.

An edge $q$ connects 2 nodes: its \emph{source} $s_1(q)$ and its
\emph{target} $t_1(q)$. Likewise, an $n$-dimensional hypercube $q$ has
$n$ sources $s_i(q)$ and $n$ targets $t_i(q)$, one in each dimension
$i=1,...,n$, and each being an $(n-1)$-dimensional hypercube.
The source $s_i(q)$ represents the possible state prior to $q$ in which
$n-1$ out of $n$ transitions are already firing, but the $i^{th}$ one
has not yet started. Likewise, $t_i(q)$ represents the possible state
past $q$ in which $n-1$ out of $n$ transitions are still firing, but
the $i^{th}$ one has terminated.

When removing the $i^{th}$ transition out of a list of $n$ transitions, an
implicit renumbering takes place, and what was formerly the $j^{th}$
transition, for $j>i$, is now called the $(j-1)^{th}$ transition.
Hence, first leaving out the $j^{th}$ and then the $i^{th}$, with
$i<j$, leaves us with the same list as first removing the $i^{th}$
and then the $(j-1)^{th}$ transition. This is the content of the
\emph{cubical laws} (*).

$I$ is the initial state, and $F$ the set of final states of the represented
system. These states are required to have dimension 0, meaning that no
transition is currently firing. An edge $q\in Q_1$ represents a state
where exactly 1 transition is firing, and $l$ indicates the label of
that transition. It is required that opposite sides of a square have
the same label. This because they represent the same transition,
scheduled before and after the firing of another one. The labelling
function can trivially be extended to a labelling of arbitrary
$n$-dimensional hypercubes by lists of $n$ actions
(cf.~Section~\ref{labelling}).
\vspace{1ex}\hrule\vspace{1em}\noindent
Based on this definition, and the computational motivation of Pratt
\cite{Pr91a}, numerous papers on higher dimensional automata have
emerged [\hyperlink{bibliography}{31--64}].\nocite{}

A semantics of CCS in terms of higher dimensional automata is provided
in Goubault \& Jensen \cite{GJ92}, and also studied by Lanzmann
\cite{Lan93}.  In Goubault~\cite{Gou93}, higher dimensional automata
are used as a semantic domain for richer languages, and to compute
local invariants which can decide a few computational properties of
interest.  Cridlig \& Goubault \cite{CG93} provide a semantics of
Linda in terms of higher dimensional automata.  Applications of higher
dimensional automata to scheduling problems and wait-free protocols
for distributed systems are studied by Goubault
\cite{Gou95a,Gou95b,Gou96b}, and model checking applications by
Cridlig~\cite{Cri95,Cri96}.  Algorithms for deadlock detection in
terms of higher dimensional automata appear in Fajstrup et
al.~\cite{FGR98,Faj00}.  Takayama~\cite{Tak95,Tak96a,Tak96b} studies
parallelisation algorithms by means of higher dimensional automata.
Extensions of higher dimensional automata with time are investigated
by Goubault~\cite{Gou95a,Gou96a}.

In Goubault \cite{Gou02} the relations between 1-dimensional automata,
asynchronous transition systems \cite{Sh85,Bz87}, and higher dimensional
automata are cast in a categorical framework, following the work of
Winskel \& Nielsen \cite{WN95}.
To this end it appears to be fruitful to equip the cubical sets of
Definition~\ref{hda} with degeneracy mappings, so that they become
exactly the cubical sets studied before in algebraic topology \cite{Ser51}.

Homotopy for higher dimensional automata is defined in Pratt
\cite{Pr91a} and Van Glabbeek \cite{vG91}, and further investigated by
Goubault \cite{Gou95a} and Raussen \cite{Rau00}. Gunawardena
\cite{Gun94} uses homotopy theory to show that 2-phase locking is
safe.  Goubault \& Raussen \cite{GR02} show, using homotopy theory,
how geometric models of concurrency like higher dimensional automata
are suitable for attacking the state-explosion problem.

Homology theories for higher dimensional automata are proposed by
Gou\-bault and Gaucher [\hyperlink{cite.GJ92}{54},%
\hyperlink{cite.Gou95a}{48},\hyperlink{cite.Gau00b}{39--46}].
\nocite{GJ92,Gou95a,Gau00a,Gau00b,Gau01,Gau02a,Gau02b,Gau03a,GG03,Gau03b}%
Gaucher \nocite{Gau00a,Gau00b,Gau01,Gau02a,Gau02b,Gau03a}%
[\hyperlink{cite.Gau00b}{39--44}], like Pratt~\cite{Pr91a}, takes a
globular approach to higher dimensional automata, and relates it to
the cubical approach. Variations and generalisations of this approach
are studied by Gaucher \& Goubault \cite{GG03,Gau03b}.

Buckland et al.~\cite{Buc96,BJV02} study a simplified version of
globular higher dimensional automata, and equip it with process
algebraic operations.
A generalisation of higher dimensional automata suitable for modelling
continuous rather than discrete processes has been proposed by
Sokolowsky~\cite{Sok02}.

In Cattani \& Sassone \cite{CS96} a simplified form of higher
dimensional automata is proposed, called \emph{higher dimensional
transition systems}. The simplification is payed for in expressive
power though: not all higher dimensional automata that arise as the
image of a Petri net under the self-concurrent collective token
interpretation (see Section~\ref{sec-Petri}) exist as higher
dimensional transition systems.

In \cite{Pr00a,Pr02a}, Pratt argues that acyclic higher dimensional
automata can be seen as subsets of a single infinite dimensional cube,
which in turn can be modelled as Chu spaces over 3.

An overview of work related to higher dimensional automata and the use
of other geometric methods in computer science is presented in
Goubault~\cite{Gou00}.

\section{Embedding ordinary automata in HDA}
\label{sec-automata}

A (1-dimensional) automaton is a tuple $(Q_0, Q_1, s_1, t_1, I, F, l)$,
the special case of higher dimensional automaton in which $Q_n=\emptyset$
for $n>1$. Often automata are required to be \emph{extensional},
meaning that a transition is completely determined by its source,
target and label: $$s_1(q)=s_1(q')\wedge t_1(q)=t_1(q')\wedge l(q)=l(q')
\Rightarrow q=q' ~~~~\mbox{ for } q,q' \in Q_1.$$
In that case, a transition $q\!\in\! Q_1$ can be named after the triple
$(s_1(q),l(q),t_1(q))$, and, writing $S$ for the set of states $Q_0$,
the quadruple $(Q_1,s_1,t_1,l)$ can be conveniently represented by a
relation $T \subseteq S\times A \times S$, thereby contracting the
definition of an automaton to a quadruple $(S,T,I,F)$.

A straightforward embedding of ordinary automata in higher dimensional
automata is given by recognising them as HDA in which $Q_n=\emptyset$
for $n>1$. However, the concurrent interpretation of automata
from \cite{vG88a}, elaborated in \cite{vG96h}, yields a more expressive
model of concurrency.  Here an extensional 1-dimensional automaton
$\eG=(S,T,I,F)$ is, in essence, seen as an abbreviation of a higher
dimensional automaton $\fA(\eG)$ by assuming that any nondegenerate
$n$-dimensional hypercube that can be recognised in $\eG$ is ``filled
in'', i.e.\ constitutes an $n$-dimensional cell in $\fA(\eG)$.  In
\cite{vG88a,vG96h} this was merely a computational interpretation of
automata; here I use it to formally define $\fA(\eG)$. An
$n$-dimensional hypercube in $\eG$ consists of a string $\ell = a_1
\cdots a_n \in A^n$ of $n$ action labels and $2^n$ corners $p_\xi \in
S$, with $\xi\in \{0,1\}^n$ ranging over the strings of $n$ 0s and 1s,
such that $(p_\xi,a_i, p_\chi)\in T$ whenever $\xi$ and $\chi$ differ
only on their $i^{th}$ bit and that bit is 0 in $\xi$ and 1 in
$\chi$. The source $s_i(q)$ (resp.\ target $t_i(q)$) in dimension $i$
of such an $n$-dimensional hypercube $q$ in $\eG$ is the
($n-1$)-dimensional hypercube in $\eG$ obtained by deleting $a_i$ from
$\ell$ and restricting the set of corners $p_\xi$ of $q$ to those in
which the $i^{th}$ bit of $\xi$ is 0 (resp.\ 1).

A hypercube $q=(\ell,p_\xi ~(\xi\!\in\!\{0,1\}^n))$ in
$\eG$ is \emph{degenerate} iff there are indices $1\leq i < j\leq n$
such that $a_i=a_j$ in $\ell$ and, for certain bits $b_k\in\{0,1\}$ ($k\neq i,j$),
\begin{center}
{\LARGE $p$}\large$_{b_1\cdots b_{i-1} 0 b_{i+1} \cdots b_{j-1} 1 b_{j+1} \cdots b_n}$
{\LARGE $=p$}$_{b_1\cdots b_{i-1} 1 b_{i+1} \cdots b_{j-1} 0 b_{j+1} \cdots b_n}.$
\end{center}
In particular, a degenerate square consists of two transitions $(p,a,q)$
and $(q,a,r)$. It is a square by taking $\ell=aa$ and the corners
$p_{00}=p$, $p_{01}= p_{10}=q$ and $p_{11}=r$. The reason for not
assuming this square to be filled in, is that if I do, I loose the
expressive power to specify a sequence of two identical actions that
have to occur in sequential order. Hence the property that at least
all synchronisation trees are representable as automata under the
concurrent interpretation would be lost.
In general, a hypercube in $\eG$ is nondegenerate iff all its
2-dimensional faces are nondegenerate. So the definition of
degeneracy above is the most stringent one I could get away with.

\section{Embedding event oriented models in HDA}
\label{sec-event}

Winskel~\cite{Wi87a,Wi89} introduced six kinds of event structures:
the \emph{prime}, \emph{stable} and [general] \emph{event
structures}, each optionally with the restriction of \emph{binary
conflict}.  The behaviour of these event structures is fully specified
by the \emph{families of configurations} that can be associated to
them; moreover, the family of all configurations of an event structure
is fully determined by the finite configurations in the family.
Hence, event structures embed faithfully in the model of
\emph{configuration structures} of \cite{GP95}, which generalises the
families of configurations of event structures.

\begin{figure}[htb]
\begin{center}
\begin{picture}(20,110)(0,-15)
\put(0,-15){\makebox[0pt]{\textit{synchronisation trees} \cite{Mi80}}}
\put(0,-12){\vector(0,1){9}}
\put(0,2){\makebox[0pt]{\textit{prime event structures}}}
\put(0,-2){\makebox[0pt]{\textit{with binary conflict} \cite{Wi89}}}
\put(-2.5,5){\vector(-1,2){2.5}}
\put(-5.5,11){\makebox[0pt]{\textit{bundle event structures} \cite{Lk92}}}
\put(-6.9,13.8){\vector(-1,2){2.5}}
\put(-9.8,19.6){\makebox[0pt]{\textit{flow event structures} \cite{Bo90}}}
\put(-11.3,22.6){\vector(-1,2){2.2}}
\put(-15,32){\makebox[0pt]{\textit{stable event structures}}}
\put(-15,28){\makebox[0pt]{\textit{with binary conflict} \cite{Wi89}}}
\put(-18,36){\vector(-1,2){10}}
\put(-30,62){\makebox[0pt]{\textit{event structures}}}
\put(-30,58){\makebox[0pt]{\textit{with binary conflict} \cite{Wi89}}}

\put(15,5){\vector(3,1){26}}
\put(0,35){\vector(3,1){26}}
\put(-15,65){\vector(3,1){26}}

\put(45,15){\makebox[0pt]{\textit{prime event structures} \cite{Wi87a}}}
\put(43,19){\vector(-1,2){12}}
\put(30,45){\makebox[0pt]{\textit{stable event structures} \cite{Wi87a}}}
\put(28,49){\vector(-1,2){12}}
\put(15,75){\makebox[0pt]{\textit{event structures} \cite{Wi87a}}}
\put(15,78){\vector(0,1){11}}
\put(15,90){\makebox[0pt]{\textit{configuration structures} \cite{GP95}}}
\end{picture}
\end{center}
\caption{A hierarchy of event oriented models of concurrency\label{event structures}}
\end{figure}

\noindent
In Figure~\ref{event structures}, taken from \cite{GP95}, the six
models of event structures from \cite{Wi87a,Wi89} are ordered with
respect to their expressive power as measured by the class of
configuration structures they can denote. In addition, the figure
includes the {\em flow event structures} of Boudol \cite{Bo90}, and
the \emph{bundle event structures} of Langerak \cite{Lk92}. The
\emph{synchronisation trees} of Milner~\cite{Mi80}, which are just
tree shaped (1-dimensional) automata, can be seen as special kinds of
prime event structures with binary conflict, and, naturally, the
maximal expressive power is obtained by the model of all configuration
structures.

In \cite{vG96h}, the configuration structures are faithfully embedded
in the model of ordinary automata under the concurrent interpretation
of \cite{vG88a}. To this end, the concurrent interpretation of
\cite{vG88a} was extended to cover \emph{all} automata---in \cite{vG88a}
it applied merely to automata of a certain shape: the ones arising
as the images of (labelled) prime event structures.

By composing the mappings of \cite{GP95}, embedding the models of
Figure~\ref{event structures} in configuration structures, of
\cite{vG96h}, embedding configuration structures in automata under the
concurrent interpretation, and of Section~\ref{sec-automata} above,
embedding automata in HDA, all models of Figure~\ref{event structures}
embed faithfully in HDA.

\section{Embedding Petri nets in HDA}
\label{sec-Petri}

In this section I show that the model of higher dimensional automata
is at least at expressive as the model of Petri nets, by giving
translations from Petri nets to higher dimensional automata that
capture exactly the dynamic behaviour of nets, as expressed by the
\emph{firing rule}, informally described below.

\begin{definition}\label{petri}
A (labelled) {\em Petri net} is a tuple $(S,T,F,I,l)$\footnote{The
components of a net $\eN$ are called $S^\eN$, $T^\eN$, $F^\eN$,
$I^\eN$ and $l^\eN$, a convention that also applies to other
structures given as tuples. When clear from context, the index $\eN$
is omitted.} with
\begin{itemize}\vspace{-1ex}
\item $S$ and $T$ two disjoint sets of {\em places} ({\em Stellen} in German)
and {\em transitions},
\vspace{-1ex}\item $F: (S \times T \cup T\times S)\rightarrow \IN$,
the {\em flow relation},
\vspace{-1ex}\item $I:S \rightarrow \IN$, the {\em initial marking},
\vspace{-1ex}\item and $l: T \rightarrow A$, for $A$ a set of
\emph{actions}, the {\em labelling function}.
\end{itemize}\vspace{-1ex}
\end{definition}

\noindent
Petri nets are pictured by drawing the places as circles and the
transitions as boxes, containing their label. For
$x,\hspace{-1.1pt}y\!\in\! S\hspace{-1.4pt}\cup\hspace{-1.4pt} T$
there are $F(\hspace{-1pt}s,\hspace{-1.5pt}t)$ {\em arcs} from $x$ to
$y\hspace{-.9pt}$.

When a Petri net represents a concurrent system, a global state of
this system is given as a \emph{marking}, a function $M:S\rightarrow\IN$.
Such a state is depicted by placing $M(s)$ dots (\emph{tokens}) in
each place $s$. The initial state is given by the marking $I$.
A transition $t$ can \emph{fire} (occur) by taking $F(s,t)$ tokens out
of each place $s$, one for each arc from $s$ to $t$. If this is
possible in the state given by the marking $M:S\rightarrow\IN$, i.e.\
if $F(s,t)<M(s)$ for all $s\in S$, one says that $t$ is \emph{enabled}
under $M$. After $t$ has fired, $F(t,s)$ tokens are added to each
place $s$, one of each arc from $t$ to $s$.
For $t$ a transition in a Petri net $\eN$, let $^\bullet t:
S^\eN\rightarrow \IN$ be given by $^\bullet t (s)=F(s,t)$ and $t^\bullet:
S^\eN\rightarrow \IN$ by $t^\bullet (s)=F(t.s)$. The multiset $^\bullet t$
describes which tokens are consumed by firing $t$, and $t^\bullet$
which tokens are produced.

In {Van Glabbeek \& Vaandrager} \cite{GV87}, Petri nets were studied
from the point of view that transitions may take time, and we
introduced global states in which any number of transitions may be
currently firing. The states represented by markings as defined above
are those in which no transition is currently firing. In general, a
state is given by a multiset of places \emph{and transitions}. In
order to precisely keep track of causal relationships between
transition firings, we found it convenient to represent the (multi)set
of transitions in a state as a list. This made it possible to
distinguish different occurrences of currently firing transitions
(i.e.\ the third and the fifth). Hence an \emph{ST-marking} is
defined as a pair $(M,\sigma)\in \multi(S)\times T^*$ of a multiset of
places and a list of transitions.  This is exactly the notion of state
that I need below in my translations of Petri nets to higher
dimensional automata.

As pointed out in \cite{GP95}, there are $2\times 2 = 4$ computational
interpretations of Petri nets, called the \emph{individual token} and
the \emph{collective token} interpretation, and, orthogonally, the
\emph{self-sequential} and the \emph{self-concurrent} interpretation.
In the individual token interpretation one distinguishes different
tokens residing in the same place, keeping track of where they come
from. If a transition fires by using a token that has been produced by
another transition, there is a causal link between the two.
Consequently, the causal relations between the transitions in a run of
a net can always be described by means of a partial order. In the
collective interpretation, on the other hand, tokens cannot be
distinguished: if there are two tokens in a place, all that is present
there is the number 2. This gives rise to more subtle causal
relationships between transitions in a run of a net, which cannot be
expressed by partial orders.  In the self-concurrent interpretation, a
transition may fire concurrently with itself. This is not allowed in
the self-sequential interpretation.

The below can be understood as a way of formally pinpointing the
differences between these computational interpretations, by giving
four translations from Petri nets into higher dimensional automata,
one for each interpretation. In some sense this amounts to giving
four different semantics of Petri nets. 

\subsection{The self-concurrent collective token interpretation}
\label{collective}

First I define the higher dimensional automaton $\fA^{\rm CT}(\eN)$
associated to a Petri net $\eN$ according to the self-concurrent
collective token interpretation of nets.  As cells of $\fA^{\rm
  CT}(\eN)$ I take the ST-markings of $\eN$, each being a pair
$(M,\sigma)$ of a multiset $M$ of places and a list $\sigma$ of
transitions in $\eN$.  The number of transitions in the list is the
dimension of the cell.  The source $s_i(q)$ (resp.\ the target
$t_i(q)$) in dimension $i$ of a cell $q=(M,\sigma)$ is obtained by
omitting the $i^{th}$ transition $t$ from $\sigma$, and adding the
multiset of places $^\bullet t$ (resp.\ $t^\bullet$) to $M$.  Below, +
denotes the union of multisets, given by $(M+X)(s)=M(s)+X(s)$.  The
empty list is denoted $\varepsilon$.  As there is no standard
definition of successful termination in Petri nets, I map them to HDA
without final states; however, for any definition of successful
termination of Petri nets found in the literature, most likely a
corresponding definition of the final states of the associated HDA can
be obtained.

\begin{definition}
Let N be a Petri net. The higher dimensional automaton
$\fA^{\rm CT}(\eN)=(Q,s,t,I,F,l)$ is given by
\begin{itemize}
\vspace{-1ex}\item $Q_n = \multi(S^\eN)\times (T^\eN)^n$ for $n\in \IN$,
\vspace{-1ex}\item $s_i(\!M,t_1 \cdots t_n)=(M+\,^\bullet t_i,~t_1\cdots t_{i-1}
      t_{i+1} \cdots t_n)$ for $1\!\leq\! i\!\leq\! n$,
\vspace{-1ex}\item $t_i(M,t_1 \cdots t_n)=(M+t_i^\bullet,~t_1\cdots t_{i-1}
      t_{i+1} \cdots t_n)$ for $1\!\leq\! i\!\leq\! n$,
\vspace{-1ex}\item $I=(I^\eN,\varepsilon)$
      and $F=\emptyset$,
\vspace{-1ex}\item $l(M,t)=l^\eN(t)$ for $(M,t)\in Q_1$.
\end{itemize}\vspace{-1ex}
\end{definition}

\noindent
The source and target functions defined above correspond exactly to
the start and termination of a transition firing as defined in clauses
2 and 4 of Definition 7.1.1 in \cite{GV87}. They are also consistent
with the informal description of the firing rule given above.

\subsection{The self-concurrent individual token interpretation}
\label{individual}

Below I will define the notion of a token as it could occur in a Petri
net, in such a way that all possible token occurrences have a
different name.  A token will be a triple $(t',k,s)$, with $s$ the
place where the token occurs, and $t'$ the transition firing that
brought it there.  For tokens that are in $s$ initially, I take
$t'=*$. When the number of tokens that $t'$ deposits in $s$ is $n$, I
distinguish these tokens by giving them ordinal numbers $k=0,1,2,...,n-1$.
In order to define tokens as announced above I need to define transition
firings simultaneously.  These will be pairs $(X,t)$ with $t$ the
transition that fires, and $X$ the set of tokens that is consumed in
the firing. Transitions $t$ that can fire without consuming tokens can
fire multiple times on the same (empty) input; these firings will be
called $(k,t)$ with $k\in \IN$ instead of $(\emptyset,t)$.
I define the functions $\beta$ from tokens to the places
where they occur by $\beta(t',k,s)=s$, and $\eta$ from transition
firings to the transition that fires by $\eta(X,t)=t$. The function
$\beta$ extends to a function from sets of tokens $X$ to multisets of
places $\beta(X):S\rightarrow \IN$, by $\beta(X)(s)=|\{s'\in X\mid
\beta(s')=s\}|$.

\begin{definition}\label{tokens}
Given a Petri net $\eN=(S,T,F,I,l)$, the sets of \emph{tokens} $S_\bullet$
and \emph{transition firings} $T_\bullet$ of $\eN$ are recursively defined by
\begin{itemize}
\vspace{-1ex}
\item $(*,k,s)\in S_\bullet$ for $s\in S$ and $k<I(s)$;
\vspace{-1ex}
\item $(t',k,s)\in S_\bullet$ for $s\in S$, $t'\in T_\bullet$ and $k<F(\eta(t'),s)$;
\vspace{-1ex}
\item $(X,t)\in T_\bullet$ for $t\in T$ and $X \subseteq S_\bullet$ such that
      $\beta(X)=\,^\bullet t \neq \emptyset$;
\vspace{-1ex}
\item $(k,t)\in T_\bullet$ for $k\in\IN$ and $t\in T$ such that
      $^\bullet t=\emptyset$.
\end{itemize}
\end{definition}

\noindent
Now I define the higher dimensional automaton $\fA^{\rm IT}(\eN)$
associated to a Petri net $\eN$ according to the self-concurrent
individual token interpretation of nets.\footnote{As I failed to point
  out in the ENTCS version of this paper, the following definition
  is satisfactory only for \emph{standard nets}, nets in which each
  transition has at least one incoming arc: \mbox{$\forall t\in
  T.~\exists s\in S.~F(s,t)>0$}. For non-standard nets, treating
  firings $(k,t)$ as $(\emptyset,t)$, it is not true that in each
  reachable ST-marking $(M,\sigma)$ of $\fA^{\rm IT}(\eN)$ the
  multiset $M$ is a plain set.}  As cells of $\fA^{\rm IT}(\eN)$ I take the
\emph{ST-markings with individual tokens} of $\eN$, each being a pair
$(M,\sigma)$ of a multiset $M$ of tokens of $\eN$ (each token
allocated to a place in $\eN$) and a list $\sigma$ of transition
firings of $\eN$. The number of transition firings in
the list is the dimension of the cell. The source $s_i(q)$ in
dimension $i$ of a cell $q=(M,\sigma)$ is obtained by omitting the
$i^{th}$ transition firing $(X,t)$ from $\sigma$, and adding the set
of tokens $X$ (or $\emptyset$ in case $X$ is a number $k$) to $M$.
Likewise, the target $t_i(q)$ of $q$ in dimension $i$ is obtained by
omitting the $i^{th}$ transition firing $(X,t)$ from $\sigma$ and
upgrading $M$ by adding $F(t,s)$ tokens to each place $s$.  Below, in
applying the multiset union +, sets $X$ are identified with multisets
by taking $X(s)=1$ if $s\!\in\! X$ and $X(s)=0$ otherwise.

\begin{definition}\label{df-nets2hda}
Let N be a net. The HDA $\fA^{\rm IT}\!(\hspace{-.5pt}\eN\hspace{-.5pt})
=(Q,\hspace{-.5pt}s,\hspace{-.5pt}t,\hspace{-.5pt}I\hspace{-.5pt},\!F\!,l)$
is given by
\begin{itemize}
\vspace{-3pt}\item $Q_n = \multi(S_\bullet^\eN)\times (T_\bullet^\eN)^n$
      for $n\in \IN$,
\vspace{-3pt}\item $s_i(\!M,t'_1 \cdots t'_n)=(M+X,t'_1\cdots t'_{i-1}
      t'_{i+1} \cdots t'_n)$ for $1\!\leq\! i\!\leq\! n$ and $t'_i\!=\!(X,t)$,
\vspace{-3pt}\item $t_i(M,t'_1 \cdots t'_n)=(M+\{(t'_i,k,s)\mid
      k\!<\!F^\eN(\eta(t'_i),s)\},t'_1\cdots t'_{i-1}
      t'_{i+1} \cdots t'_n)$,
\vspace{-3pt}\item $I=(\{(*,k,s)\mid k<I^\eN(s)\},\varepsilon)$
      and $F=\emptyset$,
\vspace{-3pt}\item $l(M,t')=l^\eN(\eta(t'))$ for $(M,t')\in Q_1$.
\end{itemize}
\end{definition}

\noindent
It may be helpful to observe that $\fA^{\rm CT}(\eN)$ can be obtained
from $\fA^{\rm IT}(\eN)$ by applying $\beta$ and $\eta$ to the tokens
and transition firings that make up a cell in $\fA^{\rm IT}(\eN)$; in
particular one has $s_i((\beta,\eta)(q))=(\beta,\eta)(s_i(q))$, and
likewise for $t_i$.

A cell $q\in Q$ in a HDA $\eA$ is \emph{reachable} iff it occurs in a
path of $\eA$ as defined in Section~\ref{paths}.  It is not hard to
check that each reachable cell in $\fA^{\rm IT}(\eN)$ is an ST-marking
with individual tokens $(M,\sigma)$ of $\eN$ in which $M$ is a plain
set. The reason to involve multisets of tokens in the definition above
is to avoid the problems related to unions $M\cup X$ not being
disjoint.

\subsection{The self-sequential interpretations}

A self-sequential version of the collective token interpretation above
is obtained by only allowing cells $(M,\sigma)$ in which no transition
occurs twice in $\sigma$. Likewise, a self-sequential version of the
individual token interpretation above is obtained by only allowing
cells $(M,t'_1\cdots t'_n)$ such that $\eta(t'_i)=\eta(t'_j)
\Rightarrow i=j$.

\subsection{The relative expressiveness of the four interpretations}

Each of the four computational interpretations above makes a different
model of concurrency out of Petri nets. These models can now be
compared with respect to their expressive power in denoting higher
dimensional automata. A partial result is easily obtained:
standard nets under the collective token interpretation are at least
as expressive as standard nets under the individual token
interpretation, in the sense that any higher dimensional automaton
that can be denoted by a standard net under the individual token
interpretation can also be a denoted by a standard net under the
collective token interpretation.

\begin{theorem}\label{thm-standard}
For every standard net $\eN$ there exists a standard net
$\eN_\bullet$, such that $\fA^{\rm CT}(\eN_\bullet)=\fA^{\rm IT}(\eN)$.
\end{theorem}

\begin{proof}
$\eN_\bullet=(S_\bullet,T_\bullet,F_\bullet,I_\bullet,l_\bullet)$ with
\begin{itemize}
\vspace{-3pt}\item $S_\bullet$ and $T_\bullet$ as in Definition~\ref{tokens}.
\vspace{-3pt}\item $F_\bullet(s',t')=1$ if $t'=(X,t)$ with $s'\in X$;
      $F_\bullet(s',t')=0$ otherwise.
\vspace{-3pt}\item $F_\bullet(t',s')=1$ if $s'$ has the form $(t',k,s)$;
      $F_\bullet(t',s')=0$ otherwise.
\vspace{-3pt}\item $I_\bullet(*,k,s)=1$ and $I_\bullet(t',k,s)=0$ for $t'\in T_\bullet$.
\vspace{-3pt}\item $l_\bullet(t')=l^\eN(\eta(t'))$ for $t'\in T_\bullet$.
\end{itemize}
That $\fA^{\rm CT}(\eN_\bullet)=\fA^{\rm IT}(\eN)$ is straightforward.
\end{proof}

\noindent
The net $\eN_\bullet$ constructed above is a close relative of the
\emph{unfolding} of a Petri net into an \emph{occurrence net}, as
defined in \cite{MMS92}. The difference is that I have not bothered to
eliminate unreachable places and transitions.

In general, results as strong as the one above can not be obtained:
in order to compare expressiveness in a meaningful way, processes
represented by higher dimensional automata, Petri nets, or other
models of concurrency should be regarded modulo some semantic
equivalence relation. A particularly fine equivalence relation that
allows one to totally order the computational interpretations of Petri
nets is \emph{isomorphism of reachable parts} of HDA.

\begin{definition}\newcommand{\fI}{{\cal I}}
Two higher dimensional automata $\eA$ and $\eB$ are \emph{isomorphic}
if there exists a dimension preserving bijection $\cal I$ between their
cells, such that
\begin{itemize}
\vspace{-3pt}\item  $s^\eB_i(\fI(q))=\fI(s^\eA_i(q))$,
\vspace{-3pt}\item  $t^\eB_i(\fI(q))=\fI(t^\eA_i(q))$,
\vspace{-3pt}\item  $\fI(I^\eA)=I^\eB$,
\vspace{-3pt}\item  $ \fI(q)\in F^\eB \Leftrightarrow q\in F^\eA$,
\vspace{-3pt}\item  $l^\eB(\fI(q))=l^\eA(q)$ for $q\in Q^\eA_1$.
\end{itemize}
The \emph{reachable part} ${\cal R}(\eA)$ of an HDA $\eA$ is the HDA
consisting of its \emph{reachable cells}, those that occur in a path
of $\eA$ as defined in Section~\ref{paths}.  (Note that ${\cal
R}(\eA)$ is closed under $s_i$ and $t_i$.) Write $\eA \cong \eB$ if
${\cal R}(\eA)$ and ${\cal R}(\eB)$ are isomorphic.
\end{definition}

\noindent
It is possible to extend Definition~\ref{df-nets2hda}
and Theorem~\ref{thm-standard} to non-standard nets and
show that there is a subclass of Petri nets such that
\begin{itemize}
\item for any net $\eN$ in that subclass, $\fA^{\rm
  CT}(\eN)\cong\fA^{\rm IT}(\eN)$, and
\item for any net $\eN$ there is a  net $\eN'$ in the subclass such
  that $\fA^{\rm IT}(\eN')\cong\fA^{\rm IT}(\eN)$.
\end{itemize}
In fact, the indented subclass is close to the occurrence nets of
Nielsen, Plotkin \& Winskel \cite{NPW81}, but not necessarily with the
requirements that cause the elimination of unreachable parts.

Thus, up to isomorphism of reachable parts of associated HDA, the class of
all Petri nets under the individual token interpretation is equally
expressive as a subclass of nets on which the two interpretations
coincide. The situation with the self-concurrent and self-sequential
interpretations is likewise, leading to a hierarchy:

\begin{figure}[h]
\begin{center}
\begin{picture}(0,45)(0,-14)
\put(0,-12){\makebox[0pt]{\textit{self-sequential individual token interpretation}}}
\put(0,-3.5){\vector(0,-1){5}}
\put(0,-6.5){\vector(0,1){5}}
\put(0,0){\makebox[0pt]{\textit{self-concurrent individual token interpretation}}}
\put(0,3.5){\vector(0,1){10}}
\put(0,15){\makebox[0pt]{\textit{self-sequential collective token interpretation}}}
\put(0,18.5){\vector(0,1){10}}
\put(0,30){\makebox[0pt]{\textit{self-concurrent collective token interpretation}}}
\end{picture}
\caption{Relative expressiveness of four computational
  interpretations of Petri nets}
\label{computational hierarchy}
\end{center}\end{figure}

\noindent
For this reason, the self-concurrent collective token interpretation
will be my default; this is the interpretation that comes with the
Petri net entries in Figure~\ref{hierarchy}.  In order to integrate
the hierarchies of Figures~\ref{event structures}
and~\ref{computational hierarchy}, it pays to consider higher
dimensional automata up to a semantic equivalence coarser than
isomorphism of reachable parts. I will define such equivalences in
Section~\ref{sec-bisimulation}, using the material of
Section~\ref{sec-homotopy}. It turns out that up to history preserving
bisimulation equivalence the self-sequential and the self-concurrent
collective token interpretations of Petri nets coincide.

\section{Homotopy for Higher Dimensional Automata}
\label{sec-homotopy}

\subsection{Naming the faces of n-cells}

\def\T{\kern.0pt\rule[0pt]{2.8pt}{.4pt}\kern-.2pt%
\rule[0pt]{.4pt}{4.4pt}\kern-.3pt\rule[4.2pt]{3.3pt}{.4pt}\kern1.2pt}%
In order to name the faces of a hypercube, following \cite{Pr02a}, I
use the bits $0$, $\T$ and $1$ to indicate whether a transition has
not yet started, is active, or has terminated, respectively.  In other
work, the bit $\T$ is sometimes called $\frac12$, $A$, or $T$ for
\emph{active} or \emph{in transition}, and yet others use the bits
$0$, $1$, $2$, or $-$, $0$, $+$.

Since an $n$-cell represents a list of $n$ transitions being active
concurrently, each of its $3^n$ faces can be represented by a list
$b_1 \cdots b_n$ of $n$ such bits, where $b_i$ indicates the status of
the $i^{th}$ transition in the list.  Thus, the dimension of the face
$b_1 \cdots b_n$ is given by the number of $\T$s in the list, $\T
\cdots \T$ is the identity map, and $\T \cdots \T 0 \T \cdots \T$
(resp.\ $\T \cdots \T 1 \T \cdots \T$), with only $b_i\neq\T$, denotes
the map $s_i$ (resp.\ $t_i$).  The face $b_1 \cdots b_n$ can also be
expressed as $\alpha_1 \circ \ldots \circ \alpha_n$ with
$\alpha_i=s_i$ if $b_i=0$, $\alpha_i=t_i$ if $b_i=1$, and
$\alpha_i=Id$, the identity map, if $b_i=\T$.  Using this convention,
the $2^n$ 0-dimensional corners of an $n$-cell $q$ are named by lists
$b_1 \cdots b_n$ with $b_i \in \{0,1\}$, and the $n\cdot 2^{n-1}$
1-dimensional edges of $q$ by lists containing exactly one occurrence
of $\T$.

\subsection{Labelling n-cells}\label{labelling}

As a HDA is required to satisfy $l(s_i(q))=l(t_i(q))$ for all $q\in
Q_2$ and $i=1,2$, it follows that, for each $q\in Q_n$ and each $1\leq
i \leq n$, the $2^{n-1}$ edges $b_0 \cdots b_{i-1} \T b_{i+1} \cdots
b_n$ of $q$, with $b_j\in\{0,1\}$ for $j\neq i$, all have the same label.
Calling this label $l_i(q)$, the labelling function $l:Q_1\rightarrow
A$ can be extended to $Q := \bigcup_{k=0}^\infty Q_k$ by
$l(q)=l_1(q)\cdots l_n(q)$ for $q\in Q_n$. Thus, the label of an
$n$-dimensional hypercube $q$ is the list of the labels of the $n$
transitions whose concurrent execution is represented by $q$.

\subsection{Paths and their observable content}\label{paths}

\begin{definition}\label{path}
A \emph{path} in a higher dimensional automaton
$(Q,s,t,I,F,l)$ is a sequence of pairs
$(\partial_1,q_1)(\partial_2,q_2) \cdots (\partial_m,q_m)$, denoted
$I\frac{\partial_1}{}q_1\frac{\partial_2}{}q_2\frac{\partial_3}{}
\cdots \frac{\partial_m}{}q_m$, with $q_k \in Q$ and $\partial_k \in
\{s_i,t_i\mid 1\leq i \leq d(q_k)\}$ for $1\leq k \leq m$, such that
\begin{center}
 $q_{k-1}=s_i(q_k)$ if $\partial_k=s_i$ ~~~~~~and~~~~~~
 $q_k=t_i(q_{k-1})$ if $\partial_k=t_i$.
\end{center}
Here $q_0:=I$, i.e.\ I consider only paths starting from the initial
state, and $d(q)$, de \emph{dimension} of $q$, is $n$ if $q\in Q_n$.
One writes $end(\pi)$ for $q_m$.
\end{definition}
\noindent
A path $\pi$ in a HDA $\eA$ represents a partial run of the system
represented by $\eA$ in which between every two consecutive
states an action starts or terminates. It represents a total run
iff $end(\pi)\in F$. If $\partial_k=s_i$, the transition from
$q_{k-1}$ to $q_k$ represents the start of the action $l_i(q_k)$, and
if $\partial_k=t_i$, it represents the termination of the action
$l_i(q_{k-1})$.
\begin{definition}
Write $\textit{split-trace\/}(\pi)$ for the sequence $\sigma_1 \cdots
\sigma_m$, where $\sigma_k = l_i(q_k)^+$ if $\partial_k=s_i$, and
$\sigma_k = l_i(q_{k-1})^-$ if $\partial_k=t_i$.
\end{definition}
\noindent
$\textit{Split-trace\/}(\pi)$ approximates the observable content of a path
$\pi$. It consists of the sequence of starts $a^+$ and terminations
$a^-$ of actions $a$ occurring during the run represented by
$\pi$. The HDA of Figure~\ref{parallelism} in which the square is not
filled in, for instance, has only two maximal paths, whose
split-traces are $a^+ a^- b^+ b^-$ and $b^+ b^- a^+ a^-$. (The prefixes of
these sequences are also split-traces of paths.) The HDA of
Figure~\ref{parallelism} in which the square \emph{is} filled in
moreover has paths with split-traces like $a^+ b^+ b^- a^-$.

If it is possible to keep track of parallel occurrences of the same
action, a split-trace falls short of representing the full observable
content of a path.  The observable behaviour of a real-time execution
would consist of a set of action occurrences, with for each action
occurrence an interval given by a start time and a termination time,
indicating the period during with the action takes place. Abstracting
from real-time information, what remains is a split-trace~$\sigma$%
---a sequence $\sigma=\sigma_1 \cdots \sigma_m$ of \emph{action
phases}, each being a start $a^+$ or a termination $a^-$ of an action
$a$---together with an injective function \textit{start} from the
(indices of) termination phases in $\sigma$ to the (indices of) start
phases in $\sigma$.  This functions tells for every termination of an
action occurrence in $\sigma$ where that action occurrence starts.
Naturally, for every termination phase $\sigma_\ell=a^-$ in $\sigma$,
one has $\textit{start}(\ell)<\ell$ and $\sigma_{{\it
start}(\ell)}=a^+$.  Such an annotated split-trace is called an
\emph{ST-trace}. It can be compactly represented by writing $a^{{\it
start}(\ell)}$ for $\sigma_\ell$ whenever $\sigma_\ell=a^-$. A formal
definition of the ST-trace of a path in a higher dimensional automaton
will follow in Section~\ref{matching}.
\vspace{1ex}
\begin{figure}[htp]
%\input{interval}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \graphtemp=.5ex\advance\graphtemp by 0.248in
    \rlap{\kern 0.098in\lower\graphtemp\hbox to 0pt{\hss $b^+$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.248in
    \rlap{\kern 0.492in\lower\graphtemp\hbox to 0pt{\hss $a^+$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.248in
    \rlap{\kern 0.886in\lower\graphtemp\hbox to 0pt{\hss $a^+$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.248in
    \rlap{\kern 1.280in\lower\graphtemp\hbox to 0pt{\hss $b^-$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.248in
    \rlap{\kern 1.673in\lower\graphtemp\hbox to 0pt{\hss $a^+$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.248in
    \rlap{\kern 2.067in\lower\graphtemp\hbox to 0pt{\hss $a^-$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.248in
    \rlap{\kern 2.461in\lower\graphtemp\hbox to 0pt{\hss $b^+$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.248in
    \rlap{\kern 2.854in\lower\graphtemp\hbox to 0pt{\hss $a^-$\hss}}%
    \special{pn 8}%
    \special{ar 689 886 886 886 -2.159827 -0.981765}%
    \special{ar 1476 886 886 886 -2.159827 -0.981765}%
    \special{ar 2264 886 886 886 -2.159827 -0.981765}%
    \hbox{\vrule depth0.346in width0pt height 0pt}%
    \kern 2.953in
  }%
}%
\centerline{\raise 1em\box\graph}
\caption{An ST-trace}
\label{ST-trace}
\end{figure}

\noindent
A typical ST-trace is depicted as Figure~\ref{ST-trace}.  It lists
the starts and terminations of actions occurring in a path, and
additionally links the start and termination of the same action.
Its compact representation is $b^+ a^+ a^+ b^1 a^+ a^3 b^+ a^5$.
Note that it contains more information than the underlying split-trace.
ST-traces were introduced in \cite{vG90} in the context of event
structures. Arguably, they constitute the best formalisation of the
observable content of execution paths. 

Paths and their ST-traces lack the possibility to express that action
phases happen simultaneously. However, in higher dimensional automata
two action phases can occur simultaneously iff they can occur in
either order.  Therefore, considering only paths in which all
action phases are totally ordered does not lead to a decrease in
expressive power.

\subsection{Homotopy}

Two paths in a higher dimensional automaton can be considered
equivalent if they differ merely in the timing of causally independent
actions.  This applies for instance to the path $ab$ and the path $ba$
in the automaton of Figure~\ref{inside}, given that the actions $a$
and $b$ are causally independent. However, it would not apply when the
square is not filled in, as this signifies mutual exclusion, and the
relative order of $a$ and $b$ would matter.  As observed by Pratt
\cite{Pr91a}, this notion of equivalence can be formalised beautifully
by means of what he calls ``monoidal homotopy''.  When seeing a higher
dimensional automaton as a structure composed of higher dimensional
cubes embedded in a higher dimensional Euclidean space, two paths are
\emph{homotopic} if one can be obtained out of the other by a
continuous transformation, keeping the begin and endpoints the same,
and allowing as intermediate stages of the transformation arbitrary
paths going through the insides of higher dimensional cells, as long
as they are monotonically increasing when projected on the axes of the
cells they are going through. The path drawn in Figure~\ref{inside} for
instance could be one of the uncountably many stages in the continuous
transformation of $ab$ into $ba$.

This form of homotopy differs from the standard homotopy used in
topology in that the directed nature of the underlying space needs to
be preserved during transformations.  Therefore it is called
\emph{monoidal homotopy} \cite{Pr91a}, or \emph{directed homotopy}
(\emph{dihomotopy}) \cite{GR02}, as opposed to \emph{group homotopy},
although in the context of higher dimensional automata it is simply
called \emph{homotopy}.

The following discrete analog of continuous deformation defines the
same concept of homotopy without involving the notion of Euclidean space.

\begin{definition}\label{homotopy}
Two paths $\pi$ and $\pi'$ are \emph{adjacent}---denoted $\pi
\leftrightarrow \pi'$---if one can be obtained from the other by
replacing, for $q,q'\in Q$ and $i<j$,
\begin{itemize}\vspace{-3pt}
\renewcommand{\itemsep}{0pt}
\item a segment
$\frac{s_i}{}q\frac{s_j}{}$ by $\frac{s_{j-1}}{}q'\frac{s_i}{}$,
\item a segment
$\frac{t_j}{}q\frac{t_i}{}$ by $\frac{t_i}{}q'\frac{t_{j-1}}{}$,
\item a segment
$\frac{s_i}{}q\frac{t_j}{}$ by $\frac{t_{j-1}}{}q'\frac{s_i}{}$,
\item or a segment
$\frac{s_j}{}q\frac{t_i}{}$ by $\frac{t_i}{}q'\frac{s_{j-1}}{}$.
\end{itemize}\vspace{-3pt}
\emph{Homotopy} is the reflexive and transitive closure of adjacency.
\end{definition}
\noindent
The third adjacency replacement above can be motivated as follows:
suppose we have a list of $n$ actions, numbered $1$ to $n$, and we
first insert an action $a$ at position $i$ (thereby incrementing the
slot-numbers $\geq\!i$ by one) and subsequently delete the $j^{th}$
action $(j>i)$ from the list (thereby decrementing the slot-numbers
$>\!j$ by one), then we get the same result as when we first delete
the $(j-1)^{th}$ action (thereby decrementing the slot-numbers $\geq
\!j$ by one) and subsequently insert the action $a$ at position $i$
(incrementing the slot-numbers $\geq\!i$).
The other replacements are motivated in a similar way.

The paths with split-traces $a^+ a^- b^+ b^-$ and $b^+ b^- a^+ a^-$ in
Figure~\ref{inside} for instance are homotopic, because the first can
be transformed into the second through four adjacency replacements, namely
(on the level of split-traces)
\vspace{-1ex}
$$a^+ a^- b^+ b^- \leftrightarrow a^+ b^+ a^- b^- \leftrightarrow
\vspace{-1ex}
b^+ a^+ a^- b^- \leftrightarrow b^+ a^+ b^- a^- \leftrightarrow b^+b^-a^+a^-.$$
Homotopic paths share their endpoints. A homotopy class of paths in a
higher dimensional automaton (with endpoint $q$) is called a
\emph{history} (of $q$). Histories form the analog of paths, after
abstraction from the order or causally independent action occurrences.

\subsection{Matching starts and terminations of action occurrences in paths}
\label{matching}
 
The following proposition illustrates the agreement between
Definition~\ref{homotopy} and the cubical laws of Definition~\ref{hda}.

\begin{proposition}\label{adjacency}
For every segment $p\frac{s_i}{}q\frac{t_j}{}r$ with $i\neq j$, and
for every segment $p\frac{s_i}{}q\frac{s_j}{}r$ or
$p\frac{t_i}{}q\frac{t_j}{}r$ in a path $\pi$ in a HDA $\eA$, there
exists a unique path $\pi'$ in $\eA$, adjacent to $\pi$, that can be
obtained from $\pi$ by replacing the indicated segment in the manner
described in Definition~\ref{homotopy} (going either right or left).
\end{proposition}

\begin{proof}
Suppose $\pi$ contains $p\frac{s_i}{}q\frac{t_j}{}r$, with $i<j$.
Then $p=s_i(q)$ and $r=t_j(q)$. By the cubical laws in
Definition~\ref{hda},
$t_{j-1}(p)=t_{j-1}((s_i(q))=s_i(t_j(q))=s_i(r)$.  Hence the unique
replacement is $p\frac{t_{j-1}}{}q'\frac{s_i}{}r$ with
$q'=t_{j-1}(p)=s_i(r)$.

Likewise, suppose $\pi$ contains $p\frac{s_i}{}q\frac{s_j}{}r$, with $i<j$.
Then $p=s_i(q)$ and $q=s_j(r)$. By the cubical laws (*) in
Definition~\ref{hda} one has $p=s_{j-1}(s_i(r))$. So the unique
replacement is $p\frac{s_{j-1}}{}q'\frac{s_i}{}r$ with $q'=s_i(r)$.

The other four cases go similarly.
\end{proof}
\noindent
The intuition is that when two actions happen concurrently, they can
start in either order as well as terminate in either order; moreover,
if it is possible for action $a$ to start before $b$ terminates, $b$
could just as well terminate before $a$ starts, provided $a$ and $b$
are distinct action occurrences. Note, however, that
Proposition~\ref{adjacency} does not apply to segments
$p\frac{t_i}{}q\frac{s_j}{}r$. If the termination of one action
precedes the start of another, it may be that there is a causal link
between the two that prevents this order from being interchanged.

Write $\pi \stackrel{\ell}{\longleftrightarrow} \pi'$ if $\pi'$ can be obtained
from $\pi=I\frac{\partial_1}{}q_1\frac{\partial_2}{}q_2\frac{\partial_3}{}
\cdots \frac{\partial_m}{}q_m$ by an adjacency replacement of the segment
\plat{\frac{\partial_{\ell}}{}q_\ell\frac{\partial_{\ell+1}}{}} of
$\pi$, inducing a swap of the action phases $\sigma_\ell$ and
$\sigma_{\ell+1}$ in the split-trace $\sigma=\sigma_1 \cdots \sigma_m$
of $\pi$. Assume $\partial_{\ell+1}=t_i$, i.e.\ $\sigma_{\ell+1}$
is the termination $l_i(q_{\ell})^-$ of an action $l_i(q_{\ell})$.
In case $\partial_{\ell}=s_i$ we have that $\sigma_\ell$ is the start
$l_i(q_{\ell})^+$ of the very same occurrence of the action
$l_i(q_{\ell})$ in $\pi$. In this case $\sigma_\ell$ and
$\sigma_{\ell+1}$ cannot be swapped: there is no path $\pi'$ such that
\plat{\pi \stackrel{\ell}{\longleftrightarrow}\pi'}.
Proposition~\ref{adjacency} tells that in all other cases (i.e.\
when $\partial_{\ell}\neq s_i$) $\sigma_{\ell}$ and $\sigma_{\ell+1}$
can be swapped: there exists a unique path $\pi'$ in
$A$ with \plat{\pi\stackrel{\ell}{\longleftrightarrow}\pi'}. This makes it
possible to tell which action phase in $\textit{split-trace}(\pi)$ is
the start of the action occurrence whose termination happens as phase
$\sigma_{\ell+1}$: it is the unique phase $\sigma_k$ such that
$\pi \stackrel{\ell}{\longleftrightarrow}
\pi_{\ell} \stackrel{\ell-1}{\longleftrightarrow}
\pi_{\ell-1} \stackrel{\ell-2}{\longleftrightarrow}
\cdots \stackrel{k+1}{\longleftrightarrow} \pi_{k+1}
\hspace{7pt}\not\hspace{-7pt}\stackrel{k}{\longleftrightarrow} \pi_{k}$.
\begin{definition}
Let $\pi=I\frac{\partial_1}{}q_1\frac{\partial_2}{}q_2\frac{\partial_3}{}
\cdots \frac{\partial_m}{}q_m$ be a path in a higher dimensional automaton.
For $1\leq \ell \leq m$ such that $\partial_\ell$ denotes a termination phase,
let ${\it start}(\ell)$ denote the unique number $k$ such that
$$\pi \stackrel{\ell-1}{\longleftrightarrow}
\pi_{\ell-1} \stackrel{\ell-2}{\longleftrightarrow}
\cdots \stackrel{k+1}{\longleftrightarrow} \pi_{k+1}
\hspace{7pt}\not\hspace{-7pt}\stackrel{k}{\longleftrightarrow} \pi_{k}.$$
Now $\textit{ST-trace}(\pi)$ is the sequence obtained from
$\textit{split-trace}(\pi)=\sigma_1\cdots\sigma_k$, by replacing
$\sigma_\ell$ by $a^{{\it start}(\ell)}$ whenever $\sigma_\ell = a^-$.
\end{definition}

\section{Bisimulation semantics for HDA}
\label{sec-bisimulation}

Using the material of Section~\ref{sec-homotopy}, I now extend the
main forms of bisimulation equivalence found in the literature that do
not involve a special treatment of \emph{hidden} or \emph{internal}
actions, to higher dimensional automata.  For \emph{interleaving
bisimulation equivalence} this is trivial: it is just the standard
notion of bisimulation equivalence on ordinary automata found in the
literature \cite{Mi80,BW90}, applied to higher dimensional automata by
ignoring their higher dimensional cells.
\emph{ST-bisimulation equivalence} \cite{GV87} is a branching time
respecting equivalence that takes causality into account to the extent
that it is expressible by durational actions overlapping in time.
\emph{History preserving bisimulation equivalence} \cite{RT88,GG01} is
the coarsest equivalence that fully respects branching time, causality
and their interplay. \emph{Hereditary history preserving bisimulation
equivalence} \cite{Bz91} is a variant of the latter that strongly
respects the internal structure of processes, while still collapsing
choices between indistinguishable courses of action (i.e.\ satisfying
the CCS law $x+x=x$ \cite{Mi80}).

By Definition~\ref{path}, the empty path in a higher dimension
automata $\eA$ starts and ends in the initial state of $\eA$ and hence
is denoted $I^\eA$.  I write $\pi \rightarrow \pi'$ if $\pi$ is a
prefix of a path $\pi'$, i.e., if $\pi'$ is an extension of $\pi$.

\begin{definition}
Two higher dimensional automata $\eA$ and $\eB$ are \emph{history
  preserving bisimulation equivalent} if there exists a binary
  relation $R$ between their paths---a \emph{history preserving
  bisimulation}---such that
\begin{enumerate}\vspace{-3pt}
\renewcommand{\itemsep}{0pt}
\item[(1)]
the empty paths in $\eA$ and $\eB$ are related: $I^\eA R I^\eB$,
\item[(2)]
if $\pi R \rho$ then then $\textit{ST-trace}_\eA(\pi)=\textit{ST-trace}_\eB(\rho)$,
\item[(3)]
if $\pi R \rho$ and $\pi \leftrightarrow \pi'$ then $\exists \rho'$ with
$\rho \leftrightarrow \rho'$ and $\pi' R \rho'$,
\item[(4)]
if $\pi R \rho$ and $\rho \leftrightarrow \rho'$ then $\exists \pi'$ with
$\pi \leftrightarrow \pi'$ and $\pi' R \rho'$,
\item[(5)]
if $\pi R \rho$ and $\pi \rightarrow \pi'$ then $\exists \rho'$ with
$\rho \rightarrow \rho'$ and $\pi' R \rho'$,
\item[(6)]
if $\pi R \rho$ and $\rho \rightarrow \rho'$ then $\exists \pi'$ with
$\pi \rightarrow \pi'$ and $\pi' R \rho'$,
\item[(7)]
and if $\pi R \rho$ then $end(\pi)\in F^A \Leftrightarrow end(\rho)\in F^B$.
\end{enumerate}
 $\eA$ and $\eB$ are \emph{hereditary history preserving
  bisimulation equivalent} if there exists a history preserving
  bisimulation $R$ between their paths that moreover satisfies
\begin{enumerate}\vspace{-3pt}
\renewcommand{\itemsep}{0pt}
\item[(8)]
if $\pi R \rho$ and $\pi' \rightarrow \pi$ then $\exists \rho'$ with
$\rho' \rightarrow \rho$ and $\pi' R \rho'$, and
\item[(9)]
if $\pi R \rho$ and $\rho' \rightarrow \rho$ then $\exists \pi'$ with
$\pi' \rightarrow \pi$ and $\pi' R \rho'$.
\end{enumerate}
\emph{ST-bisimulation equivalence} between HDA is defined exactly as history
preserving bisimulation equivalence, but dropping clauses (3) and (4).
\end{definition}

\noindent
Note that in the presence of clause (2), related paths have the same
length. Hence clauses (8) and (9) are equivalent. I listed them both
solely to stress the symmetric nature of the definition. It is not
hard to see that the notion of ST-bisimulation equivalence would not
change upon adding clauses (8) and (9), but because of clauses (3) and
(4), this does not apply to history preserving bisimulation
equivalence.  Using clause (2) it follows that the effect of clauses
(3) and (4) would not change if I wrote
\plat{\stackrel{\ell}{\longleftrightarrow}} instead of
$\leftrightarrow$ throughout these clauses.  The clauses (3) and (4)
express that the causal relations between action phases in the
ST-traces of two related paths are the same, for these relations are
determined by the space of all allowed permutations of action phases.

\section{A hierarchy of concurrency models}
\label{counterexamples}

After having defined precisely what the arrows in
Figure~\ref{hierarchy} mean, I will now proceed to argue for their
soundness and completeness in describing the relative expressiveness
of the models of concurrency under investigation.

\subsection{Soundness of the inclusions of Figure~\ref{hierarchy}}
\label{soundness}

It is well known that stable event structures with binary conflict
\cite{Wi89} are more expressive than flow event structures
\cite{Bo90}, which are more expressive than bundle event structures
\cite{Lk92}, which are in turn more expressive than prime event
structures with binary conflict \cite{Wi89}, cf.\ Figure~\ref{event
structures}. However, this holds when comparing the families of
configurations they can express; the difference disappears when
working up to history preserving bisimulation.  This follows
immediately from the fact that prime and stable event structures with
binary conflict specify the same \emph{Scott domains}
\cite{Wi87a,Wi89}, and thus also the same [higher dimensional]
automata. Alternatively, a direct proof can be found in \cite{GV03}.
In \cite{GV03} and \cite{NW96} it has furthermore been shown that, up
to history preserving bisimulation, finitary conflict can be expressed
in terms of binary conflict. Thus, by the criteria of this paper, the
stable event structures of \cite{Wi87a} do not rank higher in
expressive power than the ones with binary conflict in
\cite{Wi89}. Likewise, the general event structures of \cite{Wi87a} do
not rank higher in expressive power than the ones with binary conflict
in \cite{Wi89}. This shows that up to history preserving bisimulation
Figure~\ref{event structures} collapses into the bottom of
Figure~\ref{hierarchy}.

A Petri net is \emph{safe} if no reachable marking will every have two
tokens in the same place. In \cite{NPW81} the expressive equivalence
has been established of the model of safe Petri nets with that of
prime event structures with binary conflict. This was done by means of
translations between these models that preserve more than history
preserving bisimulation equivalence.

Up to history preserving bisimulation equivalence, on safe Petri nets
there is no difference between any of the four computational
interpretations of Petri nets discussed in Section~\ref{sec-Petri}.
Moreover, the nets $\eN_\bullet$, constructed in the proof of
Theorem~\ref{thm-standard}, are safe. It follows that under the
self-sequential individual token interpretation, as well as under the
self-concurrent individual token interpretation, the class of all
Petri nets is equally expressive as the class of safe Petri nets.

In \cite{GP95} two forms of 1-unfolding are defined, one for Petri
nets under the self-concurrent collective token interpretation, and
one for Petri nets under the self-sequential collective token
interpretation. Each of them converts any Petri net into a so-called
\emph{1-occurrence net}, a net in which each transition can fire only
once. And each of these 1-unfoldings respects history preserving
bisimulation equivalence w.r.t.\ to the computational
interpretation of nets that comes with this 1-unfolding.
Trivially, on 1-occurrence nets there is no difference between the
self-concurrent and the self-sequential interpretation of nets.
It follows that, up to history preserving bisimulation equivalence,
Petri nets under the self-sequential collective token interpretation
are equally expressive as Petri nets under the self-concurrent
collective token interpretation.

A Petri net is \emph{pure} if it has no \emph{self-loops}, i.e.\ there
are no places $s$ and transitions $t$ with $F(s,t)>0$ and $F(t,s)>0$.
In \cite{GP95} we showed that configuration structures are equally
expressive as pure Petri nets under the collective token
interpretation (or precisely, each of the two collective token
interpretations). Taking into account that pureness is preserved by
the two 1-unfoldings, this was done my means of translations between
configuration structures and pure 1-occurrence nets that preserve more
than history preserving bisimulation equivalence.

This concludes the justification of the arrows in Figure~\ref{hierarchy}.

\subsection{Completeness of the inclusions of Figure~\ref{hierarchy}}
\label{completeness}

That the model of synchronisation trees is less expressive than that
of safe Petri nets is witnessed by the process $a\|b$, the
parallel composition of two actions $a$ and $b$. This process can be
represented by the safe Petri net P in Figure~\ref{parallelism}.
However, there is no synchronisation tree which is history preserving
bisimulation equivalent, or even ST-bisimulation equivalent, to this process.

The models of prime and stable event structures are less expressive
than that of (general) event structures of \cite{Wi89}.
This is witnessed by the process of Figure~\ref{fig-disjunctive}, which is
\begin{figure}
%\input{disjunctive}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \special{pn 8}%
    \special{ar 3150 886 98 98 0 6.28319}%
    \special{pa 3150 984}%
    \special{pa 3150 1181}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3175 1142}%
    \special{pa 3150 1181}%
    \special{pa 3125 1142}%
    \special{pa 3175 1142}%
    \special{fp}%
    \special{pa 3051 1378}%
    \special{pa 3248 1378}%
    \special{pa 3248 1181}%
    \special{pa 3051 1181}%
    \special{pa 3051 1378}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.280in
    \rlap{\kern 3.150in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
    \special{ar 2756 98 98 98 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.098in
    \rlap{\kern 2.756in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 2756 197}%
    \special{pa 2756 394}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2781 354}%
    \special{pa 2756 394}%
    \special{pa 2731 354}%
    \special{pa 2781 354}%
    \special{fp}%
    \special{pa 2657 591}%
    \special{pa 2854 591}%
    \special{pa 2854 394}%
    \special{pa 2657 394}%
    \special{pa 2657 591}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 2.756in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{pa 2854 591}%
    \special{pa 3080 816}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3070 771}%
    \special{pa 3080 816}%
    \special{pa 3034 806}%
    \special{pa 3070 771}%
    \special{fp}%
    \special{ar 3543 98 98 98 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.098in
    \rlap{\kern 3.543in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 3543 197}%
    \special{pa 3543 394}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3568 354}%
    \special{pa 3543 394}%
    \special{pa 3518 354}%
    \special{pa 3568 354}%
    \special{fp}%
    \special{pa 3445 591}%
    \special{pa 3642 591}%
    \special{pa 3642 394}%
    \special{pa 3445 394}%
    \special{pa 3445 591}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 3.543in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{pa 3445 591}%
    \special{pa 3219 816}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3265 806}%
    \special{pa 3219 816}%
    \special{pa 3229 771}%
    \special{pa 3265 806}%
    \special{fp}%
    \special{ar 2756 886 98 98 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 2.756in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 2826 955}%
    \special{pa 3051 1181}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3041 1136}%
    \special{pa 3051 1181}%
    \special{pa 3006 1171}%
    \special{pa 3041 1136}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.098in
    \rlap{\kern 1.575in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 1.181in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1519 154}%
    \special{pa 1237 436}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1282 426}%
    \special{pa 1237 436}%
    \special{pa 1247 391}%
    \special{pa 1282 426}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.295in
    \rlap{\kern 1.378in\lower\graphtemp\hbox to 0pt{\hss $a~$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 1.181in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1181 571}%
    \special{pa 1181 807}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1206 768}%
    \special{pa 1181 807}%
    \special{pa 1156 768}%
    \special{pa 1206 768}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.689in
    \rlap{\kern 1.181in\lower\graphtemp\hbox to 0pt{\hss $c~~~$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 1.280in
    \rlap{\kern 1.575in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1237 942}%
    \special{pa 1519 1224}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1509 1178}%
    \special{pa 1519 1224}%
    \special{pa 1474 1214}%
    \special{pa 1509 1178}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.083in
    \rlap{\kern 1.378in\lower\graphtemp\hbox to 0pt{\hss $b~$\hss}}%
    \special{pa 1234 598}%
    \special{pa 1522 1174}%
    \special{da 0.050}%
    \special{sh 1.000}%
    \special{pa 1527 1127}%
    \special{pa 1522 1174}%
    \special{pa 1482 1150}%
    \special{pa 1527 1127}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 1.575in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1237 548}%
    \special{pa 1519 830}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1509 785}%
    \special{pa 1519 830}%
    \special{pa 1474 820}%
    \special{pa 1509 785}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.689in
    \rlap{\kern 1.378in\lower\graphtemp\hbox to 0pt{\hss $~b$\hss}}%
    \special{pa 1575 217}%
    \special{pa 1575 768}%
    \special{da 0.050}%
    \special{sh 1.000}%
    \special{pa 1600 728}%
    \special{pa 1575 768}%
    \special{pa 1550 728}%
    \special{pa 1600 728}%
    \special{fp}%
    \special{pa 1575 965}%
    \special{pa 1575 1201}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1600 1161}%
    \special{pa 1575 1201}%
    \special{pa 1550 1161}%
    \special{pa 1600 1161}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.083in
    \rlap{\kern 1.575in\lower\graphtemp\hbox to 0pt{\hss $~~~c$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 1.969in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1630 154}%
    \special{pa 1913 436}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1903 391}%
    \special{pa 1913 436}%
    \special{pa 1867 426}%
    \special{pa 1903 391}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.295in
    \rlap{\kern 1.772in\lower\graphtemp\hbox to 0pt{\hss $~b$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 1.969in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1913 548}%
    \special{pa 1630 830}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1676 820}%
    \special{pa 1630 830}%
    \special{pa 1641 785}%
    \special{pa 1676 820}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.689in
    \rlap{\kern 1.772in\lower\graphtemp\hbox to 0pt{\hss $a~$\hss}}%
    \special{pa 1969 571}%
    \special{pa 1969 807}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1994 768}%
    \special{pa 1969 807}%
    \special{pa 1944 768}%
    \special{pa 1994 768}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.689in
    \rlap{\kern 1.969in\lower\graphtemp\hbox to 0pt{\hss $~~~c$\hss}}%
    \special{pa 1916 598}%
    \special{pa 1628 1174}%
    \special{da 0.050}%
    \special{sh 1.000}%
    \special{pa 1668 1150}%
    \special{pa 1628 1174}%
    \special{pa 1623 1127}%
    \special{pa 1668 1150}%
    \special{fp}%
    \special{pa 1913 942}%
    \special{pa 1630 1224}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1676 1214}%
    \special{pa 1630 1224}%
    \special{pa 1641 1178}%
    \special{pa 1676 1214}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.083in
    \rlap{\kern 1.772in\lower\graphtemp\hbox to 0pt{\hss $~a$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.610in
    \rlap{\kern 0.000in\lower\graphtemp\hbox to 0pt{\hss $\begin{array}{c@{~}c@{~}l}E&=&\{a,b,c\}\!\!\!\!\!\!\!\\ \# &=& \emptyset\\ \emptyset & \vdash & a \\[-3mm] \emptyset & \vdash & b \\[-3mm] a & \vdash & c \\[-3mm] b & \vdash & c \\[-3mm] \end{array}$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 3.937in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 1.280in
    \rlap{\kern 3.937in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
    \special{pa 3937 965}%
    \special{pa 3937 1201}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3962 1161}%
    \special{pa 3937 1201}%
    \special{pa 3912 1161}%
    \special{pa 3962 1161}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.280in
    \rlap{\kern 4.134in\lower\graphtemp\hbox to 0pt{\hss $\#$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 4.331in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 1.280in
    \rlap{\kern 4.331in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
    \special{pa 4331 965}%
    \special{pa 4331 1201}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 4356 1161}%
    \special{pa 4331 1201}%
    \special{pa 4306 1161}%
    \special{pa 4356 1161}%
    \special{fp}%
    \hbox{\vrule depth1.378in width0pt height 0pt}%
    \kern 4.429in
  }%
}%
\centerline{\raise 1em\box\graph}
\caption{A system with {\em disjunctive causality} represented as an
event structure of \cite{Wi89}, a [higher dimensional] automaton in
which the dashed lines indicate that all three squares are filled in,
and a Petri net.  The last picture is the best representation of the
same system as a prime event structure \cite{NPW81,Wi89}. It requires
the decomposition of the event $c$, which is causally dependent on the
disjunction of $a$ and $b$, into two events $c_1$ and $c_2$, only one
of which may happen: $c_1$ being causally dependent only on $a$, and
$c_2$ on $b$.  This prime event structure is ST-bisimulation
equivalent to the original one, but not history preserving
bisimulation equivalent.}
\label{fig-disjunctive}
\vspace{1ex}\hrule
\end{figure}
representable as an event structure of \cite{Wi89}, but, up to history
preserving bisimulation equivalence, not as a prime event structure.

In \cite{GP04}, a generalisation of Winskel's event structures is
proposed that (up to history preserving bisimulation equivalence) is
equally expressive as Petri nets under the collective token
interpretation. Also a subclass of \emph{pure} event structures is
defined that matches the expressive power of configuration structures
and pure nets. An example of a pure Petri net and a pure event structure
as in \cite{GP04} that cannot be represented as an event structure of
\cite{Wi87a,Wi89} appears in Figure~\ref{fig-resolvable}.

\begin{figure}
%\input{resolvable}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \special{pn 8}%
    \special{ar 551 98 98 98 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.098in
    \rlap{\kern 0.551in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 551 197}%
    \special{pa 551 394}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 576 354}%
    \special{pa 551 394}%
    \special{pa 526 354}%
    \special{pa 576 354}%
    \special{fp}%
    \special{pa 453 591}%
    \special{pa 650 591}%
    \special{pa 650 394}%
    \special{pa 453 394}%
    \special{pa 453 591}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 0.551in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
    \special{pa 551 591}%
    \special{pa 551 787}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 576 748}%
    \special{pa 551 787}%
    \special{pa 526 748}%
    \special{pa 576 748}%
    \special{fp}%
    \special{ar 551 886 98 98 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 0.551in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{ar 157 886 98 98 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 0.157in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 157 984}%
    \special{pa 157 1181}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 182 1142}%
    \special{pa 157 1181}%
    \special{pa 132 1142}%
    \special{pa 182 1142}%
    \special{fp}%
    \special{pa 59 1378}%
    \special{pa 256 1378}%
    \special{pa 256 1181}%
    \special{pa 59 1181}%
    \special{pa 59 1378}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.280in
    \rlap{\kern 0.157in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{pa 482 955}%
    \special{pa 256 1181}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 301 1171}%
    \special{pa 256 1181}%
    \special{pa 266 1136}%
    \special{pa 301 1171}%
    \special{fp}%
    \special{ar 945 886 98 98 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 0.945in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 945 984}%
    \special{pa 945 1181}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 970 1142}%
    \special{pa 945 1181}%
    \special{pa 920 1142}%
    \special{pa 970 1142}%
    \special{fp}%
    \special{pa 846 1378}%
    \special{pa 1043 1378}%
    \special{pa 1043 1181}%
    \special{pa 846 1181}%
    \special{pa 846 1378}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.280in
    \rlap{\kern 0.945in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{pa 621 955}%
    \special{pa 846 1181}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 836 1136}%
    \special{pa 846 1181}%
    \special{pa 801 1171}%
    \special{pa 836 1136}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.098in
    \rlap{\kern 3.386in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 2.992in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 3358 126}%
    \special{pa 3020 464}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3065 454}%
    \special{pa 3020 464}%
    \special{pa 3030 419}%
    \special{pa 3065 454}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.295in
    \rlap{\kern 3.189in\lower\graphtemp\hbox to 0pt{\hss $a~$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 2.992in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 2992 531}%
    \special{pa 2992 846}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3017 807}%
    \special{pa 2992 846}%
    \special{pa 2967 807}%
    \special{pa 3017 807}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.689in
    \rlap{\kern 2.992in\lower\graphtemp\hbox to 0pt{\hss $c~~~$\hss}}%
    \special{pa 3333 204}%
    \special{pa 3045 780}%
    \special{da 0.050}%
    \special{sh 1.000}%
    \special{pa 3085 756}%
    \special{pa 3045 780}%
    \special{pa 3040 734}%
    \special{pa 3085 756}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.280in
    \rlap{\kern 3.386in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 3020 914}%
    \special{pa 3358 1252}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3348 1206}%
    \special{pa 3358 1252}%
    \special{pa 3312 1242}%
    \special{pa 3348 1206}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.083in
    \rlap{\kern 3.189in\lower\graphtemp\hbox to 0pt{\hss $~b$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 3.386in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 3386 138}%
    \special{pa 3386 453}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3411 413}%
    \special{pa 3386 453}%
    \special{pa 3361 413}%
    \special{pa 3411 413}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.295in
    \rlap{\kern 3.386in\lower\graphtemp\hbox to 0pt{\hss $c~~~$\hss}}%
    \special{pa 3386 610}%
    \special{pa 3386 1161}%
    \special{da 0.050}%
    \special{sh 1.000}%
    \special{pa 3411 1122}%
    \special{pa 3386 1161}%
    \special{pa 3361 1122}%
    \special{pa 3411 1122}%
    \special{fp}%
    \special{pa 3358 520}%
    \special{pa 3020 858}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3065 848}%
    \special{pa 3020 858}%
    \special{pa 3030 812}%
    \special{pa 3065 848}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.689in
    \rlap{\kern 3.189in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 3.780in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 3414 126}%
    \special{pa 3752 464}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3742 419}%
    \special{pa 3752 464}%
    \special{pa 3706 454}%
    \special{pa 3742 419}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.295in
    \rlap{\kern 3.583in\lower\graphtemp\hbox to 0pt{\hss $~b$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 3.780in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 3780 531}%
    \special{pa 3780 846}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3805 807}%
    \special{pa 3780 846}%
    \special{pa 3755 807}%
    \special{pa 3805 807}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.689in
    \rlap{\kern 3.780in\lower\graphtemp\hbox to 0pt{\hss $~~~c$\hss}}%
    \special{pa 3439 204}%
    \special{pa 3727 780}%
    \special{da 0.050}%
    \special{sh 1.000}%
    \special{pa 3731 734}%
    \special{pa 3727 780}%
    \special{pa 3687 756}%
    \special{pa 3731 734}%
    \special{fp}%
    \special{pa 3414 520}%
    \special{pa 3752 858}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3742 812}%
    \special{pa 3752 858}%
    \special{pa 3706 848}%
    \special{pa 3742 812}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.689in
    \rlap{\kern 3.583in\lower\graphtemp\hbox to 0pt{\hss $b~$\hss}}%
    \special{pa 3752 914}%
    \special{pa 3414 1252}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3459 1242}%
    \special{pa 3414 1252}%
    \special{pa 3424 1206}%
    \special{pa 3459 1242}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.083in
    \rlap{\kern 3.583in\lower\graphtemp\hbox to 0pt{\hss $a~$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.295in
    \rlap{\kern 1.890in\lower\graphtemp\hbox to 0pt{\hss $\begin{array}{c@{~}c@{~}l@{~}l}E&=&\{a,b,c\}\!\!\!\!\!\!\!\\ c &\vdash& \{a, b\}\\[-3mm]\emptyset &\vdash& X& \mbox{for }X\neq\{a,b\}\end{array}$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 4.409in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.689in
    \rlap{\kern 4.409in\lower\graphtemp\hbox to 0pt{\hss $\#$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 4.606in\lower\graphtemp\hbox to 0pt{\hss $\#$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 4.409in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 4.606in\lower\graphtemp\hbox to 0pt{\hss $\#$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.098in
    \rlap{\kern 4.606in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
    \special{pa 4571 169}%
    \special{pa 4445 422}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 4485 398}%
    \special{pa 4445 422}%
    \special{pa 4440 375}%
    \special{pa 4485 398}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.492in
    \rlap{\kern 4.803in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.689in
    \rlap{\kern 4.803in\lower\graphtemp\hbox to 0pt{\hss $\#$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.886in
    \rlap{\kern 4.803in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{pa 4642 169}%
    \special{pa 4750 386}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 4755 340}%
    \special{pa 4750 386}%
    \special{pa 4710 362}%
    \special{pa 4755 340}%
    \special{fp}%
    \hbox{\vrule depth1.378in width0pt height 0pt}%
    \kern 4.902in
  }%
}%
\centerline{\raise 1em\box\graph}
\caption{A system with {\em resolvable conflict} represented as a pure
  Petri net, a pure event structure as introduced in \cite{GP04}, and
  a [higher dimensional] automaton.  The events $a$ and $b$ are
  initially in conflict (only one of them may happen), but as soon as
  $c$ occurs this conflict is resolved. The last picture is the best
  representation of the same system as a prime event structure. It
  yields a system with two maximal runs, in one of which $c$ causes
  just $a$, and in the other just $b$. Again it is ST-bisimulation
  equivalent to the original, but not history preserving
  bisimulation equivalent. There is no event structure as in
  \cite{Wi87a,Wi89} that is history preserving bisimulation equivalent
  to the system above.}
\label{fig-resolvable}
\vspace{1ex}\hrule
\end{figure}

Figure~\ref{3mutex} shows a system represented as a Petri net, that
cannot be represented as a pure Petri net, or as an automaton under
the concurrent interpretation. 
\begin{figure}[htb]
\begin{center}
\begin{minipage}{2.5in}
%\input{3mutex}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \special{pn 8}%
    \special{ar 750 750 83 83 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.750in
    \rlap{\kern 0.750in\lower\graphtemp\hbox to 0pt{\hss $\bullet\bullet$\hss}}%
    \special{pa 667 500}%
    \special{pa 833 500}%
    \special{pa 833 333}%
    \special{pa 667 333}%
    \special{pa 667 500}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.417in
    \rlap{\kern 0.750in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{ar 908 566 250 250 2.619058 3.410024}%
    \special{sh 1.000}%
    \special{pa 632 532}%
    \special{pa 667 500}%
    \special{pa 680 545}%
    \special{pa 632 532}%
    \special{fp}%
    \special{ar 592 566 250 250 -0.268432 0.522535}%
    \special{sh 1.000}%
    \special{pa 851 669}%
    \special{pa 809 691}%
    \special{pa 807 644}%
    \special{pa 851 669}%
    \special{fp}%
    \special{ar 750 83 83 83 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.083in
    \rlap{\kern 0.750in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 750 167}%
    \special{pa 750 333}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 775 293}%
    \special{pa 750 333}%
    \special{pa 725 293}%
    \special{pa 775 293}%
    \special{fp}%
    \special{pa 1000 1167}%
    \special{pa 1167 1167}%
    \special{pa 1167 1000}%
    \special{pa 1000 1000}%
    \special{pa 1000 1167}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.083in
    \rlap{\kern 1.083in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{ar 833 1000 250 250 -1.570796 -0.000000}%
    \special{sh 1.000}%
    \special{pa 1108 960}%
    \special{pa 1083 1000}%
    \special{pa 1058 960}%
    \special{pa 1108 960}%
    \special{fp}%
    \special{ar 1017 834 250 250 1.637391 3.157143}%
    \special{sh 1.000}%
    \special{pa 741 870}%
    \special{pa 767 830}%
    \special{pa 791 870}%
    \special{pa 741 870}%
    \special{fp}%
    \special{ar 1417 1417 83 83 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 1.417in
    \rlap{\kern 1.417in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1358 1358}%
    \special{pa 1167 1167}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1177 1213}%
    \special{pa 1167 1167}%
    \special{pa 1213 1177}%
    \special{pa 1177 1213}%
    \special{fp}%
    \special{pa 333 1167}%
    \special{pa 500 1167}%
    \special{pa 500 1000}%
    \special{pa 333 1000}%
    \special{pa 333 1167}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.083in
    \rlap{\kern 0.417in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
    \special{ar 667 1000 250 250 -3.141593 -1.570796}%
    \special{sh 1.000}%
    \special{pa 627 725}%
    \special{pa 667 750}%
    \special{pa 627 775}%
    \special{pa 627 725}%
    \special{fp}%
    \special{ar 483 834 250 250 -0.015551 1.504201}%
    \special{sh 1.000}%
    \special{pa 542 1106}%
    \special{pa 500 1083}%
    \special{pa 538 1056}%
    \special{pa 542 1106}%
    \special{fp}%
    \special{ar 83 1417 83 83 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 1.417in
    \rlap{\kern 0.083in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 142 1358}%
    \special{pa 333 1167}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 287 1177}%
    \special{pa 333 1167}%
    \special{pa 323 1213}%
    \special{pa 287 1177}%
    \special{fp}%
    \hbox{\vrule depth1.500in width0pt height 0pt}%
    \kern 1.500in
  }%
}%
\centerline{\box\graph}\vspace{1ex}
\end{minipage}
\hfill
\begin{minipage}{2.5in}
\begin{center}
\begin{picture}(20,33.5)(50,0)
\put(60,33.5){\vector(0,-1){3}}
\put(60,30){\circle{1}}

\put(59.65,29.65){\vector(-1,-1){9.3}}
\put(52,25){$a$}
\put(50,20){\circle{1}}

\put(50,19.5){\vector(0,-1){9}}
\put(47.5,14){$b$}
\put(50,10){\circle{1}}

\put(50.35,9.65){\vector(1,-1){9.3}}
\put(52,3){$c$}
\put(60,0){\circle{1}}

\put(60,29.5){\vector(0,-1){9}}
\put(57.7,23){$b$}
\put(60,20){\circle{1}}

\put(59.65,19.65){\vector(-1,-1){9.3}}
\put(55,17.5){$a$}

\put(60.35,19.65){\vector(1,-1){9.3}}
\put(63,17.5){$c$}

\put(50.35,19.65){\vector(1,-1){9.3}}
\put(55,10.5){$c$}
\put(60,10){\circle{1}}

\put(69.65,19.65){\vector(-1,-1){9.3}}
\put(63,10.5){$a$}

\put(60,9.5){\vector(0,-1){9}}
\put(57.7,4){$b$}

\put(60.35,29.65){\vector(1,-1){9.3}}
\put(66,25){$c$}
\put(70,20){\circle{1}}

\put(70,19.5){\vector(0,-1){9}}
\put(71,14){$b$}
\put(70,10){\circle{1}}

\put(69.65,9.65){\vector(-1,-1){9.3}}
\put(66,3){$a$}
\end{picture}
\end{center}
\end{minipage}
\end{center}
\caption{A \emph{2-out-of-3 semaphore}, represented as a Petri net and as a
  higher dimensional automaton. In the latter, all six squares are
  supposed to be filled in, but the interior of the cube is not. Up to
  history preserving bisimulation equivalence this system cannot be
  represented as an automaton under the concurrent interpretation,
  because, due to the filled-in squares, the cube shape is unavoidable,
  and interior of the cube would by default be understood to be filled in.
  Hence the system can also not be represented as a pure Petri net.}
\label{3mutex}
\end{figure}

\subsubsection{Beyond Petri nets}

The final counterexample witnessing the completeness of the
expressiveness hierarchy of Figure~\ref{hierarchy} concerns the
process of Figure~\ref{race condition}, that is representable as a
higher dimensional automaton, and even as an ordinary automaton under
the concurrent interpretation, but not as a Petri net.

\begin{figure}[htb]
\begin{center}
\begin{picture}(20,38.5)(50,-5)
\put(60,33.5){\vector(0,-1){3}}
\put(60,30){\circle{1}}

\put(59.65,29.65){\vector(-1,-1){9.3}}
\put(53,26){$a$}
\put(50,20){\circle{1}}

\put(49.65,19.65){\vector(-1,-3){4.65}}
\put(45,12){$b$}
\put(45,5){\circle{1}}

\put(45,4.5){\vector(0,-1){9}}
\put(42.2,-1){$d$}
\put(45,-5){\circle{1}}

\put(45.35,4.65){\vector(3,-1){14.2}}
\put(50,0){$c$}

\put(50,19.5){\vector(0,-1){9}}
\put(50.8,15){$c$}
\put(50,10){\circle{1}}

\put(50.35,9.65){\vector(1,-1){9.3}}
\put(55,5.5){$b$}
\put(60,0){\circle{1}}

\put(60,29.5){\vector(0,-1){9}}
\put(57.7,23){$c$}
\put(60,20){\circle{1}}


\put(59.65,19.65){\vector(-1,-1){9.3}}
\put(55,12.5){$a$}

\put(60.35,19.65){\vector(1,-1){9.3}}
\put(63,12.5){$b$}


\put(60.35,29.65){\vector(1,-1){9.3}}
\put(65,26){$b$}
\put(70,20){\circle{1}}

\put(70.35,19.65){\vector(1,-3){4.65}}
\put(73.4,12){$a$}
\put(75,5){\circle{1}}

\put(75,4.5){\vector(0,-1){9}}
\put(75.7,-1){$e$}
\put(75,-5){\circle{1}}

\put(74.65,4.65){\vector(-3,-1){14.2}}
\put(68,0){$c$}

\put(70,19.5){\vector(0,-1){9}}
\put(67.5,15){$c$}
\put(70,10){\circle{1}}

\put(69.65,9.65){\vector(-1,-1){9.3}}
\put(63,5.5){$a$}
\end{picture}
\end{center}
\caption{A process, represented as an ordinary automaton under the
  concurrent interpretation, that, up to history preserving
  bisimulation equivalence, cannot be represented as a Petri net.}
\label{race condition}
\end{figure}
\noindent
  The process displayed in Figure~\ref{race condition} was implemented
  during my presentation at EXPRESS
  2004. Two computer scientists $A$ and $B$ were travelling from one
  end of the podium to the other. Their task to was perform the
  actions $a$ resp.\ $b$ of crossing a line on the podium. Due to
  strategic placing of obstacles, the only place were this was
  possible was at a narrow opening between the obstacles that had room
  for only one of the scientists $A$ and $B$ at a time. This made the
  actions $a$ and $b$ mutually exclusive, in the sense that they could
  not occur simultaneously. A third computer scientist, $C$, was
  assigned the task $c$ of removing an obstacle that caused the
  bottleneck to exists.  The action $c$ was executed causally
  independent of $a$ and $b$. The actions $a$ and $b$ were mutually
  exclusive only until $c$ occurred, after which they became causally
  independent.  Finally, a fourth participant was assigned the task of
  making a statement when $a$ and $b$ had both occurred before the
  action $c$ started. This statement was going to be $d$ in case $A$
  passed the bottleneck before $B$ did, and $e$ in case $B$ passed the
  bottleneck before $A$ did. Hearing this statement would prevent
  computer scientist $C$ from carrying out the action $c$. The
  resulting process is described by the automaton above, in which all
  five squares are filled in.

In order to represent the process of Figure~\ref{race condition}, up
to history preserving bisimulation equivalence, as a Petri net, there
must be a single transition representing the action $a$, regardless of
whether it is scheduled before or after $b$ or $c$. This because of
the concurrency inherent in the example. The same holds for $b$.
However, in a Petri net, firing just these two transitions labelled
$a$ and $b$ necessarily leads to a unique state, independent of the
order in which $a$ and $b$ occur. This is in contradiction with the
fact that the process under consideration has two states reachable by
doing only $a$ and $b$, in which different further actions are
possible.

\subsection{Comparisons modulo other notions of equivalence}

If I compare the models of Figure~\ref{hierarchy} up to hereditary
history preserving bisimulation equivalence the same hierarchy
results. This because all translations used in Section~\ref{soundness}
even preserve hereditary history preserving bisimulation equivalence.
If I compare them merely up to interleaving bisimulation equivalence,
all models turn out to be equally expressive.  This because every
higher dimensional automaton is trivially interleaving bisimulation
equivalent to the 1-dimensional automaton resulting from ignoring its
higher dimensional cells, and to the unfolding of that 1-dimensional
automaton into a tree.

If I compare the models up to ST-bisimulation equivalence, the model
of synchronisation trees is still less expressive than that of event
structures, as explained in Section~\ref{completeness}.  I conjecture
that all models of Figure~\ref{hierarchy} other than synchronisation
trees are equally expressive, in the sense that any process
representable in any of the models can be translated into an
ST-bisimulation equivalent prime event structure.  For configuration
structures this is Theorem~1 in \cite{GP95}. My conjecture is that
this result extends to higher dimensional automata; in other words,
that up to ST-bisimulation equivalence the prime event structures have
universal expressivity.

%\bibliography{../Stanford/lib/biblio/glabbeek,../Stanford/lib/abbreviations,../Stanford/lib/dbase,../Stanford/lib/new}
\begin{thebibliography}{10}
\newcommand{\enquote}[1]{``#1''}

\bibitem{BW90}
Baeten, J.C.M. and W.P.~Weijland, \enquote{Process Algebra,} Cambridge Tracts in
  Theoretical Computer Science 18, Cambridge University Press, 1990.

\bibitem{Bz87}
Bednarczyk, M., \enquote{Categories of asynchronous systems,} Ph.D. thesis,
  Computer Science, University of Sussex, Brighton (1987).\\
Available at \url{ftp://ftp.ipipan.gda.pl/marek/phd.ps.gz}.

\bibitem{Bz91}
Bednarczyk, M., \emph{Hereditary history preserving bisimulation, or what is
  the power of the future perfect in program logics}, Technical report, Polish
  Academy of Sciences, Gdansk (1991).\\
Available at \url{ftp://ftp.ipipan.gda.pl/marek/historie.ps.gz}.

\bibitem{BDKP91}
Best, E., R.~Devillers, A.~Kiehn and L.~Pomello, \emph{Concurrent bisimulations
  in {P}etri nets}, Acta Informatica \textbf{28} (1991), pp.~231--264.

\bibitem{Bo90}
Boudol, G., \emph{Flow event structures and flow nets}, in: I.~Guessarian,
  editor, \textsl{Semantics of Systems of Concurrent Processes, Proceedings LITP
  Spring School on Theoretical Computer Science, {\rm La Roche Posay, France}},
   \rm LNCS  \textbf{469} (1990), pp. 62--95.

\bibitem{vG88a}
Glabbeek, R.J.~van, \emph{An operational non-interleaved process graph semantics
  of {CCSP} \rm (abstract)}, in: E.-R. Olderog, U.~Goltz and R.J.~van Glabbeek,
  editors, \textsl{Combining Compositionality and Concurrency, {\rm Summary of a
  GMD-Workshop, K\"onigswinter, March 1988}}, Arbeitspapiere der GMD 320
  (1988), pp. 18--19.

\bibitem{vG90}
Glabbeek, R.J.~van, \emph{The refinement theorem for {ST}-bisimulation semantics},
  in: M.~Broy and C.B.~Jones, editors, \textsl{{\rm Proceedings IFIP TC2 Working
  Conference on} Programming Concepts and Methods, {\rm Sea of Gallilee,
  Israel}} (1990), pp. 27--52, available at
  \url{http://kilby.stanford.edu/~rvg/pub/STbisimulation.pdf}.

\bibitem{vG91}
Glabbeek, R.J.~van, \emph{Bisimulations for higher dimensional automata}, email
  message (July 7, 1991), available at \url{http://theory.stanford.edu/~rvg/hda}.

\bibitem{vG96h}
Glabbeek, R.J.~van, \emph{History preserving process graphs}, draft, available
  at \url{http://kilby.stanford.edu/~rvg/pub/history.draft.dvi}
  (1996).

\bibitem{GG01}
Glabbeek, R.J.~van and U.~Goltz, \emph{Refinement of actions and equivalence
  notions for concurrent systems}, Acta Informatica \textbf{37} (2001),
  pp.~229--327, available at {\tt
  \url{http://boole.stanford.edu/pub/refinement.ps.gz}}.

\bibitem{GP95}
Glabbeek, R.J.~van and G.D.~Plotkin, \emph{Configuration structures (extended
  abstract)}, in: D.~Kozen, editor, \textsl{{\rm Proceedings $10^{th}$ Annual
  IEEE Symposium on} Logic in Computer Science, {\rm LICS'95, San Diego, USA}}
  (1995), pp. 199--209, available at 
  {\tt \url{http://boole.stanford.edu/pub/conf.ps.gz}}.

\bibitem{GP04}
Glabbeek, R.J.~van and G.D.~Plotkin, \emph{Event structures for resolvable
  conflict}, in: V.~Koubek and J.~Kratochvil, editors, \sl{{\rm Proceedings
  $29^{th}$ International Symposium on} Mathematical Foundations of Computer
  Science, {\rm MFCS 2004, Prague, Czech Republic}}, \rm LNCS (August 2004),\\
  available at {\tt \url{http://boole.stanford.edu/pub/resolv.ps.gz}}.

\bibitem{GV87}
Glabbeek, R.J.~van and F.W.~Vaandrager, \emph{Petri net models for algebraic
  theories of concurrency (extended abstract)}, in: J.W.~de Bakker, A.J.~Nijman and
  P.C.~Treleaven, editors, \textsl{{\rm Proceedings} PARLE, Parallel Architectures
  and Languages Europe, {\rm Eindhoven, The Netherlands, June 1987, Vol. II:
  Parallel Languages}},  \rm LNCS  \textbf{259} (1987), pp. 224--242, available
  at \url{http://kilby.stanford.edu/~rvg/pub/petri.pdf}.

\bibitem{GV97}
Glabbeek, R.J.~van and F.W.~Vaandrager, \emph{The difference between splitting in
  $n$ and $n+1$}, Information and Computation \textbf{136} (1997),
  pp.~109--142, available at {\tt \url{http://boole.stanford.edu/pub/split.pdf}}.

\bibitem{GV03}
Glabbeek, R.J.~van and F.W.~Vaandrager, \emph{Bundle event structures and {CCSP}},
  in: R.~Amadio and D.~Lugiez, editors, \textsl{{\rm Proceedings} CONCUR 2003,
  {\rm 14$^{\it th}$ International Conference on} Concurrency Theory, {\rm
  Marseille, France, September 2003}},  \rm LNCS  \textbf{2761} (2003), pp.
  57--71, available at \url{http://boole.stanford.edu/pub/bundle.ps.gz}.

\bibitem{Lk92}
Langerak, R., \enquote{Transformations and Semantics for LOTOS,} Ph.D. thesis,
  Department of Computer Science, University of Twente (1992).

\bibitem{MMS92}
Meseguer, J., U.~Montanari and V.~Sassone, \emph{On the semantics of {Petri}
  nets}, in: W.~Cleaveland, editor, {\rm Proceedings CONCUR
  '92, Second International Conference on {\sl Concurrency Theory}, {\rm
  Stony Brook, NY, USA}},  \rm LNCS  \textbf{630} (1992), pp. 286--301.

\bibitem{Mi80}
Milner, R., \enquote{A Calculus of Communicating Systems,}  \rm LNCS
  \textbf{92}, Springer, 1980.

\bibitem{NPW81}
Nielsen, M., G.D.~Plotkin and G.~Winskel, \emph{Petri nets, event structures and
  domains, part {I}}, Theoretical Computer Science \textbf{13} (1981),
  pp.~85--108.

\bibitem{NW96}
Nielsen, M. and G.~Winskel, \emph{Petri nets and bisimulation}, Theoretical
  Computer Science \textbf{153} (1996), pp.~211--244.

\bibitem{Pap86}
Papadimitriou, C., \enquote{The Theory of Database Concurrency Control,}
  Computer Science Press, 1986.

\bibitem{Pr91a}
Pratt, V.R., \emph{Modeling concurrency with geometry}, in:
  \textsl{Proc. 18th Ann. ACM Symposium on Principles of Programming
  Languages} (1991), pp. 311--322, available at
  \url{http://boole.stanford.edu/pub/cg.ps.gz}.

\bibitem{Chu}
Pratt, V.R., \emph{Chu spaces}, a summary and large collection of papers
  available at \url{http://chu.stanford.edu/} (1993--2002).

\bibitem{RT88}
Rabinovich, A. and B.A.~Trakhtenbrot, \emph{Behavior structures and nets},
  Fundamenta Informaticae \textbf{11} (1988), pp.~357--404.

\bibitem{Ser51}
Serre, J., \emph{Homology singuli\`ere des espaces fibr\'es. application},
  Ph.D. thesis, \'Ecole Normale Sup\'erieure (1951).

\bibitem{Sh85}
Shields, M.W., \emph{Concurrent machines}, The Computer Journal \textbf{28}
  (1985), pp.~449--465.

\bibitem{Sta89}
Stark, E.W., \emph{Concurrent transition systems}, Theoretical Computer Science
  \textbf{64} (1989), pp.~221--269.

\bibitem{Wi87a}
Winskel, G., \emph{Event structures}, in: W.~Brauer, W.~Reisig and
  G.~Rozenberg, editors, \textsl{Petri Nets: Applications and Relationships to
  Other Models of Concurrency, Advances in Petri Nets 1986, Part II;
  Proceedings of an Advanced Course, {\rm Bad Honnef, September 1986}},  \rm
  LNCS  \textbf{255} (1987), pp. 325--392.

\bibitem{Wi89}
Winskel, G., \emph{An introduction to event structures}, in: J.W.~de~Bakker,
  W.P.~d. Roever and G.~Rozenberg, editors, \textsl{REX School and Workshop on
  Linear Time, Branching Time and Partial Order in Logics and Models for
  Concurrency, {\rm Noordwijkerhout, The Netherlands, May/June 1988}},  \rm
  LNCS  \textbf{354} (1989), pp. 364--397.

\bibitem{WN95}
Winskel, G. and M.~Nielsen, \emph{Models for concurrency}, in: \textsl{Handbook
  of Logic in Computer Science}, Oxford University Press, 1995 pp. 1--148.
\vspace{-2em}

\end{thebibliography}
\def\refname{\normalsize Bibliography on Higher Dimensional Automata
{\rm (besides [22] and [8])}}
\hypertarget{bibliography}{}
\begin{thebibliography}{10}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}
\refstepcounter{enumiv}

\bibitem{Buc96}
Buckland, R., \emph{Choice as a first class citizen}, in: M.~Orgun and
  E.~Ashcroft, editors, \emph{\rm Proceedings {\sl Intensional Programming I}}
  (1996), pp. 249--259.

\bibitem{BJV02}
Buckland, R., M.~Johnson and D.~Verity, \emph{On the specification of higher
  dimensional automata}, Electronic Notes in Theoretical Computer Science
  \textbf{68(1)} (2002), pp.~1--11.

\bibitem{CS96}
Cattani, G.L. and V.~Sassone, \emph{Higher dimensional transition systems},
  in: \emph{\rm Proceedings LICS '96, Eleventh Annual IEEE Symposium on {\sl
  Logic in Computer Science}, New Brunswick, USA} (1996), pp. 55--62.
  \\Available at \url{ftp://ftp.cl.cam.ac.uk/users/glc25/hdts.dvi.gz}.

\bibitem{Cri95}
Cridlig, R., \emph{Semantic analysis of shared-memory concurrent languages
  using abstract model-checking}, in: \emph{\rm Proceedings PEPM 1995, ACM
  SIGPLAN Symposium on {\sl Partial Evaluation and Semantics-Based Program
  Manipulation}, La Jolla, USA, June 1995} (1995), pp. 214--225.\\Available
  at \url{http://portal.acm.org/citation.cfm?doid=215465.215577}.

\bibitem{Cri96}
Cridlig, R., \emph{Implementing a static analyzer of concurrent programs:
  Problems and perspectives}, in: M.~Dam, editor, \emph{\rm Selected Papers of
  {\sl Analysis and Verification of Multiple-Agent Languages}, 5th LOMAPS
  Workshop, Stockholm, Sweden, June 1996},  \rm LNCS  \textbf{1192} (1997), pp.
  244--259.

\bibitem{CG93}
Cridlig, R. and E.~Goubault, \emph{Semantics and analysis of {Linda}-based
  languages}, in: \emph{\rm Proceedings WSA '93, 3rd International Workshop on
  {\sl Static Analysis}, Padova, Italy, September 1993},  \rm LNCS
  \textbf{724} (1993), pp. 72--86.\\ Available from
  \url{http://www.di.ens.fr/~goubault/GOUBAULTpapers.html}.

\bibitem{Faj00}
Fajstrup, L., \emph{Loops, ditopology and deadlocks}, Mathematical Structures
  in Computer Science \textbf{10(4)} (2000), pp.~459--480.

\bibitem{FGR98}
Fajstrup, L., E.~Goubault and M.~Raussen, \emph{Detecting deadlocks in
  concurrent systems}, in: D.~Sangiorgi and R.~de~Simone, editors, \emph{\rm
  Proceedings CONCUR '98, 9th International Conference on {\sl Concurrency
  Theory}, Nice, France, September 1998},  \rm LNCS  \textbf{1466} (1998), pp.
  332--347.\\ Available from
  \url{http://www.di.ens.fr/~goubault/GOUBAULTpapers.html}.

\bibitem{Gau00b}
Gaucher, P., \emph{From concurrency to algebraic topology}, Electronic Notes in
  Theoretical Computer Science \textbf{39(2)} (2000).\\ Available at
  \url{http://www.pps.jussieu.fr/~gaucher/expose.ps.gz}.

\bibitem{Gau00a}
Gaucher, P., \emph{Homotopy invariants of higher dimensional categories and
  concurrency in computer science}, Mathematical Structures in Computer Science
  \textbf{10(4)} (2000), pp.~481--524.\\ Available at
  \url{http://www.pps.jussieu.fr/~gaucher/homotopie\_cat.ps.gz}.

\bibitem{Gau01}
Gaucher, P., \emph{Combinatorics of branchings in higher dimensional automata},
  Theory and Applications of Categories \textbf{8(12)} (2001), pp.~324--376.
  \\ Available at \url{http://www.pps.jussieu.fr/~gaucher/coin.ps.gz}.

\bibitem{Gau02a}
Gaucher, P., \emph{About the globular homology of higher dimensional automata},
  Cahiers de Topologie et G\'eom\'etrie Diff\'erentielle Cat\'egoriques
  \textbf{XLIII(2)} (2002), pp.~107--156. At
  \url{http://www.pps.jussieu.fr/~gaucher/sglob.ps.gz}.

\bibitem{Gau02b}
Gaucher, P., \emph{Investigating the algebraic structure of dihomotopy types},
  Electronic Notes in Theoretical Computer Science \textbf{52(2)} (2002).\\
  Available at \url{http://www.pps.jussieu.fr/~gaucher/dihomotopy.ps.gz}.

\bibitem{Gau03a}
Gaucher, P., \emph{The branching nerve of {HDA} and the {Kan} condition},
  Theory and Applications of Categories \textbf{11(3)} (2003), pp.~75--106.\\
  Available at \url{http://www.pps.jussieu.fr/~gaucher/fibrantcoin.ps.gz}.

\bibitem{Gau03b}
Gaucher, P., \emph{A model category for the homotopy theory of concurrency},
  Homology, Homotopy and Applications \textbf{5(1)} (2003), pp.~549--599.\\
  Available at \url{http://www.pps.jussieu.fr/~gaucher/modelflow.ps.gz}.

\bibitem{GG03}
Gaucher, P. and E.~Goubault, \emph{Topological deformation of higher
  dimensional automata}, Homology, Homotopy and Applications \textbf{5(2)}
  (2003), pp.~39--82.\\ Available at
  \url{http://www.pps.jussieu.fr/~gaucher/diCW.ps.gz}.

\bibitem{Gou93}
Goubault, E., \emph{Domains of higher-dimensional automata}, in: E.~Best,
  editor, \emph{\rm Proceedings CONCUR '93, 4th International Conference on
  {\sl Concurrency Theory}, Hildesheim, Germany, August 1993},  \rm LNCS
  \textbf{715} (1993), pp. 293--307.\\ Available from
  \url{http://www.di.ens.fr/~goubault/GOUBAULTpapers.html}.

\bibitem{Gou95a}
Goubault, E., \emph{The geometry of concurrency}, Ph.D. thesis, \'Ecole Normale
  Sup\'erieure (1995), \url{http://www.di.ens.fr/~goubault/papers/these.ps.gz}.

\bibitem{Gou95b}
Goubault, E., \emph{Schedulers as abstract interpretations of
  higher-dimensional automata}, in: \emph{\rm Proceedings PEPM 1995, ACM
  SIGPLAN Symposium on {\sl Partial Evaluation and Semantics-Based Program
  Manipulation}, La Jolla, USA, June 1995} (1995), pp. 134--145.\\ Available
  from \url{http://www.di.ens.fr/~goubault/GOUBAULTpapers.html}.

\bibitem{Gou96a}
Goubault, E., \emph{Durations for truly-concurrent actions}, in: H.~R. Nielson,
  editor, \emph{\rm Proceedings {\sl Programming Languages and Systems} -
  ESOP'96, 6th European Symposium on {\sl Programming}, Link{\"o}ping, Sweden,
  April 1996},  \rm LNCS  \textbf{1058} (1996), pp. 173--187, available as {\it
  Transitions take time} from
  \url{http://www.di.ens.fr/~goubault/GOUBAULTpapers.html}.

\bibitem{Gou96b}
Goubault, E., \emph{A semantic view on distributed computability and
  complexity}, in: \emph{\rm Proceedings 3rd {\sl Theory and Formal Methods}
  Workshop} (1996).\\ Available from
  \url{http://www.di.ens.fr/~goubault/GOUBAULTpapers.html}.

\bibitem{Gou00}
Goubault, E., \emph{Geometry and concurrency: a user's guide}, Mathematical
  Structures in Computer Science \textbf{10(4)} (2000), pp.~411--425.\\
  Available from \url{http://www.di.ens.fr/~goubault/GOUBAULTpapers.html}.

\bibitem{Gou02}
Goubault, E., \emph{Cubical sets are generalized transition systems} (2002),
  available from \url{http://www.di.ens.fr/~goubault/GOUBAULTpapers.html}.

\bibitem{GJ92}
Goubault, E. and T.P.~Jensen, \emph{Homology of higher dimensional automata}, in:
  R.~Cleaveland, editor, \emph{\rm Proceedings CONCUR '92, Third International
  Conference on {\sl Concurrency Theory}, Stony Brook, NY, USA, August 1992},
  \rm LNCS  \textbf{630} (1992), pp. 254--268.\\ Available from
  \url{http://www.di.ens.fr/~goubault/GOUBAULTpapers.html}.

\bibitem{GR02}
Goubault, E. and M.~Raussen, \emph{Dihomotopy as a tool in state space
  analysis}, in: \emph{\rm Proceedings LATIN '02, 5th Latin American Symposium
  on {\sl Theoretical Informatics}, Cancun, Mexico}, 2002, pp. 16--37.\\
  Available from \url{http://www.di.ens.fr/~goubault/GOUBAULTpapers.html}.

\bibitem{Gun94}
Gunawardena, J., \emph{Homotopy and concurrency}, Bulletin of the EATCS
  \textbf{54} (1994), pp.~184--193, also in: G. Paun, G. Rozenberg and A.
  Salomaa, editors, {\sl Current trends in Theoretical Computer Science:
  Entering the 21st Century}, World Scientific, 2001. \\ Available at
  \url{http://www.jeremy-gunawardena.com/papers/hac.pdf}.

\bibitem{Lan93}
Lanzmann, E., \emph{Automates d'ordre sup\'erieur}, {Master's} thesis,
  Universit\'e d'Orsay (1993).

\bibitem{Pr00a}
Pratt, V.R., \emph{Higher dimensional automata revisited}, Mathematical
  Structures in Computer Science \textbf{10(4)} (2000), pp.~525--548.
  \\Available at \url{http://boole.stanford.edu/pub/hda.ps.gz}.

\bibitem{Pr02a}
Pratt, V.R., \emph{Transition and cancellation in concurrency and branching
  time}, Mathematical Structures in Computer Science \textbf{13(4)} (2003),
  pp.~485--529.\\Available at
  \url{http://boole.stanford.edu/pub/seqconc.ps.gz}.

\bibitem{Rau00}
Raussen., M., \emph{On the classification of dipaths in geometric models for
  concurrency}, Mathematical Structures in Computer Science \textbf{10(4)}
  (2000), pp.~427--457.

\bibitem{Sok02}
Sokolowski, S., \emph{A case for po-manifolds: in chase after a good
  topological model for concurrency}, Electronic Notes in Theoretical Computer
  Science \textbf{81} (2003), at
  \url{ftp://ftp.ipipan.gda.pl/stefan/reports/73-pomanif.ps.gz}.

\bibitem{Tak95}
Takayama, Y., \emph{Parallelization of concurrent processes in higher
  dimensional automata}, in: \emph{\rm Proceedings RIMS Workshop on {\sl Term
  Rewriting Systems and its Applications}, RIMS Kyoto University}, 1995.

\bibitem{Tak96a}
Takayama, Y., \emph{Extraction of concurrent processes from higher dimensional
  automata}, in: H.~Kirchner, editor, \emph{\rm Proceedings CAAP '96, 21st
  International Colloquium on {\sl Trees in Algebra and Programming},
  Link{\"o}ping, Sweden, April 1996},  \rm LNCS  \textbf{1059} (1996), pp.
  72--86.

\bibitem{Tak96b}
Takayama, Y., \emph{Towards cycle filling as parallelization}, in: \emph{\rm
  Proceedings 4th International RIMS Workshop on {\sl Concurrency Theory and
  Applications}, RIMS Kyoto University}, 1996.

\end{thebibliography}
\end{document}
