Sometime’ is Sometimes ‘Not Never’

After graduating from Cornell, Susan Owicki joined the faculty of Stanford. Some time around 1978, she organized a seminar to study the temporal logic that Amir Pnueli had recently introduced to computer science. I was sure that temporal logic was some kind of abstract nonsense that would never have any practical application, but it seemed like fun, so I attended. I observed that people got very confused because, in Pnueli’s logic, the concepts of always and eventually mean what they do to ordinary people. In particular, something is not always true if and only if it is eventually false. (It doesn’t always rain means that it eventually stops raining.) However, most computer scientists have a different way of thinking. For them, something is not always true if and only if it might possibly become false. (The program doesn’t always produce the right answer means that it might produce the wrong answer.)

I realized that there are two types of temporal logic: the one Pnueli used I called linear time logic; the one most computer scientists seemed to find natural I called branching time. (These terms were used by temporal logicians, but they distinguished the two logics by the axioms they satisfied, while I described them in terms of different kinds of semantics.) Pnueli chose the right kind of logic–that is, the one that is most useful for expressing properties of concurrent systems. I wrote this paper to explain the two kinds of logic, and to advocate the use of linear-time logic. However, I figured that the paper wouldn’t be publishable without some real theorems. So, I proved some simple results demonstrating that the two kinds of logic really are different.

I submitted the paper to the Evian Conference, a conference on concurrency held in France to which it seems that everyone working in the field went. I was told that my paper was rejected because they accepted a paper by Pnueli on temporal logic, and they didn’t feel that such an obscure subject merited two papers. I then submitted the paper to FOCS, where it was also rejected. I have very rarely resubmitted a paper that has been rejected. Fortunately, I felt that this paper should be published. It has become one of the most frequently cited papers in the temporal-logic literature.