图灵奖得主、模型检测之父 Allen Emerson 去世，享年 70 岁

10 月 16 日，因将模型检测技术发展为一张高效的验证方法而获得 2007 年图灵奖的 Allen Emerson 永远离开了我们。

图灵奖得主、形式化研究方法的巨擘 Allen Emerson，刚刚不幸去世。

2007 年，他与 Edmund Clarke 和 Joseph Sifakis 一起，因将模型检测技术（Model Checking）发展为一种高效的验证技术，并被硬件和软件行业广泛采用，而获得图灵奖。

除了图灵奖，Emerson 还与 Randal Bryant、Clarke 和 Kenneth L. McMillan 一起获得了 1998 年的 ACM Paris Kanellakis 奖，以表彰他们在开发符号模型检测方面的贡献。

授奖理由如下：

「他们发明了符号模型检测，这是一种正式检查系统设计的方法，在计算机硬件行业得到广泛使用，并且在软件验证和其他领域也开始显示出重要的应用前景。」

他对时序逻辑和模态逻辑的贡献，包括引入计算树逻辑（CTL）及其扩展 CTL*，这些技术被用于并发系统的验证。

此外，他还与其他研究者一起开发了符号模型检测，用于解决许多模型检测算法中出现的组合爆炸问题，因此获得了广泛认可。

生平

Allen Emerson 出生于美国得克萨斯州达拉斯，从小便对科学、数学话题非常感兴趣。

在上公立学校之前的几年里，他自学了微积分。

在高中时期，Emerson 学习了一门计算机编程课，并学习了 GE Mark I 分时系统的基础知识。

随后，他又自学了 BASIC、Fortran 和 ALGO 60 编程语言，并在 Burroughs B5500 大型计算机上运行了程序。

1976 年，Emerson 在得克萨斯大学奥斯汀分校获得了数学学士学位。

他继续在哈佛大学研究生院学习，并于 1981 年获得了应用数学（计算机科学）博士学位。

此后不久，他便以教员的身份，加入了得克萨斯大学奥斯汀分校，并一直在此任教。此后担任荣休教授和荣休校董事主席。

4 年前的采访中，Emerson 透露了自己转而从事计算机科学的原因。

他对建立程序正确性的形式化方法的兴趣，可以追溯到大学时期。

并从 Tony Hoare 在 ACM 上发表的一篇题为「Proof of Program: Find」论文中受到了启发。

另外，还有一个启发性因素是 Zohar Manna 在得克萨斯大学发表的演讲 —— 不动点和 Tarski-Knaster 定理。

Emerson 还对 J. W. De Bakker、W. P De Roever 和 Edsger W. Dijkstra 关于谓词 Transformer 的工作感兴趣。

模型检测

20 世纪 80 年代初，Emerson 与他的博士导师 Edmund M. Clarke 共同开发了验证有限状态系统对形式规范的技术。

他们创立了一种自动化质量保证方法的技术概念，该方法检查一个名义上有限状态并发系统是否提供其规范的模型（即满足其规范）。

他们为这个概念创造了「模型检测」这个术语，在欧洲，Joseph Sifakis 独立发现了类似的想法。

这里「模型」一词的含义与数理逻辑中模型理论的用法相符：系统被称为规范的模型。

这种模型检测方法具有几个理想的特点：

• 是完全自动化和算法化的，因为它需要对程序的状态空间进行系统的搜索；

• 精确且富有表现力，具有正式定义的规范逻辑，计算树逻辑（CTL），可以捕获各种感兴趣的正确性属性；

• 高效，运行时间在输入系统和规范的大小上是多项式的，这部分归功于这种特殊的逻辑；

• 非常适合推理关于并发程序，对于这些程序，传统的质量保证方法已被证明大多无效；

• 从一开始就被设计为提供一个实用的验证方法的基础。

Emerson 在模型检测领域的工作主要包括两个方面：一是开发了早期且有影响力的时序逻辑，用于描述系统规范；二是提出了减少状态空间爆炸的技术。

