Good Math, Bad Math

Why Temporal Logic?

One of the basic properties of predicate logic is that a true statement is always true, and a false statement is always false. Predicate logic doesn't allow things to change. But the most fundamental fact about time - what really defines the passage of time - is that things do change. When I'm writing this, it's monday. But when you read it, it might be tuesday or wednesday. Today, my children are in elementary school. Five years from now, they won't be.

Of course, you can always find a way to work around things if you're clever. There are ways to work around the problem of change over time using standard predicate logic. For example, one way is to add a time parameter to every predicate. So instead of saying GoesToSchool(Elementary,Rebecca), I could say GoesToSchool(Elementary, Rebecca, 20090420). But then for all of the typical, non-temporal statements in predicate logic, I would need to add universal statements: "∀t: Father(Mark,Rebecca,t)". It gets very cumbersome very quickly, and worse, it makes using the logic for reasoning incredibly awkward.

There's also another problem with predicate logic: there are lots of temporal statements I'd like to make which have a common form, which I can't express in first-order logic. I'd like to be able to say things like "Eventually I'll be hungry"; or "I'll be tired until I get some sleep". Those are two typical temporal statements, which have common forms, and it would be really useful to be able to take advantage of those common forms in temporal inference - but in first order predicate logic, I can't define a form like "eventually" - in predicate logic with time parameters, eventually is a statement about another statement - that is, it's a second-order logical construction.

Computation Tree Logic

So if predicate logic is so awkward for reasoning about time, what do we do? We create a new logic. That may sound silly, but it's something we do all the time in math. After a logic is a pretty simple formal system - we can define new ones whenever we want - and mathematicians do it all the time. So we'll just create a new logic, a temporal logic, which will make it easy for us to reason about how things change over time. In fact, there isn't just one temporal logic - mathematicians have designed many temporal logics - CTL, ATL, CTL*, LTL, and μTL to name just a few. I'm going to describe the one I'm most familiar with, which is called Computation Tree Logic, or CTL. CTL is designed for reasoning about computations with mutable states. It's a very simple logic - it may seem unreasonably simple when you see it. But it's really not; it's actually extremely useful.

CTL may be simple, but it's a fairly typical example of the way that you can look at time in a logic. The semantics - that is the meaning or model of the logic is based on a general idea called Kripke semantics which is very useful for describing change. I'll describe the specific model for temporal logic in this article, but if you want to know more about the idea of Kripke semantics, I wrote about it when I was talking about intuitionistic logic here.

