“Sometimes” and “not never” revisited

TLDR

These issues have been previously considered by Lamport, and CTL* is related to the logics MPL of Abrahamson and PL of Harel, Kozen, and Parikh. The paper studies the differences and appropriateness of branching versus linear time temporal logic for reasoning about concurrent programs and introduces CTL*, a language that allows a universal or existential path quantifier to prefix any linear time assertion. The authors define CTL*, a language that permits a universal or existential path quantifier to prefix any linear time assertion, to examine these issues. The paper compares the expressive power of several sublanguages and concludes with a comparison of the utility of branching versus linear time temporal logics.

Abstract

The differences between and appropriateness of branching versus linear time temporal logic for reasoning about concurrent programs are studied. These issues have been previously considered by Lamport. To facilitate a careful examination of these issues, a language, CTL * , in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined. The expressive power of a number of sublanguages is then compared. CTL* is also related to the logics MPL of Abrahamson and PL of Harel, Kozen, and Parikh. The paper concludes with a comparison of the utility of branching and linear time temporal logics.