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
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.