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.