Resumen de Especificacióncy validación de un protocolo de negociación multiagente usando técnicas de descripción formal

María Victoria Belmonte Martínez , José Luis Pérez de la Cruz , Francisco Andrés Triguero Ruiz

• Un aspecto básico en Inteligencia Artificial Distribuida (IAD) es el diseño de agentes automatizados que sean capaces de interactuar de una forma efectiva. Con el fin de modelar esta interacción entre agentes es necesario definir Protocolos de Negociación Multiagente. En este artículo se presenta la especificación de un protocolo de negociación que resuelve de forma cooperativa problemas de interacción multiagente sujetos a restricciones, en dominios no-cooperativos. El protocolo ha sido especificado y validado usando Técnicas de Descripción Formal (TDF). En concreto el lenguaje de especificación usado ha sido SDL. De esta forma se ha obtenido un modelo de validación que expresa las características esenciales del mismo de forma clara, concisa y consistente. El modelo ha sido validado con ayuda de la herramienta Geode, usando técnicas de simulación y técnicas de análisis de alcanzabilidad exhaustivo. En ambos casos los resultados obtenidos fueron satisfactorios. Por último y haciendo uso de lenguaje MSC, se han comprobado diferentes propiedades del protocolo de negociación.