# What does “linear” in Linear Temporal Logic refer to?

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?

• 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. Sep 2, 2021 at 11:34
• I believe the linear in LTL refers to the linear-time vs branching-time discussion. Sep 2, 2021 at 11:43
• @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.
– user127009
Sep 2, 2021 at 12:03
• 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. Sep 2, 2021 at 12:08
• @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.
– user127009
Sep 2, 2021 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.

• 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?
– user127009
Sep 2, 2021 at 12:33
• @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. Sep 2, 2021 at 15:40
• @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.
– user127009
Sep 2, 2021 at 18:56
• Not only are there no cycles, what matters more is the absence of any kind of branching (the total order you already mention). Oct 12, 2022 at 15:55