Petri Nets, Configuration Structures, Propositional Theories
		  and History Preserving Process Graphs

	   Summary of a talk given at Sloss Dagstuhl, May 1996


			     Rob van Glabbeek
			   Stanford University

Translations between several models of concurrency are reviewed cq.
proposed. The models considered capture causality and branching time
(and their interplay) and this behaviour is preserved by the translations.
  
  ._______.                     ._______.      ._______.      ._______.
  |       |      		|       |      |       |      | Trans.|
  | Petri |      		| Higher|      |Process|      |systems|
  | nets  |<------------------->| dim.  |      |graphs |      |  with |
  |       |      		| autom.|      |       |      | indep.|
  |_______|      		|_______|      |_______|      |_______|
      |                             |              |              |
      | unfolding                   |              |  unfolding   |
      |                             |              |              |
  .___V___.      ._______.      .___V___.      .___V___.      .___V___.      
  |       |      | Prop. |      |       |      | Hist. |      | Trans.|      
  |  (1-) |      |  th.  |      | (ST-) |      | pres. |      |systems|      
  | Occur.|<---->|-------|<---->| Conf. |<---->|process|<-----|  with |
  | nets  |      | Event |      |  str. |      |graphs |      | indep.|      
  |_______|      |  str. |      |_______|      |_______|      |_______|
		 `-------'

Starting point is the work of Nielsen, Plotkin and Winskel, in which safe
Petri nets are translated, through the intermediate stages of occurrence
nets, prime event structures with a binary conflict relation, and their
families of configurations, into a class of Scott domains.
	The resulting Scott domains, which were originally not intended to
denote (separate) concurrent systems, can easily be regarded as transition
systems, or process graphs. Therefore I like to see the connection between
safe Petri nets and these domains as one between a class of nets and a
class of process graphs. These graphs capture causality through confluence
of squares of transitions. This gives rise to the question which process
graphs can be regarded as modelling causal independence through transition
squares. My answer is `all of them', and I propose an unfolding of
arbitrary graphs into the so-called history preserving process ones, that
preserves this structure. History preserving process graphs generalise
the Scott domains originating from prime, or even general, event structures.
	Several brands of transition systems enriched with some auxiliary
structure to capture causality have been proposed as models of concurrency,
cf. the concurrent transition systems of Stark and Droste, the
asynchronous transition systems of Shields and Bednarczyk and the
transition systems with independence of Nielsen and Winskel. In each of
these cases the added structure does not yield greater expressiveness:
after a suitable behaviour preserving unfolding, the causalities expressed
by this added structure are completely determined by the underlying
transition system, which forms always a history preserving process graph.
	The families of configurations of (prime) event structures are
given as sets of sets of events satisfying certain closure properties.
The model of configuration structures is obtained by dropping all closure
conditions. ST-configuration structures are a further generalisation in
which the configurations may contain events `partially' (in case they are
currently being executed). Event automata, studied by Pinna and Poigne',
fit between configuration structures and ST-configuration structures. 
Through appropriate translations these are shown to be equally expressive
as the so-called configuration-deterministic process graphs. Graphs which
are not configuration deterministic do not correspond to nets or
event-oriented models.
	Further translations are provided between general S/T-nets and
ST-configuration structures, as well as the so-called higher dimensional
automata. These three models are more general then process graphs or the
mentioned transition systems with extra structure to capture causality,
which can be regarded as one and two dimensional automata, respectively.
The ordinary configuration structures correspond with Petri nets without
self-loops. Propositional theories, which can be regarded as a
generalisation and abstraction of event structures, appear as a stepping
stone in the translation from configuration structures to nets.
	The mentioned transitions involving nets fit with the so-called
collective token interpretation, as opposed to the individual token
interpretation of nets, which is needed to justify the unfolding of
S/T-nets into occurrence nets proposed by Sassone, Meseguer and Montanari.
Under the collective token interpretation, a less ambitious unfolding
into so-called 1-occurrence nets is called for.
        My transitions are consistent with the correspondence between flow
nets and flow event structures proposed by Boudol and Castellani, and with
the correspondence between elementary net systems and elementary transition
systems proposed by Ehrenfeucht, Rozenberg, Nielsen and Thiagarajan.