Эмерсон, Эрнест Аллен

Эмерсон получил степень бакалавра наук по математике в Техасском университете в Остине в 1976 году и степень доктора философии в области прикладной математики в Гарвардском университете в 1981 году^[3].

С 1981 года преподавал в Техасском университете в Остине. Вышел на пенсию в 2016 году после 35 лет работы, сохранив звание почётного профессора (Regents Chair Emeritus).

Награждён в 2007 году вместе со своим научным руководителем Эдмундом Кларком и Иосифом Сифакисом премией Тьюринга за вклад в развитие теории проверки моделей^[4].

Скончался 15 октября 2024 года в своём доме в Остине, штат Техас. 28 апреля 2025 года в Техасском университете в Остине состоялся мемориальный семинар, посвящённый его жизни и работе^[5].

Эрнест Аллен Эмерсон внёс фундаментальный вклад в развитие метода проверки моделей (model checking) — высокоэффективной техники автоматической верификации программного и аппаратного обеспечения. За эти достижения он, вместе с Эдмундом Кларком и Иосифом Сифакисом, был удостоен премии Тьюринга в 2007 году^[6].

Разработка логики CTL и первого алгоритма проверки моделей

В 1981 году в своей основополагающей работе «Design and synthesis of synchronization skeletons using branching time temporal logic», написанной совместно с Эдмундом Кларком, Эмерсон представил два ключевых нововведения^[7]:

• Логика CTL (Computation Tree Logic): Они предложили использовать темпоральную логику ветвящегося времени (branching-time temporal logic), названную CTL^[8]. В отличие от ранее предложенной линейной логики (LTL), которая рассматривает одно возможное будущее, CTL описывает свойства системы через дерево всех возможных вычислений^[9]. Это позволяет формулировать более сложные спецификации, например, «существует ли путь выполнения, на котором система может достигнуть безопасного состояния» или «на всех ли возможных путях система неизбежно вернётся в исходное состояние»^[10].
• Первый алгоритм проверки моделей: В той же работе Эмерсон и Кларк описали первый практический алгоритм для проверки моделей^[9]. Этот алгоритм мог автоматически и эффективно проверять, удовлетворяет ли конечная система (представленная в виде графа состояний) спецификациям, записанным на языке CTL^[8]. Сложность алгоритма была полиномиальной от размера модели и длины формулы, что делало его применимым на практике^[8].

Исследование выразительности темпоральных логик

После первоначального прорыва Эмерсон продолжил исследования теоретических аспектов темпоральных логик. Совместно с Джозефом Халперном он определил логику CTL*, которая объединяет выразительные возможности CTL и LTL. В серии работ, таких как «‘Sometimes’ and ‘Not Never’ Revisited: On Branching Versus Linear Time», Эмерсон и Халперн формально исследовали, какие свойства систем можно и нельзя выразить в различных логиках, установив их теоретические границы и помогая инженерам выбирать подходящий формализм для задач верификации^[11].

Вклад в развитие символьной проверки моделей

Работа Эмерсона также была критически важна для решения «проблемы взрыва состояний», когда число состояний системы растёт экспоненциально^[12]. Хотя основной прорыв в этой области — использование двоичных диаграмм решений (BDD) — был сделан другими исследователями, созданный Эмерсоном и Кларком алгоритмический и логический фундамент (CTL) стал основой для последующего развития символьной проверки моделей (Symbolic Model Checking)^[12]. Этот метод, работая с символьным представлением состояний, позволил верифицировать системы с огромным числом состояний (более 10²⁰)^[6].

За время своей работы в Техасском университете в Остине Эрнест Аллен Эмерсон был научным руководителем для 15 аспирантов (доктор философии (PhD)). Многие из его учеников сделали заметную карьеру в академических кругах и ведущих исследовательских лабораториях, внеся собственный вклад в развитие информатики^[13].

Среди наиболее известных учеников Эмерсона:

• Чаранджит Джатла (англ. Charanjit Jutla) — научный сотрудник в исследовательском центре IBM T.J. Watson Research Center. Известен как изобретатель первой однопроходной схемы аутентифицированного шифрования. Его научные интересы лежат в областях криптографии, теории кодирования и теории сложности^[14].
• Кедар Намджоши (англ. Kedar Namjoshi) — сотрудник Nokia Bell Labs^[15]. Его исследования сосредоточены на создании доказуемо корректных и безопасных программных систем, включая верификацию программ, проверку моделей и темпоральные логики^[16].
• Винит Кахлон (англ. Vineet Kahlon) — научный сотрудник в NEC Laboratories America, ранее работал в Google^[17]. Его работа посвящена автоматической верификации, программной инженерии и анализу параллельных программ. Внёс вклад в разработку инструментов для верификации ПО, таких как F-Soft^[18].
• Томас Валь (англ. Thomas Wahl) — после работы в Оксфордском университете и преподавания в Северо-Восточном университете перешёл в компанию GrammaTech, Inc. Его исследования касаются формальных методов для обеспечения надёжности и безопасности сложных вычислительных систем^[19].
• Джьотирмой Дешмукх (англ. Jyotirmoy Deshmukh) — доцент (англ. Associate Professor) в Университете Южной Калифорнии^[20]. Ранее работал главным инженером-исследователем в Toyota. Его научные интересы включают применение формальных методов для анализа киберфизических систем и верификацию встроенных систем управления^[21].
• Рупша Саманта (англ. Roopsha Samanta) — доцент (англ. Assistant Professor) в Университете Пердью^[22]. Является получателем награды NSF CAREER Award (2019) и исследовательской премии от Amazon (2021). Её работа сосредоточена на верификации и синтезе программ, а также на параллельных и распределённых системах^[23].

• 1998 — Paris Kanellakis Award (ACM)^[24]
• 1999 — Allen Newell Award (факультет информатики университета Карнеги — Меллон)^[25]
• 2006 — Test-of-Time Award (IEEE)^[26]
• 2007 — Премия Тьюринга вместе с Кларком и Сифакисом за их роль в развитии проверки моделей — высоко эффективную технику верификации программ, широко применяемую при разработке как программного так и аппаратного обеспечения^[27][28]