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.