Completitud e implementación de modalidades en MAS

Abstract

En este trabajo de grado realizamos un estudio sobre lógicas modales y combinaciones de ellas, haciendo énfasis en operadores modales aplicables al desarrollo de sistemas multi-agentes. Algunos de estos operadores son normales y otros no-normales, como es habitual en esta clase de sistemas. Nos concentramos en la combinación de estos dos tipos de operadores, poniendo particular atención a la teoría de modelos y en su utilidad para demostrar completitud y/o decidibilidad de lógicas. Utilizamos dos tipos diferentes de técnicas de combinación: fibrado y unión. Para la técnica de fibrado probamos las propiedades de completitud y modelo finito para dar sustento a implementaciones computacionales para la lógica resultante y habilitar el diseño de algoritmos que computen satisfactibilidad de una fórmula dentro de un modelo; esto es: teniendo un modelo y una fórmula, podemos averiguar si la fórmula es verdadera en tal modelo. Sobre la base de estas propiedades definimos diferentes chequeadores de modelos. Logramos una implementación computacional en los lenguajes PROLOG y SPINdle partiendo de la definición de los chequeadores para el fibrado e investigamos la complejidad computacional de los algoritmos resultantes. Para la técnica de unión construimos un chequeador de modelos.