EpistemicModelChecker (EMC) un programa capaz de evaluar el estatus semántico de una fórmula epistémica en modelos multiagentes. El proceso de evaluación utilizado es el que describe el algoritmo model checking. Para el desarrollo del programa ha sido esencial el uso de dos librerías; Tweety project y GraphStream. EMC no es sino el primer paso de un proyecto en desarrollo que pretende mejorar las funcionalidades de dicha herramienta. Es por ello por lo que toda sugerencia, advertencia de bug, etc. es más que bienvenida. Para ello bien se puede contactar a través del email aportado más abajo, así como abriendo una entrada a través del siguiente enlace https://github.com/cagve/EpistemicModelChecker/issues.
Para poder ejecutar EMC basta con tener instalado una versión java superior a JAVA 11. La última versión de puede ser descargada en el siguente enlace: Java 14.
Para descargar y compilar el código se requiere además de la última versión de JavaFX
Para instalar EMC basta con descargar el archivo correspondiente para su sistema operativo en el siguiente enlace; Descargar.
- Introducir nuevo modelo
- Recargar modelo
- Ayuda
- Campo de texto donde introducir la fórmula
- Ejecutar el verificador
- Limpiar interfaz
- Área de texto donde se muestra el resultado
- Área gráfica donde se muestra el grafo del modelo
La introducción del modelo consiste en la creación de un archivo de texto (txt) en donde se escribe el modelo siguiendo la notación matemática. Aportamos ahora un ejemplo, así como algunas consideraciones a tener en cuenta.
W={w0,w1,w2}
Ra={<w0,w1>,<w2,w2>}
Rc={<w1,w1>,<w2,w1>}
Rb={<w2,w1>,<w0,w0>}
V(p)={w0,w1,w2}
V(q)={w2,w1}
V(r)={w0}
- Se pueden crear hasta un máximo de 10 mundos, empezando siempre por w0.
- El número de agentes está restringido a 4; a, b, c y d.
- El dominio de los átomos interpretables por EMC es: {p,q,r,s,t,u,v,w,x,y,z}
- Se pueden descargar ejemplos en el siguiente enlace: ejemplo de modelos
La sintaxis para la introducción de fórmulas es la siguiente.
| Operador | Ejemplo notación clásica | Ejemplo notación EMC |
|---|---|---|
| Negación* | ¬p | \lnot( p ) |
| Conjunción | p ∧ q | p \land q |
| Disyunción | p v q | p \lor q |
| Implicación | p → q | p \to q |
| Equivalencia | p ↔ q | p \eq q |
| Conocimiento* | Kap | Ka( p ) |
| Dual del conocimeinto* | Map | Ma( p ) |
*Es importante recalcar que los operadores monádicos deben escribirse siempre manteniendo los paréntesis que delimiten la fórmula a la que afectan
El proyecto ha sido desarrollado para un trabajo final de grado (TFG) en el departamento de filosofía de la Universidad de Málaga por:
- Carlos Aguilera Ventura (carlos.aguilera13416@gmail.com) Bajo la supervisión de:
- Alfredo Burrieza Muñiz
- Antonio Yuste Ginel
EMC está licenciado bajo GNUv3, véase: LICENCE