多条可能路径，一个精确模型

达纳·斯科特

达纳·斯科特是一位把数理逻辑与程序设计基础联系起来的逻辑学家。他与迈克尔·拉宾提出非确定有限自动机，并证明它与确定自动机之间的关系。后来，他与克里斯托弗·斯特雷奇发展指称语义，为程序赋予数学意义。1976 年共同获得图灵奖、表彰自动机研究时，他任职于牛津大学。

迈克尔·拉宾

迈克尔·拉宾帮助奠定自动机与算法的数学基础。他与达纳·斯科特的研究表明，非确定有限自动机可以识别与确定自动机相同的语言。他后来开创随机算法研究，并对密码学作出重要贡献。他长期任职于耶路撒冷希伯来大学，承担学术领导工作并曾任校务长，后来还在哈佛担任教授。