Algoritmos heurísticos y aplicaciones a métodos formales

Abstract

Los algoritmos de optimización basados en búsquedas locales recorren el espacio de soluciones tratando de conseguir una buena solución en un tiempo razonable para minimizar o maximizar un valor y tratando de evitar quedarse estancado en mínimos o máximos locales. Parten de una solución y la modifican aplicando ciertos operadores para calcular soluciones vecinas que mejoren la calidad de la solución inicial. Estas técnicas de búsqueda se aplican a problemas NP-completos en los que el espacio de búsqueda es muy grande y es necesario el uso de funciones heurísticas para eliminar rutas de búsqueda no prometedoras. Los métodos evolutivos se han aplicado de manera exitosa en los últimos años a los métodos formales. Los métodos formales son técnicas que típicamente han sido aplicadas tanto a la especificación formal como a la verificación formal de sistemas, buscando desarrollar especificaciones claras, concisas y sin ambigüedades. El punto de encuentro entre estas dos áreas es debido a un problema práctico que aparece en los métodos formales: éstos deben analizar sistemas en los que el número de estados de la especificación crece exponencialmente. Es aquí donde las heurísticas proporcionan estrategias eficientes. En esta tesis se introduce una nueva técnica evolutiva llamada River Formation Dynamics basada en el proceso geológico de la formación de los ríos. Se ha diseñado un algoritmo basado en estas ideas para aplicarlo a resolver distintos problemas NP-completos, como por ejemplo al problema del viajante de comercio. Además se han definido nuevos problemas NP-completos en los que es necesario adaptar el algoritmo básico a cada caso. También se ha aplicado River Formation Dynamics a escenarios típicos de métodos formales donde se ha utilizado esta técnica para alcanzar ciertos estados/transiciones de una especificación definida por una máquina de estados finitos.