What is branching time and why to use it?
R.J. van Glabbeek
Computer Science Department, Stanford University,
Stanford, CA 94305, USA.
The concept of branching time in the semantics of
concurrent systems is well known and well understood. Still
a formal definition of what it means for a model or
equivalence to respect branching time has never explicitly
be given. This note proposes such a definition.
Additionally the opportunity is taken to voice an old but
poorly understood argument for using branching time
semantics instead of models or equivalences that are fully
abstract with respect to some notion of observability.
KEYWORDS: Concurrency, semantic equivalences, linear time, branching
time, labelled transition systems, branching bisimulation.
This work was supported by ONR under grant number N00014-92-J-1974.
- Report No. STAN-CS-93-1486, Stanford 1993.
- Available at
TEX) and at http://Theory.stanford.edu/~rvg/branching.
- In: The Concurrency Column (M. Nielsen, ed.),
Bulletin of the EATCS 53, June 1994, pp. 190-198.
- In: Current Trends in Theoretical Computer Science;
Entering the 21st Century (G. Paun, G. Rozenberg &
A. Salomaa, eds.), World Scientific, 2001, pp. 469-479.