Talk:Linear temporal logic

From Wikipedia, the free encyclopedia

[edit] 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)

[edit] PLTL

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

[edit] 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 φ etc. at every time point, formulae Xφ 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 φ and one for Xφ 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 φ scattered around and, for each state, an indication of whether the corresponding LTL formula, e.g. Xφ, 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 φ 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)