Talk:Linear temporal logic

LTL is a fragment of FO

It seems to be more accurate to say that LTL is a fragment of of first order logic rather than MSO. According to this source.128.148.231.11 (talk) 14:52, 21 June 2019 (UTC)

Who invented it?

Who invented/discovered it?90.80.39.42 (talk) 15:12, 12 August 2009 (UTC)

I think Pnueli introduced LTL. See 38 of | The writings of Leslie Lamport page. However [Leslie Lamport] wrote one of the most known Temporal Logic article (the 38 on his website). AFAIK new comments/questions are to be put under the older ones Halladba (talk) 00:56, 14 August 2009 (UTC)

Pnueli invented LTL, in his paper "The temporal logic of programs". In FOCS, pages 46-57. IEEE, 1977. It would be a good idea to add a history subsection and mention this fact, with a reference to the paper. 134.130.91.61 (talk) 21:14, 9 June 2010 (UTC)

There was definitely a certain German (whose name doesn't occur to me now) before Pnueli who “invented” LTL. Certainly, no doubt Amir Pnueli popularized LTL. Furthermore, there is no such thing as THE LTL. There is, roughly speaking, Past-LTL and Future-LTL, and variants thereof with/without next, with “since” or “until” or “weak until”, etc., and the answers about who invented all these variants might differ. Already Hans Kamp in his thesis presented a temporal logic somewhat resembling LTL. Better ask Leslie Lamport directly for the name of that German (as long as Leslie Lamport is alive). PeterMüllerr (talk) 20:02, 3 September 2021 (UTC)

Figure

is the diagram for pUq correct? it seems that the bottom line shows qUp, and not pUq —The preceding unsigned comment was added by 128.30.84.40 (talk • contribs) 15:04, 17 November 2005 (UTC)

Thanks! The figure was indeed wrong. Paolo Liberatore (Talk) 19:00, 17 November 2005 (UTC)

PLTL

Is there a difference between LTL an PLTL (Propositional Linear Temporal Logic)? -- Neatlittleeraser

Release

Is the Diagram for φRψ correct? It seems as if the symbols are switched -- 195.176.177.179 15:09, 12 December 2006 (UTC)Gio

The diagrams are better-looking than the original ones, but IMO miss an important point: given the value of formulae $\phi$ etc. at every time point, formulae $X\phi$ may be true or false in each time point. For every operator there should be two or three lines; for example one line for the truth of $\phi$ and one for $X\phi$ etc. Tizio 16:44, 12 December 2006 (UTC)

Yes, I can understand what you mean, but I found those kind of diagrams more confusing. The previous diagrams used to show a path with some values of $\phi$ scattered around and, for each state, an indication of whether the corresponding LTL formula, e.g. $X\phi$, holds or not.

The new diagrams only show (all) the possible examples of paths which would make the corresponding LTL formula true at the first state. I found this easier to read and to give a quick illustration to the reader of how a path that satisfies the formula should look. I agree that the previous diagrams included more information but, at least from my point of view, it was much more than needed to quickly grasp the intuition behind each operator. I think such kind of diagrams could be great as a text book exercise (e.g. give some values of $\phi$ and get the student to fill the values of other LTL formulas on every state on the path). This all is, of course, very much subjective, so I'll be happy to hear other opinions or suggestions. --NavarroJ 05:52, 27 December 2006 (UTC)

The new diagrams are actually clearer than the original ones (and also look better, IMO), but I think they could still be made more informative:

• they should then contain Xpsi, etc. over the first point of every diagram. Otherwise, there would be no indication that the figure refers to a condition where these formulae are true in the initial state;
• if the first one is done, you might possibly want to consider adding an inward arrow to the first point, so that you are still showing the truth value of a formula in a single point, but that might not be the initial one; I'm not sure on this one, as it might add some confusion; however, it would clarify that formulae can be evaluated in time points different from the initial one.

What do you think? Tizio 14:04, 27 December 2006 (UTC)

This sounds like a good idea, I don't have the original TeX sources that I used to create the diagrams now at hand. But hopefully within a couple of weeks I can have them updated. --NavarroJ 05:47, 7 January 2007 (UTC)

Yes, they seem to be wrong. But I'm not sure about them. :(130.83.72.224 23:52, 12 December 2006 (UTC)

Well I just checked it and they are wrong. I'll try to correct it.130.83.72.224 23:55, 12 December 2006 (UTC)

Uhm, could someone correct that last image? I can't130.83.72.224 23:57, 12 December 2006 (UTC)

Actually the symbols are reversed for both Until and Release. Since it's easier, I'll just swap the symbols in the textual description. --NavarroJ 05:17, 27 December 2006 (UTC)

Model checking concept is inverted

The section about model checking (http://en.wikipedia.org/wiki/Linear_temporal_logic#Automata_theoretic_Linear_temporal_logic_model_checking) is wrong or misleading.

You do the intersection of the automaton of the model and the automaton of the negated property formula and check that the language of the resulting automaton is empty. Then the model is correct (or at least not wrong).

This is also explained in the document linked in the WP article (http://www.cmi.ac.in/~madhavan/papers/isical97.html) on page 1, paragraph 6, "...It suffices to show that no run of P is a model for ¬α, which is the same as checking that the intersection of the language accepted by P and the language defined by ¬α is empty...". The WP article currently describes the opposite. 0meaning (talk) 10:48, 6 March 2008 (UTC)

I also remember the negation of the property was used instead of the property. Well, some ambiguity is hidden in the clause "check for emptyness", which could mean both "the model satisfies the property if the intersection is empty" but also the opposite. I tried to clarify this point in the article. Tizio 18:12, 6 March 2008 (UTC)

LTL in DFA?

LTL can be shown to be equivalent to the first-order logic over one successor and the smaller relation, FO[S,<] as well as star-free regular expressions or deterministic finite automata with loop complexity 0. I have found a cite for this at: http://www.webml.org/webml/upload/ent5/1/minor5.pdf however this does not give a citation to an actual paper proving this. This seems implausible, as I cannot see how a DFA could represent liveness, the papers giving a reduction from LTL to an automata seem to give reductions to Buchi automata. —Preceding unsigned comment added by 131.254.13.19 (talk) 11:39, 19 September 2008 (UTC)

The article is awful. Please start by saying what it is in plain english. —Preceding unsigned comment added by 137.73.8.8 (talk) 15:42, 9 March 2010 (UTC)

Past fragment of LTL

LTL has a past fragment, which includes operators like "since" (the opposite of "until"), "previous" (the opposite of "next") etc. More details about the past fragment can be found, e.g., in the book: Z. Manna and A. Pnueli. The temporal logic of concurrent and reactive systems: specification. Springer, 1992. Using the past fragment is popular in many LTL specifications. It would be a good idea to present it in the article. —Preceding unsigned comment added by 134.130.91.61 (talk) 21:21, 9 June 2010 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Linear temporal logic. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20101204043002/http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 to http://mitpress.mit.edu/catalog/item/default.asp?tid=11481&ttype=2

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 10:13, 16 May 2017 (UTC)

What does “linear” in “linear temporal logic” refer to?

I think “linear“ in “linear temporal logic” refers to the time, not to the logic, right? So, shouldn't it be “linear-temporal logic”, strictly speaking?

Good Source to Add

This source has a very good introduction to linear temporal logic. It would be a good reference to add to this article and has useful information that could be added as.

Piterman, N., Pnueli, A. (2018). "Handbook of Model Checking". In Clarke, E. M., Henzinger, T. A., Veith, H., Bloem, R. (eds.). Temporal Logic and Fair Discrete Systems. Springer International Publishing. pp. 27–73. doi:10.1007/978-3-319-10575-8_2. ISBN 978-3-319-10575-8. -The-erinaceous-one (talk) 09:07, 10 October 2022 (UTC)