SSP Group Meeting

11am, 16 August, 2005
Room 4.03, Appleton Tower
CISA, School of Informatics
University of Edinburgh

Run-Time Model Checking of Interaction and Deontic Models for Multi-Agent Systems

Nardine Osman

My thesis proposal will be presented during this SSP talk. The goal of this thesis is the verification of multi-agent systems. However, the nondeterministic nature of these systems and the lack of an explicitly predefined set of agents results in difficulties when verifying such systems as opposed to verifying traditional hardware or software systems.
We argue that interactions, the backbone that holds a multi-agent system together, may be affected by: (a) interaction rules for coordinating messages between agents, (b) deontic rules for specifying obligations, permissions, and prohibitions, and (c) rules on the agent level for dealing with agents' knowledge, belief system, desires, goals, intentions, etc. We then propose the use of a dynamic model checker which may be invoked at runtime to verify dynamic properties of the interaction and deontic models.