Amir Pnueli, pioneer of temporal logic, dies at 68

Amir Pnueli, who turned a philosopher's explorations of time, logic, and free will into a critical technique for verifying the reliability of computers, died on November 2 in Manhattan. He was 68.

The cause of death was a brain hemorrhage, according to New York University, where Pnueli (pronounced p'new-EL-ee) was a professor of computer science.

In their first few decades, computers were essentially glorified calculators. Numbers were fed in, and after some calculating the answers came out. By the 1970s, programmers knew how to verify that the programs were performing such calculations correctly.

But as computers became more powerful and software more sophisticated--juggling multiple tasks and responding to changing data--verification grew harder. Programmers had to take into account the behavior of the system over time as it responded to new data or instructions while calculating.

In researching the problem, Pnueli, then at Tel Aviv University, came across the work of the philosopher Arthur Prior, who had developed "tense logic" to evaluate statements whose truthfulness changes over time.

Take the statement "I am tired," for example. While its meaning does not change, it is sometimes true and sometimes less so, and a person acts differently depending on the extent of tiredness--going to bed versus going on a hike.

In much the same way, a computer's actions must often adjust to circumstances. If the hard disk is busy reading data for another process, then a command to write data to the hard disk must wait.

"What Pnueli realized is this logic is actually a perfect fit for computer science," said Moshe Y. Vardi, a professor of computational engineering at Rice University.

Pnueli's findings on using Prior's concepts (now more commonly known as temporal logic) in computer systems appeared in a landmark 1977 paper, "The Temporal Logic of Programs."

In 1996, Pnueli received the A.M. Turing Award from the Association for Computing Machinery, an honor often called computer science's equivalent of the Nobel Prize. The award citation said his 1977 paper "triggered a fundamental paradigm shift in reasoning about the dynamic behavior of systems."

Chipmakers now use software employing temporal logic to verify that the millions of transistors are calculating as designed, and programmers use temporal logic to minimize the number of bugs in their software.

"All these things are the result of Amir Pnueli's work over 30 years ago," Vardi said.

Amir Pnueli was born on April 22, 1941, at Nahalal, in what is now Israel. He earned a bachelor's degree in mathematics from the Technion-Israel Institute of Technology and a doctorate in applied mathematics from the Weizmann Institute of Science, writing a thesis on the calculation of ocean tides. He switched to computer science as a postdoctoral fellow at Stanford and then moved to positions at the Watson Research Center of IBM in Yorktown Heights, N.Y., and at Weizmann.

He founded the computer science department at Tel Aviv University in 1973 and served as its first chairman. In 1981 he returned to Weizmann as a professor of computer science. He joined the computer science department at NYU in 1999.

Pnueli also founded two software companies, Mini-Systems in 1971 and AdCad in 1984.

His awards include the Israel Prize, the highest honor given by the State of Israel, and membership as a foreign associate in the National Academy of Sciences.

Pnueli is survived by his wife, Ariela; two daughters, Shira Pnueli-Levi of Nes Ziona, Israel, and Noga Pnueli of Brooklyn; a son, Ishay, of Hod Hasharon, Israel; and four grandchildren.

Entire contents, Copyright © 2009 The New York Times. All rights reserved.