可以说，无论是制定广泛使用的灵活和富有表现力的规范逻辑，还是相关的模型检测算法，Emerson 都做出了开创性贡献。

强大的计算树逻辑以及不动点逻辑的表现力在理论和实践中，都具有基础性的作用。

甚至，表现力比推理方法的效率更为基本：如果重要的正确性属性甚至无法表达，那么逻辑对于程序验证是无用的。

Emerson 开发的许多逻辑工具，都是大多数工业规范逻辑和相关模型检测工具的核心。

因此，这些逻辑已被纳入几个著名的商业框架（例如 IBM Sugar）和规范的工程标准（例如 Accellera-IEEE 属性规范逻辑，IBM 属性规范逻辑 / Sugar）。

最初的论文描述了模型检测的基本原理。然而，它和所有后续的模型检测器都必须应对效率问题。

直观地说就是，问题在于小程序可能具有极大的状态数量，即包括数据值和位置计数器的程序变量的配置。

早期的模型检测器通常会计算程序的每一个可能状态。这可能导致系统状态图大小的组合爆炸，称为状态爆炸。

例如，一个具有 50 个相似进程的并发系统，每个进程仅有 10 个本地状态，可能拥有全局状态的个数是一个天文数字。

随着领域的进步，研究者开发出许多强大的技术来缓解状态爆炸，通常基于简化或缩小状态图的表示。

因此，适合模型检测的系统规模多年来大幅增加。虽然状态爆炸尚未完全被消除，但对于许多应用来说，它已在很大程度上得到控制。

避免组合爆炸

正如 A 图灵奖长篇引文中所指出的：「模型检测的发展使其能够成功应用于复杂系统，这需要开发复杂的方法来应对所谓的『状态爆炸问题』。

自 1981 年以来，通过现在已经非常庞大的国际研究社区，在这个问题上取得了巨大进展。因此，许多主要的硬件和软件公司现在在实践中使用模型检测。其应用实例包括超大规模集成电路（VLSI 电路）、通信协议、软件设备驱动程序、实时嵌入式系统和安全算法的验证。」

在大多数情况下，系统规模占主导地位，即使是线性时序逻辑中，小规范的指数爆炸也是可以容忍的。但在其他情况下，规范很大，导致不可行的显著（指数或更糟）爆炸。

Emerson 的工作解决了系统规模和规范规模的效率问题。使用 CTL 等逻辑的一个优势是模型检测的成本在规范规模上是线性的。

Emerson 还在限制状态爆炸的技术方面，取得了极具创新和影响深远的进展。

其中一项技术利用了系统中许多相似子组件的对称性所固有的冗余。这使得大型系统可以转换为更小的系统，从而显著提高模型检测器的速度和容量。对称性简化允许使用指数减少的模型来推理大型模型。许多模型检测工具都包含对称性简化，包括 IBM 的 Rulebase。

Emerson 还在将简化与其他应对状态爆炸的方法结合方面发挥了先锋作用，例如将对称性简化与符号模型表示结合，或将对称性简化与部分顺序简化结合。

Emerson 的另一项工作，是对某些模型检测方法的关键组成部分进行研究。这涉及应用不动点逻辑来检查无限对象上的自动机的非空性，并计算开放系统与其环境之间游戏的获胜策略。这些应用于多智能体系统的模型检测。

另一种方法解决了参数化模型检测问题的许多重要情况，其中对于所有 n，必须为由 n 个子组件组成的系统建立正确性。

Emerson 使用这些技术以算法方式验证了摩托罗拉的无限长汽车数据协议，并验证了常见缓存协议的任意大型系统。

对于 Allen Emerson 的离去，他的朋友表示深切的悼念。

「Allen，一路走好。真的很想念你的建议和洞察力。」

参考资料：

• https://amturing.acm.org/award_winners/emerson_1671460.cfm

• https://en.wikipedia.org/wiki/E._Allen_Emerson