PDF de programación - Implementación Java de un Chequeador de Modelos para un Sistema Multiagente Multimodal

Implementación Java de un Chequeador de Modelos

para un Sistema Multiagente Multimodal

Clara Smith1, Gastón Fournier1, and Leonardo Otonelo1

1 Facultad de Informática, Universidad Nacional de La Plata

calle 50 esq. 120, 1900 La Plata, Argentina

{csmith,gfournier,lotonelo}@info.unlp.edu.ar

Resumen. En este trabajo acercamos conceptos de la lógica modal -cuando es
usada como herramienta para la modelización de sistemas multiagentes- al
lenguaje de programación Java. Construimos un framework para definir
estructuras de frames modales y de modelos modales, y chequear en ellos la
validez de fórmulas bien formadas escritas en un lenguaje de agentes.

1 Introducción

Sistemas Multi-Agentes (MAS) es un paradigma computacional para modelar
sistemas de inteligencia distribuida. En este paradigma, un sistema computacional es
visto como una composición de un conjunto de componentes autónomos y
heterogéneos, llamados agentes, que interactúan unos con otros. MAS apunta
principalmente al modelado, entre otra cosas, de agentes cognitivos o reactivos que
coexisten y dependen unos de otros para alcanzar sus objetivos. Los agentes imitan los
atributos y capacidades humanas como son descriptos en psicosociología y más
ampliamente en las ciencias cognitivas; los agentes pueden ―razonar‖, ―adaptarse‖,
―aprender‖. Las estructuras son comúnmente descriptas con una terminología
sociológica: ―organización‖, ―comunidad‖, ―institución‖. En este contexto, las lógicas
modales –vistas como extensiones decidibles de la lógica proposicional- son usadas
como un enfoque formal para la construcción de MAS.

Uno de nuestros objetivos en este trabajo es mostrar cómo acercar conceptos y
herramientas de la lógica modal –cuando es usada como lenguaje para la
modelización- a un lenguaje de programación actual y de amplia difusión como Java.

Un chequeador de modelos es un programa tal que dado un modelo para una
lógica y una fórmula escrita en el lenguaje de dicha lógica determina si la fórmula es
verdadera en el modelo o no lo es.

Implementamos en Java el chequeador de modelos descripto en [1]. Proveemos,
para las estructuras del chequeador, un framework lo suficientemente abstracto que
puede ser instanciado con cualquier tipo de frame multimodal y que está
implementado en un lenguaje de programación bien conocido como Java. Existen
implementaciones de chequeadores de modelos (como MCK de la U. de Wales,
MCMAS, del Imperial College, Mocha, de las U. de Berkeley, Pensylvannia y NYU)
pero ellos, en su mayoría, fueron diseñados para ciertos tipos específicos de lógicas
temporales (LTL Linear Temporal Logic y CTL Computational Tree Logic) y lógicas
epistémicas.

El algoritmo que programamos tiene como referencia la lógica base descripta en
[2,3]: una lógica multimodal multiagente útil para modelar sistemas donde intervienen
múltiples agentes que interactúan para intentar cumplir sus objetivos. Dicha lógica

ASAI 2015, 16º Simposio Argentino de Inteligencia Artificial. 44 JAIIO - ASAI 2015 - ISSN: 2451-758517 combina los operadores modales normales bien conocidos Bela x, Inta x, y Goala x
(usados para modelar ―el agente a cree x‖, ―el agente a tiene la intención de que x sea
verdadero‖ y ―el agente a tiene el objetivo x‖), con operadores no normales de la
forma Doesa x (para referirse a acciones intencionales como ―el agente a lleva a cabo
x exitosamente‖) [4].

En los trabajos [2,3] se estudia la transferencia de propiedades de lógicas
pequeñas (o ―de propósitos especiales‖ para modelar creencias, intenciones, etc) a la
combinación multimodal multiagente resultante de ellas. Se analizan las propiedades
de completitud y decidibilidad, concluyendo que ambas son preservadas por la
combinación, en el sentido de conservatividad dado en [5,6]. Este resultado sirve de
base para la búsqueda de algoritmos computacionales correctos para esa lógica
combinada. En [1] ya se había descripto la exploración de un código fuente para
implementaciones del chequeador, pero usando lenguajes declarativos, como Prolog.
Nuestra motivación, a partir de los trabajos [1,2,3], consiste en lograr una
implementación computacional flexible hecha esta vez en un lenguaje imperativo bien
conocido, ampliamente difundido y usado en ámbitos comerciales como lo es Java.

El resto del artículo se organiza como sigue. En la Sección 2 presentamos el
algoritmo chequeador de modelos que sirve de base para la construcción de un
framework Java para MAS modales, framework que finalmente implementamos. En la
Sección 3 presentamos el código Java para los módulos más relevantes del
framework, con algunas discusiones interesantes referidas al código. La Sección 4
contiene nuestras conclusiones.

