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 Nov. 2 in Manhattan. He was 68.
The cause of death was a brain hemorrhage, according to New York University, where Dr. 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, Dr. 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.
Read entire article at NYT
The cause of death was a brain hemorrhage, according to New York University, where Dr. 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, Dr. 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.