1996 · 语言与软件

说明时间中必须发生什么

时序逻辑为持续运行的系统提供了表达承诺的语言。

阿米尔·普努埃利

1996图灵奖

视觉指南

奖项，化为图解

阅读图解文字

不断与环境交互的系统，需要关于时间和进展的规格，而不只是一个最终答案。

时序性质的验证依赖模型，包括调度和环境方面的假设。

01 · 核心想法

阿米尔·普努埃利将时序逻辑引入计算机科学。系统要求往往涉及事件序列：请求最终应得到回应，或者两个进程绝不能同时进入临界区。时序运算符能够精确表达这些性质，使持续行为可以接受形式化验证。

不断与环境交互的系统，需要关于时间和进展的规格，而不只是一个最终答案。

02 · 人物

阿米尔·普努埃利把时态逻辑引入计算机科学，为随时间展开的性质提供精确描述语言。这对持续与环境交互的并发和反应式系统尤为有用。他在魏茨曼研究所发展软件与硬件的规格描述和验证方法，推动形式化验证从孤立的数学论证走向系统研究持续行为的工具。

03 · 延伸阅读

本站原创讲解依据官方获奖记录。领域标签用于编辑导航。