What is Branching Time Semantics and Why to Use it
Rob J. van Glabbeek · 1994
Introduction When comparing models or equivalences for concurrent systems, it is common practice to distinguish between linear time and branching time semantics (see for instance De Bakker, Bergstra, Klop & Meyer [1] or Pnueli [9]). In the former, a process is completely determined by the observable content of its possible (partial) runs, whereas in the latter also the information is preserved where two different courses of action diverge (although branching of identical courses of action may still be neglected). Standard examples are the processes in Figure 1 and 2. In Figure 1, both processes b ? a b \\Gamma \\Gamma \\Gamma\\Psi b b @ @ @R c b b \\Gamma \\Gamma \\Gamma\\Psi a b ? b b @ @ @R a b ? c b Figure 1: a(b + c)