Consider the term linear temporal logic (in the meaning of linear-time temporal logic). In linear temporal logic, what does linear refer to:

  1. to temporal or

  2. to logic?

If I interpret http://en.wikipedia.org/wiki/Linear_logic and http://en.wikipedia.org/wiki/Linear_temporal_logic correctly, the linear temporal logic is not an instance of the linear logic and not related to it in any way (except that both are, well, logics), is it? So, linear must refer to temporal. Shouldn't we write then

linear-temporal logic

(i.e., with a hyphen) then to avoid misinterpretation?

  • $\begingroup$ I'm fairly sure that 'linear' refers to a property of the logic system, although the temporal aspect is also a part of the intuition behind this property. (However, I'm having a hard time to formalize this intuition properly) The lack of a direct connection to linear logic is perhaps confusing, but terms tend to collide like that from time to time. $\endgroup$
    – Discrete lizard
    Sep 2 at 11:34
  • 1
    $\begingroup$ I believe the linear in LTL refers to the linear-time vs branching-time discussion. $\endgroup$
    – Janmar
    Sep 2 at 11:43
  • $\begingroup$ @Janmar I would partially agree: if you mean the abbreviation LTL, you could indeed say that the first L may refer to “linear-time”. However, that's not the question. $\endgroup$ Sep 2 at 12:03
  • $\begingroup$ Well if your question is about why the term "linear" occurs in LTL, then the answer is found in the branching-time vs linear-time views. If your point is linguistic and only like to see the hyphen added, then I have no answer. $\endgroup$
    – Janmar
    Sep 2 at 12:08
  • $\begingroup$ @Janmar Got it. I did not mention the abbreviation LTL anywhere, and I am very well aware of the difference between the linear time and the branching time. $\endgroup$ Sep 2 at 12:14

Linear (used the same way as in linear extensions) refers to the fact that the semantic model is an infinite "path" ("linear", if you will) without cycles; every state has a well-defined next element.

There is a total ordering over the Kripke-structure (possible worlds).

I.e. it refers to temporal.

  • 1
    $\begingroup$ I am unsure whether the existence of the next element is relevant at all. After all, linear is simply a synonym for total when we speak about partial orders, isn't it? Therefore, I don't think that it matters whether paths are finite or infinite: they are linear in any case in the sense of being totally ordered, aren't they? $\endgroup$ Sep 2 at 12:33
  • $\begingroup$ @GeekestGeek Pål was simply describing what the "linear" in LTL refers to. Of course we have things like finite linear orders, but LTL formulas are only evaluated over infinite paths. $\endgroup$ Sep 2 at 15:40
  • $\begingroup$ @ReijoJaakkola Yes. I know that the standard Future-LTL models are infinite sequences. Is there any strong reason for omitting the finite ones? We sometimes wish to specify programs that may terminate, after all, without attaching self-loops to terminate states. I see also no mathematical reason to confine ourselves to infinite paths only. $\endgroup$ Sep 2 at 18:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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