Rajeev Alur es un profesor estadounidense de informática en la Universidad de Pensilvania que ha realizado contribuciones a los métodos formales , los lenguajes de programación y la teoría de autómatas , incluida en particular la introducción de autómatas cronometrados (Alur y Dill , 1994) y palabras anidadas (Alur y Madhusudan, 2004).
El profesor Alur nació en Pune . Obtuvo su licenciatura en informática en el Instituto Indio de Tecnología de Kanpur en 1987 y su doctorado en informática en la Universidad de Stanford en 1991. Antes de incorporarse a la Universidad de Pensilvania en 1997, trabajó en el Centro de Investigación en Ciencias de la Computación de los Laboratorios Bell . Su investigación ha incluido el modelado formal y el análisis de sistemas reactivos , sistemas híbridos , verificación de modelos , verificación de software , automatización del diseño para software integrado y síntesis de programas . Es miembro de la ACM , [1] miembro del IEEE y ha sido presidente del ACM SIGBED (Grupo de Interés Especial sobre Sistemas Integrados). Tiene el título de Profesor de la Familia Zisman en la UPenn desde 2003. [2]
En los últimos treinta años, Alur ha presentado varios modelos novedosos de computación que proporcionan las bases teóricas para el análisis, diseño, síntesis y verificación de sistemas informáticos. Si bien sus investigaciones se basan en algoritmos y lógica, con más de 52.000 citas, han encontrado aplicaciones en la teoría del control, los sistemas ciberfísicos, los sistemas multiagente y la síntesis de programas. Las contribuciones específicas que se enumeran a continuación son los aspectos más destacados de sus contribuciones fundamentales y de gran impacto a los fundamentos de la informática, por las que se le reconoce con el Premio Knuth 2024.
Autómatas temporizados: La comprobación de modelos clásicos se desarrolló para el análisis de sistemas discretos de estados finitos. En un artículo innovador publicado en ICALP 1991, Alur y Dill introdujeron una extensión de los autómatas con temporizadores continuos. Propusieron un algoritmo para analizar los sistemas de estados infinitos resultantes introduciendo una noción novedosa de bisimulación abstracta en el tiempo para la construcción algorítmica de cocientes de estados finitos. Este marco de autómatas temporizados se ha convertido en el modelo formal estándar para sistemas en tiempo real, inspirando mucha investigación en lógica de especificación, algoritmos de verificación, teoría del lenguaje formal y teoría de control. Problemas como "¿se produce un bloqueo de protocolo de comunicación?" y "sintetizar el controlador más general para mantener la seguridad", en presencia de restricciones de tiempo, se pueden formular y resolver utilizando problemas de decisión sobre autómatas temporizados. Estos algoritmos se han implementado en muchas herramientas y se han aplicado a la depuración de ejemplos del mundo real. Su trabajo sobre autómatas temporizados es uno de los artículos más citados en informática teórica: la versión de la revista TCS'95 tiene ahora más de 10 000 citas. Por este trabajo, Alur y Dill recibieron el premio inaugural de Verificación Asistida por Computadora (CAV) en 2008 y el premio inaugural Alonzo Church por contribuciones destacadas en lógica y computación en 2016.
Lógicas temporales en tiempo real: Una línea de investigación relacionada se ocupa de las extensiones de las lógicas temporales para especificar requisitos en tiempo real. Este trabajo proporciona un estudio básico de diferentes variantes basadas en las modalidades utilizadas (tiempo de ramificación versus tiempo lineal), la semántica subyacente para el tiempo (denso versus discreto) y las primitivas permitidas en la sintaxis para expresar restricciones temporales. En una secuencia de artículos, Alur y coautores identificaron las restricciones sintácticas y semánticas necesarias para la decidibilidad y desarrollaron algoritmos óptimos de verificación de modelos siempre que fue posible. Los artículos importantes de esta serie incluyen "Verificación de modelos de sistemas en tiempo real" [Alur, Courcoubetis, Dill; LICS'90 e I&C'93; ganador del premio LICS Test-of-Time en 2010]; "Una lógica realmente temporal" [Alur y Henzinger; [FOCS'89 y JACM'94] y "Beneficios de relajar la puntualidad" [Alur, Feder, Henzinger; PODC'91 y JACM'96].
Autómatas híbridos: Los sistemas integrados, como los controladores de los sistemas automotrices, médicos y de aviónica, consisten en una colección de módulos de software que interactúan y reaccionan ante un entorno analógico y lo controlan. La disciplina de los sistemas híbridos, que combina los principios de modelado discreto y continuo, está demostrando ser crucial en el diseño y análisis sistemático de sistemas integrados críticos para la seguridad. El trabajo de Alur, en colaboración con Henzinger, que introdujo los "autómatas híbridos" y los algoritmos de verificación simbólica para autómatas híbridos, fue el primero en formalizar el modelo computacional para sistemas híbridos y condujo al desarrollo de verificadores de modelos para sistemas híbridos. Este trabajo muestra cómo los algoritmos simbólicos que manipulan poliedros se pueden utilizar de manera efectiva para el análisis de ecuaciones diferenciales e inspiró una cantidad sustancial de investigaciones posteriores tanto en las comunidades de métodos formales como de teoría de control. Entre los artículos muy influyentes se incluyen "El análisis algorítmico de los sistemas híbridos" [TCS'95], "Verificación simbólica automática de los sistemas integrados" [TSE'96] y "Abstracciones discretas de los sistemas híbridos" [Proc. IEEE, 2000]. Los conceptos de modelado en autómatas híbridos se han incorporado en herramientas de modelado estándar industriales como Simulink, Modelica y LabVIEW.
Razonamiento estratégico para sistemas multiagente: lógica temporal de tiempo alternante (ATL) [Alur, Henzinger, Kupferman; FOCS'97 y JACM'02] es un lenguaje de teoría estratégica para especificar y razonar sobre los objetivos de agentes individuales y equipos de agentes desde una perspectiva de teoría de juegos. Este trabajo proporciona un análisis riguroso de la decidibilidad y la complejidad de diferentes fragmentos lógicos basados en la naturaleza de la interacción entre agentes (sincrónica vs. asincrónica) y la observabilidad. Módulos reactivos [Alur y Henzinger; LICS'96 y FMSD'99] es un formalismo de modelado ejecutable y compositivo para describir formalmente la interacción entre múltiples componentes heterogéneos respaldados por reglas de asunción-garantía para el razonamiento. Estos artículos fueron el catalizador de una extensa investigación sobre la visión de la teoría de juegos para el diseño y análisis de sistemas multiagente en verificación formal, teoría de control y planificación de IA. El artículo ATL JACM'02 ganó el premio AAMAS Influential Paper Award en 2021.
Lenguajes visiblemente pushdown: Alur y Madhusudan introdujeron el modelo de “palabras anidadas” para la representación de datos con un orden lineal y una correspondencia jerárquicamente anidada de elementos [“Lenguajes visiblemente pushdown”, STOC'04 y JACM'09]. Las palabras anidadas generalizan tanto las palabras como los árboles ordenados y permiten operaciones tanto con palabras como con árboles. Los autómatas de palabras anidadas (también conocidos como autómatas visiblemente pushdown) son aceptadores de estados finitos que definen la clase de lenguajes regulares de palabras anidadas. Esta clase tiene la mayoría de las atractivas propiedades teóricas de las que disfrutan los lenguajes de palabras regulares clásicos. Por ejemplo, los autómatas de palabras anidadas deterministas son tan expresivos como sus contrapartes no deterministas; la clase está cerrada bajo muchas operaciones; la pertenencia, el vacío, la inclusión de lenguajes y la equivalencia de lenguajes son todas decidibles; y la definibilidad en la lógica monádica de segundo orden corresponde exactamente a la reconocibilidad de estados finitos. Esta teoría proporciona una nueva base para la verificación algorítmica de programas estructurados: en lugar de ver el programa como un lenguaje libre de contexto, sobre las palabras, se puede ver como un lenguaje regular de palabras anidadas, y esto permite la verificación del modelo de muchas propiedades (como la inspección de la pila) que no se pueden expresar en las lógicas de especificación existentes, lo que conduce a nuevas herramientas de análisis de programas.
Síntesis de programas: Alur y sus colaboradores introdujeron el problema de la síntesis guiada por sintaxis (ahora conocida como SyGuS), junto con soluciones algorítmicas basadas en búsquedas, como un marco unificador para sintetizar fragmentos de programas que cumplan con las especificaciones lógicas [“Síntesis guiada por sintaxis”, FMCAD'13]. Este paradigma fue una contribución fundamental del proyecto ExCAPE de NSF Expeditions in Computing dirigido por Alur. La síntesis de programas basada en búsquedas es ahora un tema fundamental en los lenguajes de programación, con una competencia anual de solucionadores, lo que lleva al desarrollo de herramientas de programación para el usuario final en empresas como AWS, Google y Microsoft.
Liderazgo, educación y tutoría: el profesor Alur es un líder de alto nivel en las áreas de métodos formales y lógica en informática y ha trabajado como presidente de programa y/o presidente general de conferencias destacadas como LICS, CAV y FLoC. También ha desempeñado un papel crucial en el establecimiento de los sistemas ciberfísicos (CPS) como una disciplina académica distinta en la intersección de la teoría de control, el software integrado y los métodos formales. Fue (co)presidente de las primeras reuniones sobre este tema: taller de sistemas híbridos (1995), EMSOFT (2003) y HSCC (2004), y se desempeñó como presidente general del recién formado Grupo de Interés Especial en Sistemas Integrados (SIGBED) de la ACM. Es el autor del libro de texto "Principios de los sistemas ciberfísicos" [MIT Press, 2015]. Los métodos formales para los CPS han encontrado ahora aceptación en herramientas y aplicaciones en industrias como Mathworks y Toyota. Alur ha asesorado a 45 estudiantes de doctorado y posdoctorado. Entre los alumnos destacados se incluyen S. Bansal (Georgia Tech), P. Černý (TU Vienna), S. Chaudhuri (UT Austin), L. D'Antoni (Wisconsin), J. Deshmukh (USC), R. Grosu (TU Vienna), K. Mamouras (Rice), M. Parthasarathy (UIUC), M. Raghothaman (USC), C. Stanford (UC Davis), A. Trivedi (Colorado) y B.-Y. Wang (Academia Sinica, Taiwán). Premio Knuth
Por sus contribuciones a la especificación y verificación de sistemas reactivos e híbridos.
Por el trabajo pionero en la verificación de modelos de sistemas en tiempo real.
