Conditional narrowing modulo membership equational logic theories with SMT solvers.

• Autores: Luis Manuel Aguirre García
• Directores de la Tesis: Narciso Martí Oliet (dir. tes.) , Isabel Pita Andreu (dir. tes.) , Miguel Palomino Tarjuelo (dir. tes.)
• Lectura: En la Universidad Complutense de Madrid ( España ) en 2024
• Idioma: inglés
• Títulos paralelos:
  • Estrechamiento condicional módulo lógicas ecuacionales de pertenencia con resolutores SMT.
• Tribunal Calificador de la Tesis: David de Frutos Escrig (presid.) , Francisco Javier López Fraguas (secret.) , Francisco Durán Muñoz (voc.) , Santiago Escobar Román (voc.) , Hernán Camilo Rocha Niño (voc.)
• Enlaces
  • Tesis en acceso abierto en: Docta Complutense
• Resumen

  • Esta tesis es un estudio sobre cómo mejorar la eficiencia del estrechamiento condicional módulo lógicas ecuacionales de pertenencia para problemas simbólicos de alcanzabilidad en lógica de reescritura, usando el lenguaje Maude. Con este fin, se han analizado distintos enfoques en la tesis. Para cada uno de ellos se ha definido un cálculo de alcanzabilidad y se ha demostrado su corrección y completitud débil. También se han desarrollado varios prototipos para algunos de estos cálculos.

    La lógica de reescritura, propuesta por Meseguer en 1992, es una lógica computacional orientada a la especificación de sistemas concurrentes. Esta lógica se ha diseñado con una semántica matemática precisa que permite probar propiedades de los sistemas especificados. La resolución de problemas de alcanzabilidad en lógica de reescritura es del mayor interés, ya que normalmente está asociada a la comprobación de propiedades de seguridad de las especificaciones.

    Aunque la reescritura sólo permite resolver problemas de alcanzabilidad con un estado inicial carente de variables, excepto para casos muy especiales de estados iniciales simbólicos, en un momento dado se demostró que el estrechamiento, que hasta entonces se utilizaba básicamente como método de unificación, se podía usar también para resolver problemas de alcanzabilidad con un estado simbólico inicial cualquiera.

    Algunos prototipos de alcanzabilidad han sido desarrollados en el lenguaje de especificación Maude usando sus capacidades reflexivas, y posteriormente se han añadido al motor de Maude como nuevas opciones, alcanzando un mejor rendimiento a través de su implementación en C++.

    Esta tesis lleva la alcanzabilidad un paso más allá, extendiendo tanto las clases de teorías de reescritura aceptables para el estrechamiento como los tipos de problemas de alcanzabilidad que se pueden formular.

    Todos los cálculos mostrados en esta tesis están basados en la unificación de un término con la cabeza de una regla, módulo un subconjunto de la teoría ecuacional subyacente a la teoría de reescritura considerada: sus axiomas. El primer cálculo mostrado en esta tesis se centra en el uso de la información de los tipos de los dos términos que se están unificando, para evitar aplicar reglas cuando la unificación no genera un término con el tipo requerido. El segundo cálculo usa la normalización del término sobre el que se intenta la alcanzabilidad así como la no reducibilidad de la composición de los unificadores aplicados en el cálculo para podar el espacio de estados. El tercer cálculo se centra en el uso de resolutores SMT como oráculo para algunas de las subteorías de la teoría ecuacional subyacente a la teoría de reescritura considerada. Finalmente, el cuarto cálculo usa un lenguaje de estrategias, junto con resolutores SMT, para podar más el espacio de estados, además de permitir la parametrización tanto de las teorías de reescritura como de las estrategias definidas para un problema de alcanzabilidad dado.