A Quick Bit of Temporal Logic: Introducing CTL

This post is something that I'm thinking of including in my
book. I haven't decided whether I want to spend this much time on
logics; they're really interesting and fun - but there's lots of
other interesting and fun stuff, and there's only so much space.

The topic of the moment is temporal logic - that is, a logic which
is built for reasoning about things that change over time.

To begin with, why do we want temporal logic? Most of the time,
when we want to use logical reasoning, we use predicate logic. So why
do we need another logic?

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.