Talk:Linear temporal logic

From Wikipedia, the free encyclopedia

Contents

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

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