Classifying models of concurrency
A model of concurrency usually consist of a set (domain) whose
elements denote concurrent systems, together with some structure. The
structure takes the shape of a collection of operators, turning
the domain into an algebra (a process algebra), optionally
in combination with a collection of predicates, or a collection
of morphisms between the elements, making the domain into a
category. Classifying models of concurrency with respect
to the kind of mathematical objects that are used to represent
processes, I find it convenient to distinguish 5 types of models.
-
GRAPH oriented models. Here a concurrent system is
represented by a process graph, or state-transition
diagram, also called automaton. Or by a richer
graph-like object. A variant are labelled transition systems,
in which a concurrent system is not denoted by a whole graph, but
by a vertex in a graph; the entire domain is then one large graph.
-
NET oriented models, in which a concurrent system is
represented by a Petri net, or a net-like object.
-
EVENT orient models, in which a concurrent system is represented by
a set of events (action occurrences) together with some structure
on this set, determining the relations between the events. This
class of models includes the various brands of event structures.
-
EXPLICIT models. In the models mentioned above, a concurrent system
is not really modeled as a single graph/net/event structure,
but actually by an equivalence class of such objects. Thus
different graphs/nets/etc. represent the same concurrent system.
Which equivalence relation is divided out is partly determined by
which properties of concurrent systems are considered to be
relevant. The choice of equivalence is important in proving the
correctness of specifications w.r.t. implementations.
The explicit models on the other hand are not quotient
models, but offer one `explicit' object to represent a system.
This object is usually a mathematically coded set of the relevant
properties, or of the possible executions, of the represented system.
-
TERM models. Here a concurrent system is represented as a term in a
system description language. Well known system description
languages are CCS and CSP. Instead of speaking of term models as
type of model, one could say that systems can be denoted either
syntactically (by means of an expression in a language) or
semantically (in a model of type 1-4). The notion of a term model
is the result of unifying these views. Usually, the meaning of an
expression is given by means of a mapping from the used set of terms
into another model. This mapping constitutes the semantics of the
used language.
Besides w.r.t. type (as above), models of concurrency can be
classified w.r.t.
-
the equivalence relation that is divided out (explicitly in
term, graph, net and event oriented models; implicitly in explicit
models),
-
the scope of the model (which systems can be represented and
which cannot)
-
and the chosen structure (the selection of operators,
relations and morphisms defined on the model).
As there are canonical translations between the various types of
models, models of different type can be compared w.r.t. scope,
structure and level of identification.
Rob van Glabbeek
rvg@CS.Stanford.EDU