The starting point for CTL is propositional logic. So we start with a basic propositional logic: a finite set of atomic statements (propositions) that we can use. (There are predicate extensions to CTL, but they make it vastly more complicated, so we'll stick to the simple, basic propositional version.) We can combine the propositions using the standard propositional logical operators - and, or, implication, and negation.

Where it gets interesting is that we also have a set of temporal quantifiers which are used to specify the temporal properties of propositional statements. Every statement in CTL has at least two temporal quantifiers. But before we get into them in detail, we need to talk about the basic model of time in CTL.

The idea of the model CTL, as I said above, is based on Kripke semantics. Kripke semantics defines a changing system by using a collection of worlds. Each world consists of an assignment of truth values to each of the basic propositions, and a set of successor worlds. In Kripke semantics, you follow a path through the worlds - in each step, you move from a world to one of its successors. In CTL, a world represents a moment in time; the successors to a world represent the possible moments of time that immediately follow it.

The Kripke semantics of CTL effectively gives us a non-deterministic model of time. From a given moment, there can be more than one possible future - and we have no way of determining which possible future will come true until we reach it. So time becomes a tree of possibilities - from each moment, you could go to any of its successors, so each moment spawns a branch for each of its successors - and each path through the tree represents a timeline for a possible future.

CTL gives us two different ways of talking about time in that tree of possible futures; to make a meaningful temporal statement, we need to combine them. First, if you look at time from any particular moment, there's a collection of possible paths into the future - so you can talk about things in terms of the space of possible futures - making statements that begin with things like "In all possible futures ..."; or "In some possible future ...". Second, you can talk about the steps along a particular path into the future - a sequence of worlds that define one specific future. You can make statements about paths like "... will eventually be true". By putting them together, you can produce meaningful temporal statements: "In all possible futures, X will always be true"; or "In at least one possible future, X will eventually become true".

Following on this idea, there are two kinds of temporal quantifiers that are used to construct temporal statements: universe quantifiers and path quantifiers. Every CTL statement uses a pair of quantifiers: one universe quantifier, and one path quantifier.

Universe quantifiers are used to make statements that range over all paths forward from a particular moment in time. Path quantifiers are used to make statements that range over all moments of time on a particular timeline-path. As I said above, in CTL statements, the quantifiers always appear in pairs: one universe quantifier which specifies what set of potential futures you're talking about, and one path quantifier that describes the properties of paths within the set quantified by the universe.

There are two universe quantifiers, which correspond to the universal and existential quantifiers from predicate logic. There's "A", which is used to say that some statement is true in all possible futures; and there's "E", which is used to say that there exists at least one possible future where something is true.

Next, there are path quantifiers. Path quantifiers are similar to universe quantifiers, except that instead of ranging over a set of possible timelines, they range over the time-worlds on a specific timeline-path. There are five path quantifiers, which can be divided into three groups:

1. The simplest path quantifier is the immediate quantifier, X (next). X is used to make a statement about the very next time-world on this path.
2. There are universal and existential path quantifiers: "G" (global), which is used to state a fact about every world-moment on the path, and "F" (finally) which is used to state a fact about at least one world-moment along a particular timeline-path.
3. There are temporal relationship quantifiers which are used to describe relationships between facts. U(strong until) and W(weak until). U and W both join statements, like "xUy" or "xWy". What they mean is that the first statement (x) is true until the second statement (y) becomes true. The strong form also means that the second statement must eventually become true; the weak form says that x is true until y becomes true, but y may never become true - in which case x will be true forever.

It's hard to see quite what all that means in the abstract, but once you see a few examples, it's actually quite simple.

• AG.(I have a big nose): No matter what happens, at every point in time, I will always have a big nose.
• EF.(I lost my job): It's possible that in some future, I will be laid off. (Formally, there exists a possible timeline where the statement "I lost my job" will eventually become true.
• A.(I do my job well)W(I deserve to get fired): For all possible futures, I do my job well until I deserve to be fired - but I won't necessary eventually deserve to be fired - it's possible (and I hope very probable) that I'll always do my job well, and so "I deserve to be fired" will never become true.
• A.(I am alive)U(I am dead): No matter what happens, I will be alive until I die - and my eventual death is absolutely inevitable.
• AG.(EF.(I am sick)): It's always possible that I'll eventually get sick.
• AG.(EF.(My house is painted blue) ∨ AG.(My house is painted brown)): In all possible futures, either my house will eventually be painted blue, or it will stay brown. It will never be any color other than blue or brown.

What's it good for?

Up above, I said that CTL, despite its simplicity, is actually very useful. What's it really good for?

I'm not going to go into detail - but one of the main uses of it is in something called model checking. Model checking is a technique used by both hardware and software engineers to check the correctness of certain temporal aspects of their system. They write a specification of their system in terms of CTL; and then they use an automated tool that compares an actual implementation of a piece of hardware or software to the specification. The system can then verify whether or not the system does what it's supposed to; and if not, it can provide a specific counter-example demonstrating when it will do the wrong thing.

In hardware model checking, you've got a simple piece of hardware - like a single functional unit from a microprocessor. That hardware is, basically, a complex finite state machine. The way that you can think of it is that the hardware has some set of points where it can have a zero or a one. Each of those points can be represented by a proposition. Then you can describe operations in terms of how outputs are produced from inputs.

So, for example, if you were looking at a functional unit that implements division, one of the propositions would be "The divide by zero flag is set". Then your specification would include statements like AG.(DivisorIsZero)&implies;AF.(DivideByZeroFlag). That specification says that if the divisor is zero, then eventually the divide by zero flag will be set. It does not specify how long it will take - it could take one step, or it could take 100. But since the behavior that we care about with that specification should be true regardless of the details of how the divider is implemented, we don't want to specify how many steps - the important behavior is that if you try to divide by zero, the appropriate flag bit is set.

Obviously, the real specifications are a lot more complex than that, but that gives you the general sense.

It's also used in software. A friend of mine from when I worked at IBM did some really cool work on model-checking software. Lots of people have looked at that, but it doesn't appear to be too useful in general - writing the specifications is hard, and checking them given the amount of state in a typical program is a nightmare. What my friend did is realize that when you look at a multithreaded system, the desired synchronization behavior is generally pretty simple - and is almost ideally suited for description in a language like CTL. So he worked out a way of using model checking to verify the correctness of the synchronization behaviors of software systems.

So that's the basics of CTL - an extremely simple, but extremely useful logic for describing time-based behaviors.