Good Math, Bad Math

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.

Comments

  1. #1 Chris Granade
    April 28, 2009

    I’m very happy you posted this, but I must admit being confused on one point. In particular, the example statement AG.(EF.(My house is painted blue) ∨ AG.(My house is painted brown)) confuses me. If the house is presently green, and you’ll repaint it blue tomorrow, wouldn’t that satisfy the EF.(My house is painted blue) clause? Then, it seems that the entire statement would be satisfied if your house is presently green and you are guaranteed to repaint it blue in all futures. Am I missing something?

    Anyway, thanks for writing this article. It’s really interesting to see how the ? and ? quantifiers generalize to a temporal model.

  2. #2 Greig Robertson
    April 28, 2009

    Nice post. I hope you do include some logics in your book, (or maybe write another book?!) it’s a subject that’s hard to explain once you get beyond the basics. I’ve just finished reading about LTL and CTL in Huth & Ryan’s Logic for Comp Sci – they use NuSMV to model concurrent processes.
    Chris – I believe you are correct since AG refers to “all future” colours regardless of what the current colour is.

  3. #3 Adrian Morgan
    April 28, 2009

    Ian Stewart uses the following as an example of an applied logical fallacy in his book “Game, Set and Math”:

    “Only an elephant or a whale gives birth to a creature that weighs more than 100 kilograms,” said Tweedledumb. “Right?”
    “I suppose,” said Tweedledim.
    “The President weighs 101 kilograms,” said Tweedledumb.
    “Uh-oh,” said Tweedledim. “I can see exactly where you’re going and I don’t…”
    “Therefore,” said Tweedledumb…
    “The President’s mother is either an elephant or a whale!” they yelled in chorus.

    As an exercise, I just tried to apply CTL to that scenario, but I can’t get it to work (mind you, I’d only been trying for a few minutes). Partly because CTL as you’ve explained it is a “from now on” thing, whereas the President’s birth is an event in the past. Can CTL be used to describe and draw conclusions from the above scenario if you know what you’re doing, or is it simply outside the scope of this particular type of temporal logic?

  4. #4 Kaleberg
    April 28, 2009

    I remember Kripke from doxastic and epistemic logic. He did a lot of mathematics that was basically reasoning about graphs of relationships, as with temporal logic and as with doxastic and epistemic logic. I gather in his later years, he started out in his early teens, he began to regret referring to “other worlds” in his model. There were all too many crackpots eager for a bit of stirring.

  5. #5 micah
    April 29, 2009

    in predicate logic with time parameters, eventually is a statement about another statement

    I don’t understand what you’re trying to say here. Why isn’t “I’ll eventually be hungry” expressible by the first-order statement “∃ t:t>t_now ∧ IsHungry(Micah, t)”?

  6. #6 csrster
    April 29, 2009

    Cool. What happens when you have relativity of simultaneity?

  7. #7 Jonathan Amsterdam
    April 29, 2009

    Following up on micah’s comment: you can express “eventually”, “until” and similar ideas — in fact, everything you can express with the CTL path quantifiers — in predicate logic + time. (E.g. G is just “for all t” and F is just “there exists a t”.) What you can’t express is modality — possibility and necessity. This is where the box and diamond (or A and E, as you write them), and possible-worlds semantics, come in. I suppose CTL introduce the path quantifiers, rather than add box and diamond to predicate logic + time, in order to expand the range of what is expressible without having to deal with quantifying into modal contexts.

  8. #8 Avi Steiner
    April 29, 2009

    I’d like to be able to say things like “Eventually I’ll be hungry”…

    Exists(t) ( LaterThan(t,20090420) && Hungry(Avi,t) )

    where Exists( ) is the existential quantifier. (I’m on a public computer that doesn’t allow access to character map).

  9. #9 Zeno
    April 30, 2009

    It’s April 30. Happy Gauss’s Birthday!

    There won’t be any Gauss caroling, but appropriate memorial lectures may occur in certain math classes.

  10. #10 TonyC
    April 30, 2009

    re: AG.(EF.(My house is painted blue) ∨ AG.(My house is painted brown))

    As ar as I understand this (and it’s been a very long time since I did any formal logic – CS was many decades ago!)

    If you parse this – the Globally true Axiom asserted is indeed true only if one the internally asserted clauses is true (EITHER blue at some future time in the path, or BROWN in all current worlds)

    If your house is currently GREEN, you fail the AG(Brown) clause. The EF(blue) would then only be true if indeed there is a defined world in the path with such a property. It may not yet (or ever) be defined. The axiom is only guaranteed to be formally true if the house is currently Brown or Blue, OR potentially Blue at some point in the future.

    Your house may be green, but that is not a defined state or axiom, so the logic is perhaps incomplete with regards to your query (your question is undecidable). However, the fact that the compound clause is considered to be a global axiom (true at this time) tells us that ‘my house is green’ is a false statement in the logic as defined (an axiom AG.(FALSE ∨ TRUE) would be meaningless)

    Of course – this may simply be babble – so I’d appreciate some help form someone who actually has a clue :)

  11. #11 Jonathan Vos Post
    May 1, 2009

    “An interesting temporalization of Gödel’s ontological proof” by Gavriel Segre.

    http://arxiv.org/abs/0904.3921

  12. #12 NeilF
    May 4, 2009

    Responding to comment number 7:

    I don’t believe there is a qualitative difference here between the logical expressibility of temporal vs modal concepts.

    Temporal: You can render “eventually phi” as “there exists a time t such that t > now and phi(t)”

    Modal: You can render “possibly phi” as “there exists a world w such that w R thisworld and phi(w)”. (Here ‘R’ is our frame relation, which may or may not have to satisfy certain properties. E.g. in S5 R must be an equivalence relation.)

    Basically, ‘expressing’ these ideas in ordinary predicate logic amounts to the same thing as providing a semantics for the ‘special’ quantifiers one finds in temporal or modal logic.

  13. #13 Gzus
    May 6, 2009

    Who’s the name of the IBM’s tool for model checking? Thanks.

  14. #14 Gilbert
    May 9, 2009

    At the beginning of Computation Tree Logic you write, “After a logic is a pretty simple formal system – we can define new ones whenever we want” Perhaps you meant “After *all* a logic is …”?

  15. #15 Anonymous
    May 31, 2009

    Mark, if you’re editing this for your book, perhaps you would appreciate the following comment. In this paragraph on model checking

    “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.”

    you use the word system ambiguously to refer to both the system being model checked and the model checker itself. Maybe the clarity would be improved if you said (for instance)

    “The *model checker* can then verify whether or not the system does…”

The site is currently under maintenance and will be back shortly. New comments have been disabled during this time, please check back soon.