2 El Chequeador de Modelos

En lógica modal un modelo se define como un par M = (F, V) donde F = (W, R)
es un frame, W es un conjunto de puntos o mundos posibles, R es un conjunto de
relaciones de accesibilidad entre mundos y V es una función de valuación que asigna a
cada proposición p del lenguaje modal un subconjunto V(p) de W [7].

Las lógicas multimodales son, por lo general, una combinación de lógicas
monomodales específicas que da lugar a teorías complejas. La lógica para la que
implementamos el chequeador de modelos se llama N(Does) [1]; es una lógica normal
multimodal multiagente (N) que se combinó con operadores no normales (los
operadores Does de acción, uno para cada agente) mediante una técnica de fibrado
[8,9].

Intuitivamente, fibrar dos lógicas consiste en organizarlas en dos niveles. Es por
eso que el algoritmo chequeador de modelos funciona así: dado un modelo para la

lógica y dada una fórmula φ del lenguaje de la lógica, el chequeador parsea la fórmula
y ―navega‖ por la parte normal (de Kripke) del modelo; cuando encuentra una
subfórmula no normal, el chequeador pasa a otr nivel y ―navega‖ por un modelo
especial llamado de Scott-Montague1. Es decir, en la lógica base hay una parte modal
normal en un nivel y una parte ―no normal‖ en otro nivel.

Técnicamente, se convierten en (nuevas) letras proposicionales todas las
subfórmulas no normales que hay en la fórmula a chequear, logrando que el chequeo
final se haga sobre un modelo único, ―aplanado‖. Para lograr esto hay que chequear la



1 Podemos generalizar la semántica tradicional de Kripke de la siguiente manera. En lugar de
tener una colección de mundos conectados a un mundo w mediante una relación R,
consideramos un conjunto de colecciones de mundos conectados a w [10]. Estas colecciones
son los vecindarios (neighbourhoods) de w. Formalmente, un frame de Scott-Montague es un
par ordenado <W, N> donde W es un conjunto de mundos y N es una función total que
asigna para cada w en W un conjunto de subconjuntos de W (los vecindarios de w).

ASAI 2015, 16º Simposio Argentino de Inteligencia Artificial. 44 JAIIO - ASAI 2015 - ISSN: 2451-758518 validez de cada fórmula no normal en su correspondiente modelo de Scott-Montague,
transformarla a una nueva letra proposicional si es verdadera, y así tener un modelo
único sobre el cual evaluar.

Tenemos entonces tres procedimientos principales:



Function MCN(Does)(<A,W,Bi,Gi,Ii,V´,di>,φ)
input: modelo <A,W,Bi,Gi,Ii,V´,di>, fórmula φ
computar MMLDoes(φ)
for every α  MMLDoes(φ)

i := identificar el agente que aparece en α
if (MCDoes(di(w),α) = true) then


V’(w):= V’(w)  pα
construir φ’



return MCN (<A,W,Bi,Gi,Ii,V´,di>,φ’)

Function MCDoes(di(w),α)
input: modelo Scott-Montague, subfórmula monolítica maximal α

while quedan neighbourhoods sin chequear en di(w)

nk = set ni  di(w)
for every w  nk

if α  v(w) then return false

return true



Function MCN (<A,W,Bi,Gi,Ii,V´,di>,φ’)

input: un modelo M=<A,W,Bi,Gi,Ii,V´,di>,φ’)

for every w  W

if check(<A,W,Bi,Gi,Ii,V´>, φ’)

return w

return false

La descripción de estos tres módulos del chequeador es la siguiente: la función
MCN(Does) (llamada así por ―model checker para la lógica N(Does)‖) primero computa
el conjunto MMLDoes(φ) de subfórmulas monolíticas maximales de φ2. Para cada una de
éstas, identifica el agente que está llevando a cabo la acción con el Does. Luego,
averigua los mundos en los que dicha acción es llevada a cabo satisfactoriamente.
Para esto, la función MCDoes es invocada con un modelo Scott-Montague como
parámetro.

Sea φ una fórmula y MMLDoes(φ) el conjunto de subfórmulas monolíticas maximales
de φ pertenecientes al lenguaje LDoes. Sea φ’ la fórmula obtenida reemplazando cada
subfórmula α  MMLDoes(φ) por una nueva letra proposicional pα [FG94]. La nueva
fórmula φ’ fue construida sin las modalidades Does, ya que éstas se reemplazaron, y
será uno de los inputs del chequeador MCN.

Notar entonces que el chequeador principal MCN es, en términos generales, la
implementación de la función de valuación sobre el modelo multimodal resultante de
haber ―aplastado‖ los modelos no normales de Scott-Montague.



2 Las fórmulas monolíticas son las que empiezan con un operador modal. Ej: Doesx(A).
LDoes(φ) se refiere al lenguaje de la lógica restringido a las fórmulas que tienen solo
operadores no nor