Let 
be a class of processes. I assume that for each process
a set 
of (partial) runs is defined, equipped
with a prefix ordering 
, and that with each run (or
execution) 
is associated its observable content 
.
A first idea of what could be the branching structure of a process 
, is the pomset with representative 
. This I
will call the strict branching structure of p, as it
corresponds with the idea that the branching of all, possibly
indistinguishable, runs is taken into account. In order to
arrive at a less strict definition, one needs to identify certain
runs.
This is the intermediate variant of three possible generalizations of
the concept of a congruence from algebras to algebraic structures with
relations. A strong congruence would even require that 
, so
that 
can simply be defined by 
. A weak congruence
on the other hand doesn't require anything for 
, and
needs to be defined by 
.
Obviously a coarsest congruence on a pomset exists, as the union of arbitrary many congruences is again a congruence. The following observations are meant as tool for deciding whether or not a model or equivalence respects branching time.
Proof: This follows immediately from the following two facts, whose proofs are straightforward.
is the coarsest and 
any congruence on an
elpo 
, and 
is the coarsest congruence on
, then
.
and 
is a congruence on
, then there is a congruence 
on 
such
that 
. Moreover, 
is the
coarsest iff 
is. 
