“Sometimes” and “not never” revisited: on branching versus linear time temporal logic. Emerson, E. A. & Halpern, J. Y. Journal of the ACM, 33(1):151–178, 1986. ISBN: 0897910907
“Sometimes” and “not never” revisited: on branching versus linear time temporal logic [link]Paper  doi  abstract   bibtex   
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.
@article{emerson_sometimes_1986,
	title = {“{Sometimes}” and “not never” revisited: on branching versus linear time temporal logic},
	volume = {33},
	issn = {00045411},
	url = {http://portal.acm.org/citation.cfm?doid=4904.4999},
	doi = {10.1145/4904.4999},
	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.},
	number = {1},
	journal = {Journal of the ACM},
	author = {Emerson, E. Allen and Halpern, Joseph Y.},
	year = {1986},
	note = {ISBN: 0897910907},
	pages = {151--178}
}

Downloads: 0