01 · 计算人生
成果背后的人
阿米尔·普努埃利把时态逻辑引入计算机科学，为随时间展开的性质提供精确描述语言。这对持续与环境交互的并发和反应式系统尤为有用。他在魏茨曼研究所发展软件与硬件的规格描述和验证方法，推动形式化验证从孤立的数学论证走向系统研究持续行为的工具。
理解这项贡献
阿米尔·普努埃利将时序逻辑引入计算机科学。系统要求往往涉及事件序列：请求最终应得到回应，或者两个进程绝不能同时进入临界区。时序运算符能够精确表达这些性质，使持续行为可以接受形式化验证。
为什么重要
不断与环境交互的系统，需要关于时间和进展的规格，而不只是一个最终答案。