Talk:Temporal logic

History as stated is wrong

It was Amir Pnueli (without Zohar Manna) who brought linear temporal logic to CS (Amir Pnueli, "The Temporal Logic of Programs" FOCS 1977: 46-57), and it was Ben-Ari, Pnueli, and Manna who invented Computational Tree Logic (CTL) in (Mordechai Ben-Ari, Zohar Manna, Amir Pnueli: "The Temporal Logic of Branching Time". POPL 1981: 164-176) Emerson and Clarke have very little to do with it. In their model-checking paper they used 'synchronization skeletons'. Later Pnueli told them about his POPL paper with Manna and Ben-Ari, and then they switched to CTL. — Preceding unsigned comment added by 24.131.17.108 (talk) 01:31, 28 July 2011 (UTC)

Untitled

This talk page used to be a redirect to Talk:Time loop logic. I have removed this redirect. Paolo Liberatore (Talk) 14:43, 18 October 2005 (UTC)

Section of common properties

A section describing common properties to check should be added, for example:

• AG p - Safety
• AF p - Liveness
• EF p - Reachability
• EG p - ?? <- is there a name for that?

Notation and Diagrams

In the section on Temporal Operators, the notation is confusing at best. There is no explanation of the reason for both a "Textual" column and a "Symbolic" one. Are these just alternate notations? If so, "Notation", and "Alternative Notations" would be clearer, and could perhaps be better omitted altogether in favor of simply extending the list of alternate notations which is already given below the table.

The notation given in these columns isn't used consistently in the "Definition" column. In the row for φ U ψ, with alternate (?) notation Φ U ψ, we get what purports to be a definition of (B U C)(Φ).

But why do we suddenly shift from using Φ and ψ as the operands to using B and C? And why is that 'Φ' tacked on there? Is it now a temporal variable, in contrast to its use in 'Φ U ψ' as a sentential variable? If a temporal variable is wanted, 't' would seem to be a better choice. And what is the relation of Φ to Φi and Φj? If the latter are temporal variables, too, why use a subscripted Φ? Why not just use t, i, j without confusingly attaching them to an idle symbol Φ? And shouldn't j be constrained to be at least as great as t? Similar questions arise for the rest of this table.

The diagrams are a useful device, but need to be repaired. For example, the diagram for the until operator does not distinguish it from a Boolean or. Adding a red bar for p from point 5 to point 6, without extending the red bar for p U q would make the distinction clearer.

Also, the diagrams (with their continuous bands of red) suggest the formalism is applicable on a continuous model of time as well as a discrete model, but if the model of time is continuous then there are subtleties about potentially open intervals not represented here, while if a discrete model is assumed, the continuous color bars are misleading. And if neither is presumed, then some mention of the important distinction between discrete time and more general temporal orderings is needed, together with a mention of the fact that the former is more appropriate for computational situations and the latter (perhaps) more apt in philosophical applications.

Mark A. Brown 24.58.210.222 (talk) 00:44, 18 July 2010 (UTC)

Until operator

Is the diagram for Until operator correct? The way we were taught in lectures is that p U q should also be true at t=0 because p will hold from that time, i.e. not immediately but starting with the next chronon. Also p U q should cease to hold much earlier than in the diagram given. I am aware that we were taught U-S logic due to Kamp (1968), but if there is more than one understanding of this operator, this should be made clear. —Preceding unsigned comment added by 155.198.14.157 (talk) 19:03, 25 November 2008 (UTC)

Name

I think we should change the name to tense logic because WILL and WAS opertor belong to the grammatical category of tense. Temporal logic uses variabels for instances of time. RickardV 06:29, 24 July 2007 (UTC)

I think that we should introduce a distinction between temporal logic and tense logic. One[1] of the cited resources explains that temporal logic is any logic system which deals with time, while tense logic is the one with the diamond and square operators described in the body of this article. Cloudyed (talk) 09:31, 21 June 2008 (UTC)

I think the F and G operators of tense logic described in the Stanford Encyclopedia of Philosophy are related to, but not the same as, the F and G operators described in our article. The meanings described here, which are current in computer science, only consider the future and not the past, unlike tense logic.  --Lambiam 07:02, 27 June 2008 (UTC)

Improperly parenthesised expressions

N.B. I guess the expression of φ U ψ and φ R ψ in the article are improperly parenthesised. If someone aware could give a look at this... —Preceding unsigned comment added by 81.56.75.108 (talk) 20:27, 10 February 2008 (UTC)

