TITLE: Time Waits for No One AUTHOR: Eugene Wallingford DATE: November 11, 2009 1:08 PM DESC: ----- BODY: OR: for all p, eventually (modal)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 possibly (modal)p, "possibly p," and necessarily (modal)p, "necessarily p." Much like the propositional operators "and" and "or", possibly (modal) and necessarily (modal) 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 identities
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. possibly (modal) and necessarily (modal) 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:
modal relationships
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. necessarily (modal)p becomes "always p" or "henceforth p," and possibly (modal)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:
temporal logic operators
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. -----