The Wikipedia article on temporal logic lists many varieties of temporal logic, such as LTL (linear temporal logic), CTL (computation tree logic), CTL*, and others. Which of these is the logic described in Manna & Pnueli's textbook The Temporal Logic of Reactive and Concurrent Systems: Specification?

I've started to read Manna & Pnueli's textbook. I'd like to read other accounts of the same theory. But to do so I need to know the name of the theory, so I can look for other textbooks about it.


1 Answer 1



PS The very book you mention has a historical note section discussing various other temporal logics near page 271.

Edit (leaving the above intact for the comments to make sense): None of the named logics in the wikipedia article (at the time of writing this) is the same as/equivalent to Manna and Pnueli's. The name LTL has however a different and broader meaning in the community.

  • $\begingroup$ Judging by the Wikipedia article on Linear temporal logic, the logic presented in Manna & Pnueli's textbook is not LTL, since LTL is propositional, whereas Manna & Pnueli's logic allows quantification over non-propositional variables. The historical note section in the textbook (titled Bibliographic Notes, and starting on p. 268) is of no help to me in answering my question. $\endgroup$
    – Evan Aad
    Commented Mar 4, 2023 at 5:04
  • $\begingroup$ Well, perhaps one should not judge by wikipedia then. In the community, LTL is colloquially understood as "what Manna & Pnueli did in their books". This is of course a bit sloppy. Some papers omit the past-time operators present on the books, others some quantifiers. The propositional version called LTL in that wikipedia article is otherwise known as Propositional Temporal Logic (p. 269 M&P'90) or PLTL (e.g. in Emerson's chapter on Temporal and Modal Logic in vol B of the Handbook of Computer Science). $\endgroup$
    – Kai
    Commented Mar 4, 2023 at 6:10
  • $\begingroup$ I'll edit my "answer" to clarify that the while the name is one used in the wikipedia article, it's got a different meaning. $\endgroup$
    – Kai
    Commented Mar 4, 2023 at 6:21
  • $\begingroup$ OK. I'll accept your answer thanks to the citation in your penultimate comment of Emerson's chapter in volume B of Handbook of Computer Science. I checked in said chapter (which was reviewed by Amir Pnueli), and it indeed looks like the temporal logic in Manna & Pnueli's textbook is First Order Linear Temporal Logic. $\endgroup$
    – Evan Aad
    Commented Mar 4, 2023 at 8:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.