next up previous
Next: Other models Up: What is branching time Previous: The branching structure

The case of labelled transition spaces with and without tau

In this section I will instantiate the general definition of branching time from the previous section for equivalences on models of concurrency that can be regarded as labelled transition spaces.

 

Notation: Write for and for .
The elements of represent the processes we are interested in, and means that process p can evolve into process q while performing the action a. I use the word `space' instead of `system' to emphasize that the elements of an LTS are all systems under investigation, and not merely the states of a single system.

 

It remains to determine the observable content of a run. In case all actions are observable, let . In case , where denotes an internal or unobservable action, the observable content of a run e is the same sequence, but from which all 's are removed. This completes the definition of the branching structure of members of an LTS.

 

 

In [5] is has been established that weak back and forth bisimulation equivalence coincides with branching bisimulation equivalence. Hence is follows that

 

If in Definition 3 the coarsest congruence would be replaced by the coarsest weak congruence, the resulting `branching structure' would have a distinct linear time flavour, as it would be nothing more than the so-called trace set of a process. The coarsest strong congruence on the other hand would on an LTS be the identity relation, causing the branching structure to become the strict branching structure. On an LTS two processes have the same strict branching structure iff they are tree equivalent, as follows immediately from the definitions. Silent actions play no special rôle here.



next up previous
Next: Other models Up: What is branching time Previous: The branching structure

Rob van Glabbeek