"Sometimes" and "Not Never" Revisited: On Branching versus Linear Time Temporal Logic

"Sometimes" and "Not Never" Revisited: On Branching versus Linear Time Temporal Logic

January 1986 | E. ALLEN EMERSON AND JOSEPH Y. HALPERN
This paper revisits the differences between branching and linear time temporal logic for reasoning about concurrent programs. It defines a language, CTL*, which allows universal or existential path quantifiers to prefix arbitrary linear time assertions. The expressive power of various sublanguages of CTL* is compared, showing that CTL* subsumes both of Lamport's interpretations and allows for a clearer comparison between branching and linear time logics. The paper also discusses the limitations of Lamport's approach, particularly his assumptions about the semantics of concurrent programs and the equivalence relation used to compare logics. It argues that Lamport's conclusions about the superiority of linear time logic for concurrent programs are not fully justified, as branching time logics can be more expressive in certain cases. The paper concludes that both branching and linear time logics have their own strengths and are appropriate for different applications.This paper revisits the differences between branching and linear time temporal logic for reasoning about concurrent programs. It defines a language, CTL*, which allows universal or existential path quantifiers to prefix arbitrary linear time assertions. The expressive power of various sublanguages of CTL* is compared, showing that CTL* subsumes both of Lamport's interpretations and allows for a clearer comparison between branching and linear time logics. The paper also discusses the limitations of Lamport's approach, particularly his assumptions about the semantics of concurrent programs and the equivalence relation used to compare logics. It argues that Lamport's conclusions about the superiority of linear time logic for concurrent programs are not fully justified, as branching time logics can be more expressive in certain cases. The paper concludes that both branching and linear time logics have their own strengths and are appropriate for different applications.
Reach us at info@study.space