TITLE: A new framework for multi-agent system verification
SPEAKER: Franco Raimondi (Middlesex University, UK)

ABSTRACT:

Recently, there has been a proliferation of tools and
languages for modeling multi-agent systems (MAS). Verification tools,
correspondingly, have been developed to check properties of these
systems. Most MAS verification tools, however, have their own input
language and often specialize in one verification technology, or only
support checking a specific type of property.
In this talk I present an extensible framework that leverages mainstream
verification tools to successfully reason about various types of
properties. The Brahms agent modeling language is used to demonstrate
the effectiveness of the approach (Brahms is used to model real
instances of interactions between pilots, air-traffic controllers, and
automated systems such as the NASA autopilot). The framework takes as
input a Brahms model along with a Java implementation of its semantics
and explores all possible behaviors of the model. The model is then
verified using mainstream model checkers, including PRISM, SPIN, and NuSMV.
(This is work in collaboration with Neha Rungta @NASA Ames and
Richard Stocker @Liverpool)