The paper revisits the debate between branching and linear time temporal logic for reasoning about concurrent programs, revisiting and critiquing Lamport's arguments. The authors define a new language, CTL*, which allows path quantifiers to prefix linear time assertions, and compare its expressive power with various sublanguages. They find that while linear time logic is generally adequate for verifying preexisting concurrent programs, branching time logic is necessary for reasoning about nondeterministic programs. The paper also explores the relationship between CTL* and other logics like MPL and PL, providing a comprehensive taxonomy of linear and branching time logics. The results show that branching time logic can be more expressive than linear time logic in certain contexts, and that the choice between the two depends on the specific requirements of the application.The paper revisits the debate between branching and linear time temporal logic for reasoning about concurrent programs, revisiting and critiquing Lamport's arguments. The authors define a new language, CTL*, which allows path quantifiers to prefix linear time assertions, and compare its expressive power with various sublanguages. They find that while linear time logic is generally adequate for verifying preexisting concurrent programs, branching time logic is necessary for reasoning about nondeterministic programs. The paper also explores the relationship between CTL* and other logics like MPL and PL, providing a comprehensive taxonomy of linear and branching time logics. The results show that branching time logic can be more expressive than linear time logic in certain contexts, and that the choice between the two depends on the specific requirements of the application.