I think you are right, because in both the second occurrence of i is not bound. Frankly, the whole thing does not make much sense, what with the switches from φ and ψ to B and C to p and q, and with φ having a totally different and unexplained role in the "Definition" column.  --Lambiam 03:49, 11 February 2008 (UTC)

general versus broad sense

The article's a little vague on what it defines "temporal logic" as, starting with a very general definition, but somewhat implying through the rest of the article a more specific definition that uses modal operators. In some areas at least (like AI), the term is sometimes used much more broadly to refer to any logic that reasons about change over time, including those which take the fluent approach rather than the special-temporal-operators approach. --Delirium (talk) 07:34, 6 September 2008 (UTC)

Removed bogus claim of priority for Avicenna

Here. It contradicts p. 72 in ISBN 0-7923-3586-4, and there is a well-known POV pusher who fills Wikipedia with that crap. Tijfo098 (talk) 05:17, 28 March 2011 (UTC)

After several pages of discussion on temporal propositions in Antiquity, the book says: "In the Middle Ages, one of the first philosophers to discuss temporal propositions was the Islamic logician Ibn Sina (980-1037), in Christian Europe known as Avicenna." And after a brief discussion concludes "One cannot say that Avicenna developed a real theory of such temporal propositions, but he did try to work out the relationship between temporalis and the implication." And if you read the whole chapter, you see that quite a few others also tried. Tijfo098 (talk) 05:26, 28 March 2011 (UTC)

Perhaps a sentence or two should therefore be added mentioning ibn Sina's work even though it did not lead to a fully developed theory of temporal logic. After all there is already mention of Aristotle's work even though it was only, as the article currently says, a "partially-developed form of first-order temporal modal binary logic." You mention other tried, I guess we'd then have to consider adding them too, depending on the weight of their contribution. The other option is to mention no one (inc. Aristotle) and begin the history with Prior. 188.221.111.74 (talk) 20:20, 30 April 2011 (UTC)

I'll try to summarize the middle ages stuff. Not easy because there were many attempts. But logic (not just the temporal one) did not progress much if at all from Aristotle to Boole/Frege. There's a famous quote from Kant on that; [2] [3]. Tijfo098 (talk) 00:52, 1 May 2011 (UTC)

The post above is complete an utter bullshit. Avicenna influence towards the development of temporal modal logic, is undeniable. He is certainly the first to develop a formal idea of temporal logic. — Preceding unsigned comment added by 142.196.88.228 (talk) 02:06, 22 January 2013 (UTC)

Given that the only arguments given by the IP are the opinion that the above comments are "bullshit" and the claim that Avicenna's influence is "undeniable" when the given source apparently clearly denies it ("One cannot say that Avicenna developed a real theory of such temporal propositions"), I have reverted User:142.196.88.228's re-addition of banned user User:Jagged 85's content. --McGeddon (talk) 12:02, 23 January 2013 (UTC)

Relation to grammatical aspects

"One might also take note that in the Russian language, verbs have an aspect, based commonly upon time, but position also." Have added a link to the grammatical aspect article in Wikipedia. That article also describes grammatical aspects in other languages. In any case, the connection between grammatical aspect and temporal logic should be elaborated. 92.230.66.116 (talk) 11:04, 17 July 2012 (UTC)

Manual Revert to include contribution of Avicienna

Avicenna influence towards the development of temporal modal logic, is undeniable. He is certainly the first to develop the formal ideas of temporal-modal logic. Unfortunately, there are a self-deluded few, who make the centric efforts to deny this. — Preceding unsigned comment added by 142.196.88.228 (talk) 02:06, 22 January 2013 (UTC)

Release Diagram wrong

I think the Release diagram is wrong:

The formula reads basically:

For all points of time, either C holds or B holds before

So if at point 3 it pRq doesnt hold, then it cannot hold anymore because of the universal quantifier.

Please correct me if I'm wrong, I'll return in the next 48h to read the replies — Preceding unsigned comment added by 186.222.51.224 (talk) 12:40, 26 February 2015 (UTC)

As far as I understand, a temporal formula is evaluated from the time of evaluation until the end of the trace. So, at time 7.5, the formula "pRq" holds because for all i (higher or equal than 7.5), the formula "q" holds. Wikini (talk) 13:30, 27 February 2015 (UTC)