Implementación de chequeadores de modelos para MAS

Tesina (Licenciatura en Informática) - Universidad Nacional de La Plata. Facultad de Informática, 2014.

1. Introducción -- 2. Lógicas modales -- 2.1 Lógica modal -- 2.2 Semántica relacional (o de Kripke) -- 2.2.1 Semántica de Scott-Montague -- 2.3 Chequeador de modelos -- 3.Combinación de lógicas normales y no normales -- 3.1 Una lógica multi-modal para MAS -- 3.2 Modelo multi-relacional -- 3.3 Fibrado de lógicas -- 3.4 Fibrado: Sintaxis y semántica -- 3.5 Correctitud y completitud de la lógica base -- 4. Implementación de un chequeador de modelos para N (Does) -- 4.1 Definiciones previas -- 4.2 Programación orientada a objetos -- 4.3 Definiciones básicas sobre Java -- 4.4 Principales dificultades -- 4.5 Representación del fibrado -- 4.5.1 Representación de frames y modelos -- 4.5.2 Representación de fórmulas -- 4.6 Evaluación de fórmulas -- 4.7 Implementación de Java -- 4.8 Consideraciones sobre la implementación -- 4.8.1 Validación de las relaciones de accesibilidad -- 4.9 Ejemplo de aplicación -- 5. Análisis de tiempos de ejecución -- 5.1 Análisis de ejecución del chequeador -- 5.1.1 Orden de ejecución de eval para fórmulas booleanas -- 5.1.2 Orden de ejecución de eval para fórmulas modales -- 5.2 Propuestas de mejoras -- 6. Estado del arte en chequeadores de modelos para MAS -- 6.1 MCK -- 6.2 MCMAS -- 6.3 Mocha -- 6.4 NuSMV -- 6.5 PRISM -- 6.6 VerICS -- 6.7 Otras herramientas para MAS -- 6.7.1 LoTREC -- 6.7.2 MAELIA -- 6.7.3 G A M A -- 7. Conclusiones y trabajo futuro -- A. Apéndice: Ejemplos de uso del chequeador de modelos