Why is it that all the nodes I'm interested in have been created but there's nothing in them? Oh well, I guess that's just an opportunity for me to write something without feeling the need to rant about what's previously been written. I found my way here because I was looking for Temporal Logic of Actions or TLA+, but ended up at this node.
Let's start with a disclaimer. There are many temporal logics out there all with variations. So at best, all I can do is provide an overview of the area. Why are there so many? It's because temporal logic is a particular form of modal logic and is, therefore, rooted in philosophy. The definitions in the modal logic node are OK but miss a point. In particular the introduction of a modal operator. This still doesn't explain why so many temporal logics can exist so let me start at the beginning.
A logic comprises:
- A set of rules that define collections of symbols can be put together to make a well-formed formula (wff)
- A set of transformation rules that transform one formula into another
- A set of axioms that are underlying truths of the logic
- An interpretation of the symbols into the real world
And there you have the reason why there can be so many temporal logics; different logicians will choose different transformation rules or different axioms or different interpretations leading to all the different logics.
All the temporal logics I've seen (or used) start out with propositional logic as the basis and then add temporal operators as needed. The temporal operators permit the creation of propositions that relate to some future (or past) state. I've seen some temporal logics that included the ability to look backwards as well as forwards, but that's not really needed since you can use the start as your point of reference and everything else is then in the future!
Most temporal logics introduce 2 new operators sometime and always; it turns out that you only need one of them but, just like propositional logic, if you've got the not operator then you only need andor or, but not both. So what do these operators mean?
Sometime says that there is at least one state, either now or a future state where the proposition will be true. If the proposition is P then we would write this as ◊P (OK, the symbol may vary depending on the taste of the person (or people) who created the language.
Always says that in this, and all future states, the proposition will be true. Using the same proposition as before we would typically write this as □P
Combinations of those two operators allow for some very powerful statements; for example I can say that a proposition will be true infinitely often but that it doesn't have to be true all the time and so on.
Coming back to the idea of giving an overview; there are a number of ways we can divide up the world of temporal logic! One of the big divides is between branching time temporal logic and linear time temporal logic. Remember, temporal logic is rooted in philosophy and there's a debate among philosophers as to whether time is linear (the next state follows from this state) or whether it branches (there are multiple next states that follow from this state). This is deep stuff and it always hurt my mind when considering the multiple worlds (branching time) point of view. Another divide is whether your propositions are talking about points in time or intervals of time. If you really want to hurt your head, read up on branching time interval temporal logic!
An early, but really interesting look at temporal logic is called Temporal Logic by Nicholas Rescher and Alistair Urquhart published as volume 3 in Springer Verlag's delightfully named series The Library of Exact Philosophy. This book provides a broad overview of the philosophical underpinnings of Temporal Logic. As a computer scientist, it wasn't much help to me, as someone interested in logic it was absolutely fascinating. Many years after I had bought the book I coincidentally had the great pleasure of singing in a choir with Dorothy Rescher and, through her, meeting her husband Nick. I regret not asking him to sign my copy of the book, but it just seemed like being too much of a fanboy.