0
$\begingroup$

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.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

LTL.

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.

Improve this answer
$\endgroup$
4
  • $\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
    Mar 4 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
    Mar 4 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
    Mar 4 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
    Mar 4 at 8:15

Your Answer

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

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