\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 ii$, is now called the $(j-1)^{th}$ transition.
Hence, first leaving out the $j^{th}$ and then the $i^{th}$, with
$i1$. 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)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)$ 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 $i0$ 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}
*