Una reciente tesis doctoral ha sacado a la luz un novedoso marco algorítmico centrado en la inclusión de lenguajes de palabras infinitas, un problema fundamental en la teoría de autómatas y aplicaciones en el campo más amplio de la verificación de software.
La investigadora de IMDEA Software Kyveli Doveri, supervisada por Pierre Ganty, presentó su tesis doctoral: “A Uniform Approach to Language Containment Problems” el pasado viernes 16 de febrero en la ETSIINF de la Universidad Politécnica de Madrid.
Contexto
En un mundo cada vez más digitalizado, la verificación de software es un aspecto crucial del desarrollo de software que garantiza la corrección, fiabilidad y calidad de los sistemas de software. Implica el proceso de comprobar si un sistema de software cumple los requisitos especificados y se comporta como se espera en diversas condiciones. Además, en el ámbito de la demostración de teoremas, en particular dentro de los métodos formales y el razonamiento automatizado, resulta imprescindible comprender los lenguajes formales que describen los comportamientos o propiedades de los sistemas. Estos lenguajes sirven de base para expresar y razonar sobre las propiedades de sistemas complejos, lo que convierte el problema de la inclusión de lenguajes en una herramienta vital para verificar teoremas intrincados y garantizar la integridad de las demostraciones formales.
La tesis
La investigación de Kyveli se centra en el desarrollo de herramientas computacionales para resolver problemas de inclusión de lenguajes formales.
El investigador de IMDEA Software ha desarrollado algoritmos para casos decidibles de inclusión entre autómatas de Büchi, un reto conocido por su complejidad. Estos algoritmos, como BAIT y FORKLIFT, se basan en relaciones de cuasorden para optimizar la búsqueda de contraejemplos, lo que los convierte en una valiosa herramienta para la verificación de software. Un elemento central de su eficacia es una caracterización de punto fijo de los lenguajes, que les permite manipular conjuntos finitos de estados de forma eficiente.
Además, la tesis establece un teorema similar al de Myhill-Nerode para subclases específicas de lenguajes temporizados aceptados por autómatas temporizados de un reloj. Este avance es fundamental para comprender mejor las propiedades de los lenguajes regulares y tiene importantes implicaciones para el modelado práctico de sistemas informáticos.
En resumen, estos nuevos algoritmos y teoremas no sólo amplían nuestra comprensión teórica, sino que también tienen el potencial de influir positivamente en diversas áreas de la informática, desde la verificación de programas hasta la demostración de teoremas en combinatoria de palabras. Un paso adelante en la era de la informática automatizada.
