TITLE: Time Waits for No One
AUTHOR: Eugene Wallingford
DATE: November 11, 2009 1:08 PM
DESC:
-----
BODY:
**OR:** for all p, passed(p)
~~~~
Last week saw the
passing of computer scientist Amir Pnueli.
Even though, Pnueli received the Turing Award, I do
not have the impression that many computer scientists
know much about his work. That is a shame. Pnueli
helped to invent an important new sub-discipline of
computing:
*
Pnueli received ACM's A. M. Turing Award in 1996 for
introducing temporal logic, a formal technique for
specifying and reasoning about the behavior of systems
over time, to computer science. In particular, the
citation lauded his landmark 1977 paper, "The Temporal
Logic of Programs," as a milestone in the area of
reasoning about the dynamic behavior of systems.
*

I was fortunate to read "The Temporal Logic of Programs"
early in my time as a graduate student. When I started
at Michigan State, most of its AI research was done in
the world-class
Pattern Recognition and Image Recognition lab.
That kind of AI didn't appeal to me much, and I soon
found myself drawn to the Design Automation Research
Group, which was working on ways to derive hardware
designs from specs and to prove assertions about the
behavior of systems from their designs. This was a
neat application area for logic, modeling, and
reasoning about design. I began to work under
Anthony Wojcik,
applying the idea of modal logics to reasoning about
hardware design. That's where I encountered the work
of Pnueli, which was still relatively young and full
of promise.
Classical propositional logic allows us to reason about
the truth and falsehood of assertions. It assumes that
the world is determinate and static: each assertion must
be either true or false, and the truth value of an
assertion never changes. **Modal logic** enables
us to express and reason about contingent assertions.
In a modal logic, one can assert "John **might** be
in the room" to demonstrate the possibility of John's
presence, regardless of whether he is or is not in the
room. If John were known to be out of the country, one
could assert "John **cannot** be in the room" to
denote that it is necessarily true that he is not in
the room. Modal logic is sometimes referred to as the
logic of possibility and necessity.
These notions of contingency are formalized in the modal
operators
p,
"possibly p," and
p,
"necessarily p." Much like the propositional operators
"and" and "or",
and
can be used to express the other in combination with
¬, because necessity is really nothing more than
possibility "turned inside out". The fundamental
identities of modal logic embody this relationship:

Modal logic extends the operator set of classical logic
to permit contingency. All the basic relationships of
classical logic are also present in modal logic.
and
are not themselves truth functions but quantifiers over
possible states of a contingent world.
When you begin to play around with modal operators, you
start to discover some fun little relationships. Here
are a few I remember enjoying:

The last of those is an example of a distributive
property for modal operators. Part of my master's
research was to derive or discover other properties
that would be useful in our design verification tasks.
The notion of contingency can be interpreted in many
ways. *Temporal logic* interprets the operators
of modal logic as reasoning over time.
p
becomes "always p" or "henceforth p," and
p
becomes "sometimes p" or "eventually p." When we use
temporal logic to reason over circuits, we typically
think in terms of "henceforth" and "eventually." The
states of the world represent discrete points in time at
which one can determine the truth value of individual
propositions. One need not assume that time is discrete
by its nature, only that we can evaluate the truth value
of an assertion at distinct points in time. The
fundamental identities of modal logic hold in this
temporal logic as well.
In temporal logic, we often define other operators that
have specific meanings related to time. Among the more
useful temporal logical connectives are:

My master's research focused specifically on applications
of interval temporal logic, a refinement of temporal
logic that treats *sequences* of points in time as
the basic units of reasoning. Interval logics consider
possible states of the world from a higher level. They
are especially useful for computer science applications,
because hardware and software behavior can often be
expressed in terms of nested time intervals or sequences
of intervals. For example, the change in the state of a
flip-flop can be characterized by the interval of time
between the instant that its input changes and the instant
at which its output reflects the changed input.
Though I ultimately moved into the brand-new AI/KBS Lab
for my doctoral work, I have the fondest memories of my
work with Wojcik and the DARG team. It resulted in my
master's paper, "Temporal Logic and its Use in the
Symbolic Verification of Hardware", from which the above
description is adapted. While Pnueli's passing was a
loss for the computer science community, it inspired
me to go back to that twenty-year-old paper and reminisce
about the research a younger version of myself did. In
retrospect, it was a pretty good piece of work. Had I
continued to work on symbolic verification, it may have
produced an interesting result or two.
**Postscript**. When I first read of Pnueli's passing,
I didn't figure I had a copy of my master's paper. After
twenty years of moving files from machine to machine, OS to
OS, and external medium to medium, I figured it would have
been lost in the ether. Yet I found both a hardcopy in my
filing cabinet and an electronic version on disk. I wrote
the paper in nroff format on an old Sparc workstation.
nroff provided built-in char sequences for all of the
special symbols I needed when writing about modal logic
that worked perfectly -- unlike HTML, whose codes I've been
struggling with for this entry. Wonderful! I'll have to
see whether I can generate a PDF document from the old
nroff source. I am sure you all would love to read it.
-----